Giuseppe Della Penna :: Website @ UnivAQ

State Space Exploration (*Reachability Analysis*) is at the very heart
of all algorithms for automatic verification of concurrent systems. As well
known, the main obstruction to automatic verification of *Finite State Systems*
is the huge amount of memory required to complete state space exploration (*state
explosion*).

In general, two kinds of approaches have been studied to counteract state explosion:

- In a
**memory saving**approach one essentially tries to reduce the amount of memory needed to represent the set of visited states. - In an
**auxiliary storage**approach one tries to exploit disk storage as well as distributed processors (network storage) to enlarge the available memory (and CPU).

Moreover, there are two state exploration techniques used in verification software:

**symbolic state space exploration**(i.e. OBDD based). This technique is mainly used to verify the design of sequential logic nets, i.e. integrated circuits microcode and similar software.**explicit state space exploration**. This technique often outperforms symbolic exploration in the verification of protocols or similar software.

In our reseach, we showed experimentally that **certain software, in
particular protocols, exhibit transition locality**. That is, w.r.t.
levels of a Breadth First (BF) visit, state transitions tend to be between
states belonging to close levels of the transition graph.

To exploit this property, we developed two new explicit state space exploration algorithms that enhance the standard BF explicit state space exploration, trading space with time.

Our first enhanced BF visit algorithm is the **Cache Based Breadth First
Search** (CBBFS). Essentially, it replaces the hash table used in a BF state
exploration with a *cache memory* (i.e. visited states may be forgotten)
and uses disk storage for the BF queue.

We implemented the CBBFS on the Murphi verifier from Stanford University. The implementation is compatible with all the common state reduction techniques used by Murphi. The algorithm has been included in the last official release of the verifier. We are currently working on the integration of our algorithm in SPIN.

We experimented our approach in situations where the conventional explicit state space exploration would go out of memory, and successfully completed many verifications. In particular, our results show that CBBFS can save more than 40% of memory with an average time penality of 50%.

The first results obtained in the CBBFS experimentation using Murphi have been presented during CHARME 2001.

The second enhanced BF visit algorithm is the **Disk Based Breadth First
Search** (DBBFS). Essentially, it uses disk storage to save memory during the
exploration. Exploiting locality, we are able to access disk without the big
time penalities that affect other disk-based exploration algorithms.

We implemented also the DBBFS on the Murphi
verifier and experimented it in situations where the available memory was
very low w.r.t the protocol size. Our results
show that DBBFS ensures termination in any memory condition, with a time penalty
that degrades very well as the available memory runs out. In particular, we
verified protocols using 10% of the memory that would be required by the
standard RAM-based algorithm, and even in this extreme situation our DBBFS was
only 3 times slower (on average) than the RAM-based Murphi. We also used DBBFS
on a protocol with 10^{9} states that would require 5 gigabytes of RAM
to be verified and completed the verification using only 250 megabytes.

The first results obtained in the CBBFS experimentation have been presented during FMCAD 2002.

The DBBFS algorithm, as well as the CBBFS algorithm, is now part of the CMurphi verifier.