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