Skip to main content
SpringerLink
Log in

Model Checking: Historical Perspective and Example (Extended Abstract)

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,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.

This research is sponsored by the the Semiconductor Research Corporation (SRC) under Contract No. 97-DJ-294, the National Science Foundation (NSF) under Grant No. CCR-9505472, and the Defense Advanced Research Projects Agency (DARPA) under Contract No. DABT63-96-C-0071. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of SRC, NSF, DARPA, or the United States Government.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. 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. 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. 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. 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.

    Article  Google Scholar 

  6. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.

    Article  Google Scholar 

  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. 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. 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.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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.

    Article  MATH  Google Scholar 

  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. 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. 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. 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. 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. 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. 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. R. P. Kurshan and E. M. Clarke, editors. Proceedings of the 1990 Workshop on Computer-Aided Verification. Springer-Verlag, June 1990.

    Google Scholar 

  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. K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, 1992.

    Google Scholar 

  22. B. Mishra and E.M. Clarke. Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science, 38:269–291, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. 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. A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  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. A. P. Sistla and E.M. Clarke. Complexity of propositional temporal logics. Journal of the ACM, 32(3):733–749, July 1986.

    Article  MathSciNet  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University, USA

    Edmund M. Clarke & Sergey Berezin

Authors
  1. Edmund M. Clarke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sergey Berezin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE, Tilburg, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Clarke, E.M., Berezin, S. (1998). Model Checking: Historical Perspective and Example (Extended Abstract). In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-69778-0_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64406-4

  • Online ISBN: 978-3-540-69778-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation