Model Checking Distributed Systems against Temporal-Epistemic Specifications

Abstract : Concurrency and message reordering are two main causes for the state-explosion in distributed systems with asynchronous communication. We study this domain by analysing ABS, an executable modelling language for object-based distributed systems and present a symbolic model checking methodology for verifying ABS programs against temporal-epistemic specifications. Specifically, we show how to map an ABS program into an ISPL program for verification with MCMAS, a model checker for multi-agent systems. We present a compiler implementing the formal map, exemplify the methodology on a mesh network use case and report experimental results.
Type de document :
Communication dans un congrès
Dirk Beyer; Michele Boreale. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.130-145, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_10〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01515241
Contributeur : Hal Ifip <>
Soumis le : jeudi 27 avril 2017 - 10:46:46
Dernière modification le : jeudi 27 avril 2017 - 14:43:59
Document(s) archivé(s) le : vendredi 28 juillet 2017 - 12:45:20

Fichier

978-3-642-38592-6_10_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Andreas Griesmayer, Alessio Lomuscio. Model Checking Distributed Systems against Temporal-Epistemic Specifications. Dirk Beyer; Michele Boreale. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.130-145, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_10〉. 〈hal-01515241〉

Partager

Métriques

Consultations de la notice

35

Téléchargements de fichiers

18