Formal verification at design stage of diagnosis related properties for discrete event and real-time systems
Vérification formelle au stade de la conception de propriétés liées au diagnostic des systèmes à événements discrets et temps réel
Résumé
Fault diagnosis is a crucial and chal- lenging 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 for- mula, 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 can- not 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 algo- rithm 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 for- mula, whose satisfiability witnesses manifestability, before presenting experimental results showing the scalability of our approach.
Le diagnostic de pannes est une tâche cruciale et difficile dans le contrôle automatique des systèmes complexes, dont l’efficacité dépend d’une propriété du système appelée diagnosticabilité. La diagnosticabilité décrit la propriété du système permettant de déterminer dès la phase de conception si un défaut donné se produisant en ligne sera identifiable avec certitude sur la base des observations disponibles, ce qui est une alternative aux tests qui ne peuvent que montrer la présence de défaillances sans garantir leur absence. Le problème de diagnosticabilité des systèmes à événements discrets a reçu une attention considérable dans la littérature, mais peu nombreux sont les travaux qui prennent en compte des contraintes de temps explicites lors de cette analyse. Or de telles contraintes sont naturellement présentes dans les systèmes réels et ne peuvent être négligées compte tenu de leur impact sur cette propriété. Nous avons proposé dans notre travail de master une nouvelle approche à base de SMT (Satisfiability Modulo Theories) pour vérifier la diagnosticabilité en temps borné sur les automates temporisés. Afin d’améliorer l’efficacité de notre méthode (le problème est PSPACE-complet), nous en proposons à présent une extension incrémentale fondée sur l’utilisation de sur- et sous-approximations paramétrées dans une généralisation de la méthode CEGAR (raffinement d’abstraction guidé par un contre-exemple). Nous montrons l’amélioration apportée au travers de résultats expérimentaux. Néanmoins, la diagnosticabilité est une propriété assez forte, qui nécessite généralement un nombre élevé de capteurs. Par conséquent, il n’est pas rare que le développement d’un système diagnosticable soit trop coûteux. Afin de garantir dès la conception un certain niveau de sûreté de fonctionnement de manière économique et efficace, nous proposons deux approches. La première consiste à concevoir des systèmes à événements discrets diagnosticables en utilisant des blocs de retard. En effet, que se passe-t-il si un système se révèle comme non diagnosticable ? Une manière classique est d’ajouter des capteurs. Nous proposons une nouvelle manière non intrusive de rendre diagnosticable un système non diagnosticable en ajoutant simplement des blocs de retard sur certains événements observables, reportant ainsi leurs observations. Notre approche est codée dans une formule SMT, dont l’exactitude et l’efficacité sont démontrées par nos résultats expérimentaux. La seconde consiste à analyser une nouvelle propriété du système appelée manifestabilité, qui est une exigence plus faible sur les observations du système pour avoir une chance d’identifier l’occurrence des défauts en ligne et peut être vérifiée au stade de la conception. Intuitivement, cette propriété garantit qu’un système défectueux ne peut pas toujours apparaître sain, c’est-à-dire qu’il a au moins un comportement futur après l’apparition d’un défaut qui se distingue par l’observation de tous les comportements normaux. Nous définissons d’abord la manifestabilité des automates à états finis pour les systèmes à événements discrets et proposons un algorithme de complexité PSPACE pour la vérifier automatiquement et prouvons que le problème de vérification de la manifestabilité lui-même est PSPACE- complet. Les résultats expérimentaux montrent la faisabilité de notre algorithme d’un point de vue pratique. Ensuite, nous définissons la manifestabilité des systèmes temps-réel modélisés par des automates temporisés en tenant compte des contraintes de temps, et étendons notre approche pour vérifier la manifestabilité de ces systèmes, prouvant qu’elle est indécidable en général mais, sous certaines conditions restreintes, devient PSPACE- complet. Enfin, nous encodons cette propriété dans une formule SMT, dont la satisfaisabilité témoigne de la manifestabilité, avant de présenter des résultats expérimentaux montrant le passage à l’échelle de notre approche.
Origine : Version validée par le jury (STAR)