-
Selection by year
-
Selection by authors
-
Complete lists
RRanalysisFIFO
B. Jeannet, T. Jéron, T. Le Gall. Abstract lattices for the analysis of systems with unbounded FIFO channels. Research Report IRISA, No 1767, December 2005.
Download [help]
Download paper: Postscript ( )
Copyright notice:
This material is presented to ensure timely dissemination of scholarly and
technical work. Copyright and all rights therein are retained by authors or
by other copyright holders. All persons copying this information are expected
to adhere to the terms and constraints invoked by each author's
copyright. These works may not be reposted without the explicit permission of
the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic
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
Contact
Thierry Jéron http://www.irisa.fr/prive/jeron
BibTex Reference
@TechReport{RRanalysisFIFO,
Author = {Jeannet, B. and Jéron, T. and Le Gall, T.},
Title = {Abstract lattices for the analysis of systems with unbounded {FIFO} channels},
Number = {1767},
Institution = {IRISA},
Month = {December},
Year = {2005}
}
EndNote Reference [help]
Get EndNote Reference (.ref)