Ph.D Student | Heyman Tamir |
---|---|

Subject | Distributed Symbolic Model Checking |

Department | Department of Computer Science |

Supervisors | Professor Orna Grumberg |

Professor Assaf Schuster |

This work presents a scalable method for parallelizing symbolic reachability analysis on a distributed memory environment of workstations. We have developed an adaptive partitioning algorithm that significantly reduces space requirements. A compact BDD representation allows coordination by shipping BDDs from one machine to another. This representation allows for different variable orders in the sending and receiving processes. The algorithm uses a distributed termination protocol, with none of the memory modules preserving a complete image of the set of reachable states. No external storage is used on the disk. Rather, we make use of the network, which is much faster.

In order to implement the algorithm we had to develop the
Division system. It is a generic distributed system for research on distributed
model checking. Division enables the development of a novel distributed
symbolic algorithm for reachability analysis that can effectively exploit, ``as
needed'', a large number of machines working in parallel. The novelty of the
algorithm is in its dynamic allocation and reallocation of processes to tasks
and in its mechanism for recovery, from local state explosion. As a result, the
algorithm is **work efficient**: it utilizes only those resources that are
actually needed.

We combine our scheme with a scheme for on-the-fly model checking for safety properties. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. We further propose a distributed symbolic algorithm for model checking of propositional mu-calculus formulas. mu-calculus is a powerful formalism and mu-calculus model checking can solve many problems, including, for example, verification of (fair) CTL and LTL properties. Thus, significantly extends the scope of properties that can be verified distributively, enabling us to specify sophisticated properties for very large designs.