Paper Info
Title
Verification of communication protocols using abstract interpretation of FIFO queues
Abstract
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 recent 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 acceleration techniques, and in some cases more expressive. Last, when the system has several queues, our method can be implemented either as an attribute-independent analysis or as a more precise (but also more costly) attribute-dependent analysis.
Year
DOI
Venue
2006
10.1007/11784180_17
AMAST
Keywords
Field
DocType
recent related work,elegant method,communication protocol,abstract interpretation,fifo queue,attribute-dependent analysis,acceleration technique,abstract interpretation approach,communicating finite state machines,approximated representation,attribute-independent analysis,extrapolation operator,distributed system,regular language,dependence analysis
FIFO (computing and electronics),Abstract interpretation,Computer science,Queue,Communication channel,Finite-state machine,Theoretical computer science,Operator (computer programming),Regular language,Communications protocol
Conference
Volume
ISSN
ISBN
4019
0302-9743
3-540-35633-9
Citations 
PageRank 
References 
13
0.67
28
Authors
3
Name
Order
Citations
PageRank
Tristan Le Gall1556.89
Bertrand Jeannet264129.06
Thierry Jéron3105391.06