Incremental CTL model checking using BDD subsetting

ABSTRACT

An automatic abstraction/refinement algorithm for symbolic CTL model checking is presented. Conservative model checking is thus done for the full CTL language-no restriction is made to the universal or existen tial fragments. The algorithm begins with conserv ativ everification of an initial abstraction. If the conclusion is negativ e,it deriv es a “goal set” of states which require further resolution. It then successiv ely refines, with respect to this goal set, the appro ximations made in the sub-formulas, until the giv en form ula is v erified or computational resources are exhausted. This method applies uniformly to the abstractions based in over-appro ximation as well as under-approximations of the model. Both the refinement and the abstraction procedures are based in BDD-subsetting. Note that refinement procedures which are based on error traces, are limited to over-appro ximation on the universal fragment (or for language con tainment), whereas the goal set method is applicable to all consisten t appro ximations, and for all CTL formulas.

REFERENCES

• 1: Felice Balarin , Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment, Proceedings of the 5th International Conference on Computer Aided Verification, p.29-40, June 28-July 01, 1993
• 2: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 3: 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]
• 4: J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
• 5: Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Bernard Plessier , Fabio Somenzi, Algorithms for approximate FSM traversal, Proceedings of the 30th international conference on Design automation, p.25-30, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164555]
• 6: 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
• 7: P. Kelb, D. Dams, and R. Gerth. Practical symbolic model checking of the full p-calculus using compositional abstractions. Technical Report 95-31, Department of Computing Science, Eindhoven University of Technology, 1995.
• 8: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 9: 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]
• 10: 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
• 11: Thomas Lindner. Case Study "Production Cell": A Comparative Study in Formal Software Development, chapter 2, pages 9,21. FZI, 1994.
• 12: David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
• 13: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 14: 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
• 15: Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  J. Computer Applications

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

Keywords:
ISM frequency band, RF CMOS, digital radio, spread spectrum communication, transceiver