Ph.D
Group : Large-scale Heterogeneous DAta and Knowledge
Modeling and Qualitative Simulation of Hybrid Systems
Starts on 01/10/2015
Advisor : DAGUE, Philippe
Funding : Contrat de thèse d'autres organismes
Affiliation : Université Paris-Saclay
Laboratory : LRI - LaHDAK
Defended on 29/11/2018, committee :
Directeur :
- Philippe DAGUE Université Paris-Sud
Co-encadrant :
- Jean-Pierre GALLOIS, CEA LIST
Rapporteurs :
- Walid TAHA ,Université de Halmstad
- Goran FREHSE, ENSTA-ParisTech
Examinateurs :
- Erika ÁBRAHÁM, Université RWTH Aachen
- Sylvain CONCHON, Université Paris-Sud
Research activities :
Abstract :
Hybrid systems are complex systems that combine both discrete and continuous behaviors. Verifying behavioral or safety prop- erties of such systems, either at design stage or on-line is a challenging task. Actually, computing the reachable set of states of a hybrid system is undecidable. One way to verify those properties over such systems is by computing discrete abstractions and inferring them from the abstract system back to the original system. We are concerned with abstractions oriented towards hybrid systems diagnosability checking. Our goal is to create discrete abstractions in order to verify if a fault that would occur at runtime could be unambiguously detected in finite time by the diagnoser. This verification can be done on the abstraction by classical methods developed for discrete event systems, which provide a counterexample in case of non-diagnosability. The absence of such a counterexample proves the diagnosability of the original hybrid system. In the presence of a counterexample, the first step is to check if it is not a spurious effect of the abstraction and actually exists for the hybrid system, witnessing thus non-diagnosability. Otherwise, we show how to refine the abstraction and continue the process of looking for another counterexample.