publication . Part of book or chapter of book . Article . Conference object . 1996

Extended abstract

Boigelot, Bernard; Godefroid, Patrice;
Open Access
  • Published: 01 Jan 1996
  • Publisher: Springer Berlin Heidelberg
  • Country: Belgium
Abstract
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 spa...
Subjects
free text keywords: symbolic verification, fifo channels, QDDs, : Computer science [Engineering, computing & technology], : Sciences informatiques [Ingénierie, informatique & technologie], symbolic state-space exploration
Related Organizations
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue