Stability of Asynchronously Communicating Systems

Gwen Salaün 1, * Lina Ye 1, *
* Auteur correspondant
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Recent software is mostly constructed by reusing and composing existing components. Software components are usually stateful and therefore described using behavioral models such as finite state machines. Asynchronous communication is a classic interaction mechanism used for such software systems. However, analysing communicating systems interacting 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 buffer sizes. In this paper, we focus on infinite systems and we do not restrict the system by imposing any arbitrary bounds. 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 us 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 show how we succeed in computing these bounds for many typical examples using heuristics and equivalence checking.
Type de document :
[Research Report] RR-8561, INRIA. 2014
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger
Contributeur : Gwen Salaün <>
Soumis le : lundi 20 octobre 2014 - 09:38:28
Dernière modification le : samedi 15 décembre 2018 - 01:49:38
Document(s) archivé(s) le : mercredi 21 janvier 2015 - 10:26:33


RR-8561 (1).pdf
Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01020777, version 2



Gwen Salaün, Lina Ye. Stability of Asynchronously Communicating Systems. [Research Report] RR-8561, INRIA. 2014. 〈hal-01020777v2〉



Consultations de la notice


Téléchargements de fichiers