Formal verification at design stage of diagnosis related properties for discrete event and real-time systems
by Lulu He
Wednesday 18 May 2022 at 10am
Room 435 (salle des thèses), building 650, 6 Rue Noetzlin, 91190 Gif-sur-Yvette.
Abstract: Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on a system property called diagnosability. Diagnosability describes the system property allowing one to determine at design stage whether a given fault occurring online will be identifiable with certainty based on the available observations, which is an alternative to testing that can only show the presence of failures without guaranteeing their absence. The diagnosability problem of discrete event systems has received considerable attention in the literature, but little work takes into account explicit time constraints during this analysis. However such constraints are naturally present in real-life systems and cannot be neglected considering their impact on this property. We proposed in our master work a new SMT (Satisfiability Modulo Theories)-based approach to verify bounded time diagnosability on timed automata. The idea is to encode in SMT the necessary and sufficient condition for diagnosability. In order to improve the efficiency of our method (the problem is PSPACE-complete), we propose now an incremental extension of it based on the use of parameterized over- and under-approximations generalizing the CEGAR (CounterExample-Guided Abstraction Refinement) method. We show the improvement provided through experimental results.
Nevertheless, diagnosability is a quite strong property, which generally requires a high number of sensors. Consequently, it is not rare that developing a diagnosable system is too expensive. In order to guarantee from design an adequate level of safety in an economical and efficient way, we propose two approaches.
The first one consists in designing diagnosable discrete event systems by using delay blocks. Indeed, what if a system is revealed as non-diagnosable? One classical way is to add sensors. We propose a new non-intrusive way to make diagnosable a non-diagnosable system by merely adding delay blocks on some observable events, thus deferring their observations. As far as we know, this is the first attempt to remove non-diagnosability with delay blocks without using controllable events or changing the structure of systems. Our approach is encoded into an SMT formula, whose correctness and efficiency are demonstrated by our experimental results.
The second one consists in analyzing a new system property called manifestability, that is a weaker requirement on system observations for having a chance to identify online fault occurrence and can be verified at design stage. Intuitively, this property makes sure that a faulty system cannot always appear healthy, i.e., has at least one future behavior after fault occurrence observably distinguishable from all normal behaviors. We first define the manifestability of finite state automata for discrete event systems and propose an algorithm with PSPACE complexity to automatically verify it and prove that the problem of manifestability verification itself is PSPACE-complete. The experimental results show the feasibility of our algorithm from a practical point of view. Then we define the manifestability of real-time systems modeled by timed automata by taking into account time constraints, and extend our approach to verify manifestability for these systems, proving that it is undecidable in general but, under some restricted conditions, becomes PSPACE-complete. Finally we encode this property into an SMT formula, whose satisfiability witnesses manifestability, before presenting experimental results showing the scalability of our approach.
Jury:
- M. Yannick PENCOLÉ - Rapporteur - Chargé de Recherche CNRS, HDR, LAAS-CNRS
- M. Lakhdar SAÏS - Rapporteur - Professeur, Université d'Artois et CNRS, CRIL
- M. Thierry JÉRON - Examinateur - Directeur de Recherche Inria, Centre Inria Rennes -- Bretagne Atlantique
- M. Sylvain CONCHON - Examinateur - Professeur, Université Paris-Saclay, LMF
- M. Philippe DAGUE - Directeur de thèse - Professeur émérite, Université Paris-Saclay, LMF
- Mme Lina YE - Co-encadrant de thèse - Maître de Conférences, CentraleSupélec, Université Paris-Saclay, LMF