How to be sure a faulty system does not always appear healthy?

Autor: Dague, Philippe, He, Lulu, Ye, Lina
Přispěvatelé: Données et Connaissances Massives et Hétérogènes (LRI) (LaHDAK - LRI), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI)
Jazyk: angličtina
Rok vydání: 2019
Předmět:
Zdroj: Innovations in Systems and Software Engineering
Innovations in Systems and Software Engineering, In press, ⟨10.1007/s11334-019-00357-z⟩
Innovations in Systems and Software Engineering, Springer Verlag, In press, ⟨10.1007/s11334-019-00357-z⟩
ISSN: 1614-5046
1614-5054
DOI: 10.1007/s11334-019-00357-z⟩
Popis: International audience; Fault diagnosability (allowing one to determine with certainty whether a given fault has effectively occurred based on the available observations) is a crucial and challenging property in complex system automatic control, which generally requires a high number of sensors, increasing the system cost, since it is quite a strong property. In this paper, we analyze a new system property called manifestability, that is a weaker requirement on system observations for having a chance to identify on-line faults: that a faulty system cannot always appear healthy. We propose an algorithm with PSPACE complexity to automatically verify it for finite automata, 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 extend our approach to verify manifestability of real-time systems modeled by timed automata, proving that it is undecidable in general but under some restricted conditions it 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.
Databáze: OpenAIRE
Externí odkaz: