Diagnosis of Hybrid Systems with Model-Checkers

Research areas

Description

 Model-Based Diagnosis (MBD) is the Artificial Intelligence of detecting faults in a monitored system and, if there is any, identifying (which one?) and isolating (where?) those.  MBD uses a description of the system (the model) and an observation of the actual system to reason about what possibly happened on the system.

In this project we want consider <i>hybrid systems</i>.  HS are dynamic systems whose behaviour involves both continuous state variables (such as the temperature) and discrete ones (such as the position on/off of a switch).  HS are particularly hard to reason about because the continuous aspect leads to infinite state space while the discrete one requires to search.

The purpose of this project is to use model-checkers, and in particular UPPAAL, to compute diagnoses.  Model-checkers are programs that automatically verify specifications in system models, for instance the fact that no two agents can access the same critical bit of memory at the same time.  Many model-checking problems require to compute specific executions (or paths) in the system model.  The model-checker can then be used to verify diagnoses: for instance, verifying whether the system's observed behaviour is normal consists in finding a system execution that matches the observation and that does not include any faulty event.  The project will be primarily about how to formulate the right questions to the model-checker and how to check its answers. 

Goals

The goal of the project is to understand the potential of model-checkers for the diagnosis of hybrid systems. 

Requirements

The implementation requirements is not too high.  The project can probably be written in python or other script language that will call the right methods. 

Background Literature

* M.-O. Cordier and Chr. Largouët. Using model-checking techniques for diagnosing discrete-event systems. In International Workshop on Principles of Diagnosis (DX-01). pp.~39--46. 2001.

* Al. Grastien and P. Haslum and S. Thiébaux. Exhaustive diagnosis of discrete event systems through exploration of the hypothesis space. In International Workshop on Principles of Diagnosis (DX-11). pp.~60--67. 2011.

Keywords

Model-Based Diagnosis

Hybrid Systems

Model-Checking

 

Updated:  1 November 2018/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing