You are here:
| 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  [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 | |
| 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):
| ||||||||||||||
All documents in ORBi are protected by a user license.
