Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs

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 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.