Effective Verification of Weak Diagnosability

Anoopam Agarwal 1 Agnes Madalinski 2 Stefan Haar 3, 4
4 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : The diagnosability problem can be stated as follows: does a given labeled Discrete Event System allow for an outside observer to determine the occurrence of the "invisible" fault, no later than a bounded number of events after that unobservable occurrence, and based on the partial observation of the behaviour? When this problem is investigated in the context of concurrent systems, partial order semantics induces a separation between classical or strong diagnosability on the one hand, and weak diagnosability on the other hand. The present paper presents the first solution for checking weak diagnosability, via a verifier construction.
Type de document :
Communication dans un congrès
Proceedings of the 8th IFAC Symposium on Fault Detection, Supervision and Safety for Technical Processes (SAFEPROCESS'12), 2012, Mexico City, Mexico. IFAC, 2012, 〈10.3182/20120829-3-MX-2028.00083〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776774
Contributeur : Benedikt Bollig <>
Soumis le : mercredi 16 janvier 2013 - 10:56:52
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

Collections

Citation

Anoopam Agarwal, Agnes Madalinski, Stefan Haar. Effective Verification of Weak Diagnosability. Proceedings of the 8th IFAC Symposium on Fault Detection, Supervision and Safety for Technical Processes (SAFEPROCESS'12), 2012, Mexico City, Mexico. IFAC, 2012, 〈10.3182/20120829-3-MX-2028.00083〉. 〈hal-00776774〉

Partager

Métriques

Consultations de la notice

288