HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Abstract Interpretation of FIFO channels

Abstract : We address the analysis and the verification of communicating systems, which are systems built from sequential processes communicating via unbounded FIFO channels. We adopt the Abstract Interpretation approach to this problem, by defining approximate representations of sets of configuration of FIFO channels. In this paper we restrict our attention to the case where processes are finite-state processes and the alphabet of exchanged messages is finite. We first focus on systems with only one queue, for which we propose an abstract lattice based on regular languages, and we then generalize our proposal to systems with several queues. In particular, we define for these systems two abstract lattices, which are resp. non-relational and relational abstract lattices. We use those lattices for computing an over-approximation of the reachability set of a CFSM. Our experimental evaluation shows that, for some protocols, we obtain results that are as good as those obtained by exact methods founded on acceleration techniques.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 7:37:19 PM
Last modification on : Friday, February 4, 2022 - 3:16:12 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:42:02 PM


  • HAL Id : inria-00070237, version 1



Bertrand Jeannet, Thierry Jéron, Tristan Le Gall. Abstract Interpretation of FIFO channels. [Research Report] RR-5784, INRIA. 2005, pp.25. ⟨inria-00070237⟩



Record views


Files downloads