Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2013

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

Résumé

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.
Fichier principal
Vignette du fichier
paper.pdf (162.43 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00915478 , version 1 (08-12-2013)
hal-00915478 , version 2 (15-12-2014)

Identifiants

  • HAL Id : hal-00915478 , version 1

Citer

Laura Brandan-Briones, Agnes Madalinski, Hernán Ponce de León. Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings. [Research Report] 2013. ⟨hal-00915478v1⟩
157 Consultations
173 Téléchargements

Partager

Gmail Facebook X LinkedIn More