Shoham Ben-David, Dana Fisman, et al.
Theoretical Computer Science
This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. The extra memory requirement for counterexample generation is evenly distributed among the processes by a memory balancing procedure. At no point during computation does the memory of a single process contain all the data. This enhances scalability. Collaboration between the parallel processes during counterexample generation reduces memory utilization for the backward step. We implemented our method on a standard, loosely- connected environment of workstations, using a high-performance model checker. Our initial performance evaluation, carried out on several large circuits, shows that our method can check models that are too large to fit in the memory of a single node. Our on-the-fly approach may find counterexamples even when the model is too large to fit in the memory of the parallel system. © 2002 Springer-Verlag.
Shoham Ben-David, Dana Fisman, et al.
Theoretical Computer Science
Yael Abarbanel-Vinov, Neta Aizenbud-Reshef, et al.
Formal Methods in System Design
Shoham Ben-David, Anna Gringauze, et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Tamir Heyman, Danny Geist, et al.
Formal Methods in System Design