Automated verification of automata communicating via FIFO and bag buffers

Lakhdar Akroun 1 Gwen Salaün 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This article presents new results for the automated verification of automata communicating asynchronously via FIFO or bag buffers. The analysis of such systems is possible by comparing bounded asynchronous compositions using equivalence checking. When the composition exhibits the same behavior for a specific buffer bound, the behavior remains the same for larger bounds. This enables one to check temporal properties on the system for that bound and this ensures that the system will preserve them whatever larger bounds are used for buffers. In this article, we present several decidability results and a semi-algorithm for this problem considering FIFO and bag buffers, respectively, as communication model. We also study various equivalence notions used for comparing the bounded asynchronous systems.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2018, 52 (3), pp.260 - 276. 〈10.1007/s10703-017-0285-8〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01898159
Contributeur : Radu Mateescu <>
Soumis le : jeudi 18 octobre 2018 - 10:01:57
Dernière modification le : samedi 15 décembre 2018 - 01:50:11

Fichier

main-fmsd.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Lakhdar Akroun, Gwen Salaün. Automated verification of automata communicating via FIFO and bag buffers. Formal Methods in System Design, Springer Verlag, 2018, 52 (3), pp.260 - 276. 〈10.1007/s10703-017-0285-8〉. 〈hal-01898159〉

Partager

Métriques

Consultations de la notice

56

Téléchargements de fichiers

18