טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentHeyman Tamir
SubjectDistributed Symbolic Model Checking
DepartmentDepartment of Computer Science
Supervisors Professor Orna Grumberg
Professor Assaf Schuster


Abstract

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.