Reference : Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/74870
Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Godefroid, Patrice [ > > ]
1996
Lecture Notes in Computer Science
Springer
1102
1-12
Yes
No
International
0302-9743
1611-3349
Berlin
Germany
Computer Aided Verification, 8th International Conference (CAV '96)
New Brunswick, NJ
USA
[en] symbolic state-space exploration ; fifo channels ; QDDs
[en] We study the verification of properties of communication protocols
modeled by a finite set of finite-state machines that communicate by
exchanging messages via unbounded FIFO queues. It is well-known
that most interesting verification problems, such as deadlock detection,
are undecidable for this class of systems. However, in practice,
these verification problems may very well
turn out to be decidable for a subclass containing most "real"
protocols.

Motivated by this optimistic (and, we claim, realistic) observation,
we present an algorithm that may construct a finite and
exact representation of the state space of a communication
protocol, even if this state space is infinite. Our algorithm
performs a loop-first search in the state space of the protocol
being analyzed. A loop-first search is a search technique that
attempts to explore first the results of successive executions of
loops in the protocol description (code). A new data structure named
Queue-content Decision Diagram (QDD) is introduced for
representing (possibly infinite) sets of queue-contents. Operations
for manipulating QDDs during a loop-first search are presented.

A loop-first search using QDDs has been implemented, and experiments
on several existing communication protocols with infinite state spaces
have been performed. For these examples, our tool completed
its search, and produced a finite symbolic representation for these
infinite state spaces.
Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS, Bell Laboratories
Researchers
http://hdl.handle.net/2268/74870
10.1007/3-540-61474-5_53
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
BG96.pdfAuthor preprint230.31 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.