Symbolic guided search for CTL model checking

ABSTRACT

CTL model checking of complex systems often suffers from the state-explosion problem. We propose using Symbolic Guided Search to avoid difficult-to-represent sections of the state space and prevent state explosion from occurring. Symbolic Guided Search applies hints to guide the exploration of the state space. In this way, the size of the BDDs involved in the computation is controlled, and the truth of a property may be decided before all states have been explored. In this work, we show how hints can be used in the computation of nested fixpoints. We show how to use hints to obtain overapproximations useful for greatest fixpoints, and we present the first results for backward search. Our experiments demonstrate the effectiveness of our approach.

REFERENCES

• BCCZ99: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• BRS99: Roderick Bloem , Kavita Ravi , Fabio Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties, Proceedings of the 11th International Conference on Computer Aided Verification, p.222-235, July 06-10, 1999
• Bry86: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• CBM89: O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111-128, Leuven, Belgium, November 1989.
• CC77: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• CCLQ97: Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
• CE81: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• CGL92: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
• CHM+96: H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. IEEE Transactions on Computer-Aided Design, 15(12):1465-1478, December 1996.
• DK98: Jörg Desel , Ekkart Kindler, Proving Correctness of Distributed Algorithms Using High-Level Petri Nets - A Case Study, Proceedings of the 1998 International Conference on Application of Concurrency to System Design, p.177, March 23-26, 1998
• Eis99: Cindy Eisner, Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.97-109, September 27-29, 1999
• EL87: E. Allen Emerson , Chin-Laung Lei, Modalities for model checking: branching time logic strikes back, Science of Computer Programming, v.8 n.3, p.275-306, June 1, 1987 [doi>10.1016/0167-6423(87)90036-0]
• Eme90: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• EucBC: Euclid. Elements', Book 7, ca. 300 B.C. English edition: T.L. Heath, ed., The thirteen books of Euclid's Elements, Dover Publications, New York, 1956.
• INH96: Hiroaki Iwashita , Tsuneo Nakata , Fumiyasu Hirose, CTL model checking based on forward state traversal, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.82-87, November 10-14, 1996, San Jose, California, United States
• Jan99: Jae-Young Jang , Gary D. Hachtel, Iterative abstraction-based ctl model checking, 1999
• KMP98: Matt Kaufmann , Andrew Martin , Carl Pixley, Design Constraints in Symbolic Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.477-487, June 28-July 02, 1998
• Kur94: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• Kur97: R. P. Kurshan, Formal verification in a commercial setting, Proceedings of the 34th annual conference on Design automation, p.258-262, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266089]
• LPJ+96: Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
• McM94: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• NIJ+97: Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
• PH97: Abelardo Pardo , Gary D. Hachtel, Automatic Abstraction Techniques for Propositional µ-calculus Model Checking, Proceedings of the 9th International Conference on Computer Aided Verification, p.12-23, June 22-25, 1997
• Rav99: K. Ravi. Adaptive Techniques to Implvve State Space Search in Formal Verification. PhD thesis, University of Colorado, Department of Electrical and Computer Engineering, 1999.
• RS99a: Efficient Fixpoint Computation for Invariant Checking, Proceedings of the 1999 IEEE International Conference on Computer Design, p.467, October 10-13, 1999
• RS99b: Kavita Ravi , Fabio Somenzi, Hints to accelerate Symbolic Traversal, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.250-264, September 27-29, 1999
• SS94: Oleg Sokolsky , Scott A. Smolka, Incremental Model Checking in the Modal Mu-Calculus, Proceedings of the 6th International Conference on Computer Aided Verification, p.351-363, June 21-23, 1994
• Swa96: Gitanjali Meher Swamy , Robert K. Brayton, Incremental methods for formal verification and logic synthesis, 1996
• vL90: Jan van Leeuwen, Handbook of theoretical computer science (vol. A): algorithms and complexity, MIT Press, Cambridge, MA, 1991
• YD98: C. Han Yang , David L. Dill, Validation with guided search of the state space, Proceedings of the 35th annual conference on Design automation, p.599-604, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277201]

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Advanced technologies
  B.8 Performance and Reliability

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification