Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net UnfoldingsReportar como inadecuado




Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CONICET and Fa.M.A.F. - Universidad Nacional de Cordoba 2 Facultad de Ciencias de la Ingenierıa, Universidad Austral de Chile 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 4 LSV - Laboratoire Spécification et Vérification Cachan

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.

keyword : LTL-X parallel analysis verification Concurrency fault diagnosis diagnosability Petri nets





Autor: Laura Brandan-Briones - Agnes Madalinski - Hernán Ponce de León -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados