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 : We present a framework that shows how components in parallel can infer the diagnosability property of the complete system (distributed and with multiple faults) from the diagnosability verification of each component synchronizing with a fault free versions of the other ones. Furthermore, we use existing efficient methods and tools, in particular parallel model checking based on Petri net unfoldings, to verifier diagnosability of such components.
https://hal.inria.fr/hal-00915478
Contributeur : Hernan Ponce de Leon
<>
Soumis le : lundi 15 décembre 2014 - 14:23:42
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37
Document(s) archivé(s) le : samedi 15 avril 2017 - 04:32:18
Laura Brandan-Briones, Agnes Madalinski, Hernán Ponce de León. Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings. Workshop on Principles of Diagnosis, Sep 2014, Graz, Austria. 2013. 〈hal-00915478v2〉
