Automated Analysis of Asynchronously Communicating Systems

Abstract : Analyzing systems communicating asynchronously via reliable FIFO buffers is an undecidable problem. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing the buffer size. In this paper, our focus is on systems that are likely to be unbounded and therefore result in infinite systems. We do not want to restrict the system by imposing any arbitrary bound. We introduce a notion of stability and prove that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables one to check certain properties on the system for that bound and to ensure that the system will preserve them whatever larger bounds are used for buffers. We also prove that computing this bound is undecidable but we show how we succeed in computing these bounds for many examples using heuristics and equivalence checking.
Type de document :
Communication dans un congrès
23rd International SPIN symposium on Model Checking of Software, Apr 2016, Eindhoven, Netherlands. Springer Verlag, 2016, SPIN'2016. 〈http://www.spin2016.info/〉. 〈10.1007/978-3-319-32582-8_1〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01280164
Contributeur : Radu Mateescu <>
Soumis le : lundi 9 mai 2016 - 15:52:26
Dernière modification le : mercredi 11 avril 2018 - 01:57:28
Document(s) archivé(s) le : mardi 15 novembre 2016 - 23:50:02

Fichier

Akroun-Salaun-Ye-16.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Lakhdar Akroun, Gwen Salaün, Lina Ye. Automated Analysis of Asynchronously Communicating Systems. 23rd International SPIN symposium on Model Checking of Software, Apr 2016, Eindhoven, Netherlands. Springer Verlag, 2016, SPIN'2016. 〈http://www.spin2016.info/〉. 〈10.1007/978-3-319-32582-8_1〉. 〈hal-01280164〉

Partager

Métriques

Consultations de la notice

808

Téléchargements de fichiers

131