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.
Origine : Fichiers produits par l'(les) auteur(s)