T. Legall, B. Jeannet, T. Jéron. Verification of Communication Protocols Using Abstract Interpretation of FIFO queues. In Algebraic Methodology and Software Technology, AMAST '06, LNCS, Volume 4019, July 2006.
Download paper:
Adobe portable document (pdf)
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.
We address the verification of communication protocols or distributed systems that can be modeled by Communicating Finite-State Machines(CFSMs), i.e. a set of sequential machines communicating via unbounded FIFO channels. Unlike most related works based on acceleration techniques, we propose to apply the Abstract Interpretation approach to such systems, which consists in using approximated representations of sets of configurations. We show that the use of regular languages together with an extrapolation operator provides a simple and elegant method for the analysis of CFSMs, which is moreover often as accurate as related works, and in some cases more expressive. Last, when the system has several queues, our method can be implemented both as an attribute-independend analysis or as a more precise (but also more costly) attribute-dependent analysis
Bertrand Jeannet http://pop-art.inrialpes.fr/people/bjeannet/
@InProceedings{LJJ06,
Author = {Legall, T. and Jeannet, B. and Jéron, T.},
Title = {Verification of Communication Protocols Using Abstract Interpretation of {FIFO} queues},
BookTitle = {Algebraic Methodology and Software Technology, AMAST '06},
Volume = {4019},
Series = {LNCS},
Month = {July},
Year = {2006}
}
Get EndNote Reference (.ref)