Advertisement

Model Checking: Historical Perspective and Example (Extended Abstract)

  • Edmund M. Clarke
  • Sergey Berezin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)

Abstract

Model checking is an automatic verification technique for finite state concurrent systems such as sequential circuit designs and communication protocols. Specifications are expressed in propositional temporal logic. An exhaustive search of the global state transition graph or system model is used to determine if the specification is true or not. If the specification is not satisfied, a counterexample execution trace is generated if possible. By encoding the model using Binary Decision Diagrams (BDDs) it is possible to search extremely large state spaces with as many as 10120 reachable states. In this paper we describe the theory underlying this technique and outline its historical development. We demonstrate the power of model checking to find subtle errors by verifying the Space Shuttle Three-Engines-Out Contingency Guidance Protocol.

Keywords

Model Check Temporal Logic Linear Temporal Logic Space Shuttle Concurrent System 
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.
    S. Bose and A. L. Fisher. Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic. In L. Claesen, editor, Proceedings of the IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, November 1989.Google Scholar
  2. 2.
    M. C. Browne and E. M. Clarke. Sml: A high level language for the design and verification of finite state machines. In IFIP WG 10.2 International Working Conference from HDL Descriptions to Guaranteed Correct Circuit Designs, Grenoble, France. IFIP, September 1986.Google Scholar
  3. 3.
    M. C. Browne, E. M. Clarke, and D. Dill. Checking the correctness of sequential circuits. In Proceedings of the 1985 International Conference on Computer Design, Port Chester, New York, October 1985. IEEE.Google Scholar
  4. 4.
    M. C. Browne, E. M. Clarke, and D. Dill. Automatic circuit verification using temporal logic: Two new examples. In Formal Aspects of VLSI Design. Elsevier Science Publishers (North Holland), 1986.Google Scholar
  5. 5.
    M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035–1044, December 1986.CrossRefGoogle Scholar
  6. 6.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.CrossRefGoogle Scholar
  7. 7.
    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 Sidney Michaelson Best Paper Award.Google Scholar
  8. 8.
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proceedings of the 27th ACM/IEEE Design Automation Conference, pages 46–51. IEEE Computer Society Press, June 1990.Google Scholar
  9. 9.
    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
  10. 10.
    E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In D. Kozen, editor, Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981.Google Scholar
  11. 11.
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.zbMATHCrossRefGoogle Scholar
  12. 12.
    O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989.Google Scholar
  13. 13.
    O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In E. M. Clarke, editors. Proceedings of the 1990 Workshop on computer-Aided Verification. Springer-Verlag, June 1990 Kurshan and Clarke [19].Google Scholar
  14. 14.
    Judith Crow. Finite-state analysis of space shuttle contingency guidance requirements. Technical Report NASA Contractor Report 4741, SRI International, Menlo Park, CA, May 1996.Google Scholar
  15. 15.
    D. L. Dill and E. M. Clarke. Automatic verification of asynchronous circuits using temporal logic. IEE Proceedings, Part E 133(5), 1986.Google Scholar
  16. 16.
    E.A. Emerson and Chin Laung Lei. Modalities for model checking: Branching time strikes back. Twelfth Symposium on Principles of Programming Languages, New Orleans, La., January 1985.Google Scholar
  17. 17.
    Z. Har’El and R. P. Kurshan. Software for analytical development of communications protocols. AT&T Technical Journal, 69(1):45–59, Jan.–Feb. 1990.Google Scholar
  18. 18.
    R. P. Kurshan. Analysis of discrete event coordination. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 414–453. Springer-Verlag, May 1989.Google Scholar
  19. 19.
    R. P. Kurshan and E. M. Clarke, editors. Proceedings of the 1990 Workshop on Computer-Aided Verification. Springer-Verlag, June 1990.Google Scholar
  20. 20.
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97–107. Association for Computing Machinery, January 1985.Google Scholar
  21. 21.
    K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, 1992.Google Scholar
  22. 22.
    B. Mishra and E.M. Clarke. Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science, 38:269–291, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    C. Pixley. A computational theory and implementation of sequential hardware equivalence. In R. Kurshan and E. Clarke, editors, Proc. CAV Workshop (also DIMACS Tech. Report 90-31), Rutgers University, NJ, June 1990.Google Scholar
  24. 24.
    C. Pixley, G. Beihl, and E. Pacas-Skewes. Automatic derivation of FSM specification to implementation encoding. In Proceedings of the International Conference on Computer Desgin, pages 245–249, Cambridge, MA, October 1991.Google Scholar
  25. 25.
    C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the 29th Design Automation Conference, pages 620–623, June 1992.Google Scholar
  26. 26.
    A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium in Programming, 1982.Google Scholar
  28. 28.
    A. P. Sistla and E.M. Clarke. Complexity of propositional temporal logics. Journal of the ACM, 32(3):733–749, July 1986.CrossRefMathSciNetGoogle Scholar
  29. 29.
    M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Edmund M. Clarke
    • 1
  • Sergey Berezin
    • 1
  1. 1.Carnegie Mellon UniversityUSA

Personalised recommendations