Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 6:08:43 PM
Last modification on : Thursday, February 11, 2021 - 2:48:03 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 10:56:04 PM


  • 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⟩



Record views


Files downloads