Advertisement

Scalable Distributed On-the-Fly Symbolic Model Checking

  • Shoham Ben-David
  • Tamir Heyman
  • Orna Grumberg
  • Assaf Schuster
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

This paper presents a scalable method for parallel symbolic on-the- fly model checking on a distributed-memory environment of workstations. Our method combines a parallel version of an on-the-fly model checker for safety properties with a scalable scheme for reachability analysis. The extra load of storage required for counter example generation is evenly distributed among the processes by our memory balancing. For the sake of scalability, at no point during computation the memory of a single process contains all the data from any of the cycles. The counter example generation is thus performed through collaboration of the parallel processes. We develop a method for the counter example generation keeping a low peak memory requirement during the backward step and the computation of the inverse transition relation. We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance SMV-based model checker. Our initial performance evaluation using 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 counter examples even when the model is too large to fit in the memory of the parallel system.

Keywords

Model Check Boolean Function Single Machine Regular Expression Transition Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    I. Beer, S. Ben-David, C. Eisner, and A. Landver. Rulebase: An Industry-Oriented Formal Verification Tool. In 33rd Design Automation Conference, pages 655–660, 1996.Google Scholar
  2. 2.
    I. Beer, S. Ben-David, and A. Landver. On-The-Fly Model Checking of RCTL Formulas. In Proc. of the 10th International Conference on Computer Aided Verification, LNCS 818, pages 184–194. Springer-Verlag, June–July 1998.Google Scholar
  3. 3.
    G. Bhat, R. Cleaveland, and O. Grumberg. Efficient On-The-Fly Model Checking for CTL*. In Proc. of the Conference on Logic in Computer Science (LICS’95), June 1995.Google Scholar
  4. 4.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.CrossRefGoogle Scholar
  5. 5.
    J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the 1991 International Conference on Very Large Scale Integration, August 1991. Winner of the SidneyMichaelson Best Paper Award.Google Scholar
  6. 6.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Gianpiero Cabodi, Paolo Camurati, and Stefano Que. Improved Reachability Analysis of Large FSM. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 354–360. IEEE Computer Society Press, June 1996.Google Scholar
  8. 8.
    E. Clarke, O. Grumberg, K. McMillan, and X. Zhao. Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. In 32rd Design Automation Conference, pages 655–660, 1995.Google Scholar
  9. 9.
    Olivier Coudert, Jean C. Madre, and Christian Berthet. Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams. In R. Kurshan and E. M. Clarke, editors, Workshop on Computer Aided Verification, DIMACS, LNCS 531, pages 23–32. Springer-Verlag, New Brunswick, NJ, June 1990.Google Scholar
  10. 10.
    C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.CrossRefGoogle Scholar
  11. 11.
    T. Heyman, D. Geist, O. Grumberg, and A. Schuster. Achieving scalability in parallel reachability analysis of very large circuits. In Proc. of the 12th International Conference on Computer Aided Verification. Springer-Verlag, June 2000.Google Scholar
  12. 12.
    J. E. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison Wesely Pub. Co, 1979.Google Scholar
  13. 13.
    D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon University, 1993.Google Scholar
  14. 14.
    K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.Google Scholar
  15. 15.
    Adrian A. Narayan, Jain J. Jawahar Isles, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. Reachability Analysis Using Partitioned-ROBDDs. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 388–393. IEEE Computer Society Press, June 1997.Google Scholar
  16. 16.
    Adrian A. Narayan, Jain Jawahar, M. Fujita, and A. Sangiovanni-Vincentelli. Partitioned-ROBDDs. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 547–554. IEEE Computer Society Press, June 1996.Google Scholar
  17. 17.
    Doron Peled. Combining Partial Order Reductions with On-The-Fly Model Checking. In Proc. of the Sixth International Conference on Computer Aided Verification, LNCS 818, pages 377–390. Springer-Verlag, June 1994.Google Scholar
  18. 18.
    Ulrich Stern and David L. Dill. Parallelizing the Murphy Verifier. In Proc. of the 9th International Conference on Computer Aided Verification, LNCS 1254, pages 256–267. Springer-Verlag, June 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Shoham Ben-David
    • 2
  • Tamir Heyman
    • 1
    • 2
  • Orna Grumberg
    • 1
  • Assaf Schuster
    • 1
  1. 1.TechnionComputer Science DepartmentHaifaIsrael
  2. 2.IBM Haifa Research LaboratoriesHaifaIsrael

Personalised recommendations