Testing for the unboundedness of fifo channels in programs (1)

Thierry Jéron 1
1 ADP - Distributed Algorithms and Protocols
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : Unsolvability of the unboundedness problem for specification models allowing fifo channels was proved a few years ago by Brand and Zafiropulo. The paper investigates a testing approach of that problem. Instead of reducing the model in order to give decidability results, we work with the largest possible framework. We find a sufficient condition for unboundedness based on a relation between reachable global states. This gives a testing procedure which can be applied as well to communicating finite state machines as to Fifo-Nets. Moreover, the test extends existing decidability results. In fact it becomes a decision procedure for a class of systems strictly including linear and monogeneous systems. A few modifications of the relation make it available for Estelle specifications.
Type de document :
[Research Report] RR-1159, INRIA. 1990
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 18:08:43
Dernière modification le : vendredi 16 novembre 2018 - 01:29:40
Document(s) archivé(s) le : mardi 12 avril 2011 - 22:56:04



  • HAL Id : inria-00075399, version 1


Thierry Jéron. Testing for the unboundedness of fifo channels in programs (1). [Research Report] RR-1159, INRIA. 1990. 〈inria-00075399〉



Consultations de la notice


Téléchargements de fichiers