Oratrice: Lina Ye (Maître de Conférence, Laboratoire LRI, Université Paris-Sud 11 et CentraleSupélec, Université Paris-Saclay)
Titre: Formal Verification of hybrid Systems based on Timed Abstraction
Hybrid systems are complex systems that combine both discrete and continuous behaviors. Verifying behavioral or safety properties of such systems at design stage such as state reachability, diagnosability, and predictability is a challenging task. Actually, computing the reachable set of states of a hybrid system is an undecidable matter due to the infinite state space of continuous systems. One way to verify these properties over such systems is by computing abstractions and inferring them from the abstract system back to the original system. In our recent work, we are concerned with abstractions oriented towards hybrid systems, illustrated by checking diagnosability property, which can be applied on safety properties as well. Our goal is to create timed abstractions (here timed automata) in order to verify, at design stage, if this property is satisfied on them. This verification can be done on the timed abstraction by SMT, which provides a counterexample in case that the property is not satisfied. 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, guided by the elimination of the counterexample (counterexample guided abstraction refinement), and continue the process of looking for another counterexample until either a final result is obtained or we reach an inconclusive verdict. Abstractions as timed automata are studied as they allow one to handle time constraints that can be captured at a qualitative level from the hybrid system.