Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings

Laura Brandan-Briones 1 Agnes Madalinski 2 Hernán Ponce de León 3, 4
3 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 : 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.
Type de document :
Poster
Workshop on Principles of Diagnosis, Sep 2014, Graz, Austria. 2013
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

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

Fichier

dx-2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00915478, version 2

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

227

Téléchargements de fichiers

125