How to Be Sure a Faulty System Does Not Always Appear Healthy?
Title | How to Be Sure a Faulty System Does Not Always Appear Healthy? |
Publication Type | Book Chapter |
Year of Publication | 2018 |
Authors | Ye, L, Dague, P, Longuet, D, Brandán Briones, L, Madalinski, A |
Editor | Atig, MFaouzi, Bensalem, S, Bliudze, S, Monsuez, B |
Book Title | Verification and Evaluation of Computer and Communication Systems - 12th International Conference, VECoS 2018, Grenoble, France, September 26-28, 2018, Proceedings |
Series Title | Lecture Notes in Computer Science |
Volume | 11181 |
Pagination | 114–129 |
Publisher | Springer |
Abstract | Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system. Diagnosability describes the system property allowing one to determine with certainty whether a given fault has effectively occurred based on the available observations. However, this is a quite strong property that generally requires a high number of sensors. Consequently, it is not rare that developing a diagnosable system is too expensive. In this paper, we analyze a new discrete event system property called manifestability, that represents the weakest requirement on observations for having a chance to identify on line fault occurrences 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. Then, we prove that manifestability is a weaker property than diagnosability before proposing an algorithm with PSPACE complexity to automatically verify both properties. Furthermore, we 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. Finally, we compare our approach with related work. |
URL | https://doi.org/10.1007/978-3-030-00359-3_8 |
DOI | 10.1007/978-3-030-00359-3_8 |
PDF (Full text):