Back to Search
Start Over
Scalable distributed on-the-fly symbolic model checking.
- Source :
- International Journal on Software Tools for Technology Transfer; Aug2003, Vol. 4 Issue 4, p496-504, 9p
- Publication Year :
- 2003
-
Abstract
- 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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 14332779
- Volume :
- 4
- Issue :
- 4
- Database :
- Complementary Index
- Journal :
- International Journal on Software Tools for Technology Transfer
- Publication Type :
- Academic Journal
- Accession number :
- 15179441
- Full Text :
- https://doi.org/10.1007/s10009-002-0093-2