Automated verification of automata communicating via FIFO and bag buffers - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Formal Methods in System Design Année : 2018

Automated verification of automata communicating via FIFO and bag buffers

Lakhdar Akroun
Gwen Salaün
  • Fonction : Auteur
  • PersonId : 880331

Résumé

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.
Fichier principal
Vignette du fichier
main-fmsd.pdf (413.92 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01898159 , version 1 (18-10-2018)

Identifiants

Citer

Lakhdar Akroun, Gwen Salaün. Automated verification of automata communicating via FIFO and bag buffers. Formal Methods in System Design, 2018, 52 (3), pp.260 - 276. ⟨10.1007/s10703-017-0285-8⟩. ⟨hal-01898159⟩
114 Consultations
257 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More