Advertisement

Introduction to Model Checking

  • Edmund M. Clarke
  • Thomas A. Henzinger
  • Helmut Veith
Chapter

Abstract

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. This chapter is an introduction and short survey of model checking. The chapter aims to motivate and link the individual chapters of the handbook, and to provide context for readers who are not familiar with model checking.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Akbarpour, B., Abdel-Hamid, A.T., Tahar, S., Harrison, J.: Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput. J. 53(4), 465–488 (2010) CrossRefGoogle Scholar
  2. 2.
    Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985) MathSciNetCrossRefGoogle Scholar
  3. 3.
    Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015) Google Scholar
  4. 4.
    Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Jobstmann, B., Ray, S. (eds.) Proceedings, Formal Methods in Computer-Aided Design, FMCAD, Portland, OR, USA, October 20–23, 2013, pp. 1–8. IEEE, Piscataway (2013) Google Scholar
  5. 5.
    Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000) CrossRefGoogle Scholar
  6. 6.
    Appel, A.W.: Modern Compiler Implementation in C. Cambridge University Press, Cambridge (1998) zbMATHGoogle Scholar
  7. 7.
    Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  8. 8.
    Baier, C., Katoen, J-P.: Principles of Model Checking. MIT Press, Cambridge (2008) zbMATHGoogle Scholar
  9. 9.
    Baresi, L., Di Nitto, E.: Test and Analysis of Web Services. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  10. 10.
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) Proceedings, Computer Aided Verification, CAV, Haifa, Israel, June 22–25, 1997. LNCS, vol. 1254, pp. 279–290. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  11. 11.
    Ben-Ari, M.: Principles of the SPIN Model Checker. Springer, Heidelberg (2008) zbMATHGoogle Scholar
  12. 12.
    Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  13. 13.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  14. 14.
    Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) Proceedings, Tools and Algorithms for the Construction and Analysis of Systems, TACAS, London, UK, April 11–18, 2015. LNCS, vol. 9035, pp. S33–S48. Springer, Heidelberg (2015) Google Scholar
  15. 15.
    Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Log. 15(4), 27:1–27:25 (2014) MathSciNetCrossRefGoogle Scholar
  16. 16.
    Bortolussi, L., Milios, D., Sanguinetti, G.: Machine-learning methods in statistical model checking and system design. In: Proceedings, Runtime Verification, RV, Vienna, Austria, September 22–25, 2015. LNCS, vol. 9333, pp. 323–341. Springer, Heidelberg (2015) CrossRefGoogle Scholar
  17. 17.
    Canini, M., Venzano, D., Perešíni, P., Kostić, D., Rexford, J.: A NICE way to test openflow applications. In: Gribble, S.D., Katabi, D. (eds.) Proceedings, Networked Systems Design and Implementation, NSDI, San Jose, CA, USA, April 25–27, 2012, pp. 127–140. USENIX Association, Berkeley (2012) Google Scholar
  18. 18.
    Cassandras, C.G., Lafortune, S.: Introduction to Discrete-Event Systems, 2nd edn. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  19. 19.
    Cerný, P., Clarke, E.M., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Samanta, R., Tarrach, T.: From non-preemptive to preemptive scheduling using synchronization synthesis. In: Kroening, D., Pasareanu, C.S. (eds.) Proceedings, Computer Aided Verification, CAV, Part II, San Francisco, CA, USA, July 18–24, 2015. LNCS, vol. 9207, pp. 180–197. Springer, Heidelberg (2015) CrossRefGoogle Scholar
  20. 20.
    Cerný, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21–35 (2012) MathSciNetCrossRefGoogle Scholar
  21. 21.
    Cerný, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: Giacobazzi, R., Cousot, R. (eds.) Proceedings, Principles of Programming Languages, POPL, Rome, Italy, January 23–25, 2013, pp. 115–128. ACM, New York (2013) Google Scholar
  22. 22.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Proceedings, Logics of Programs, Yorktown Heights, NY, USA, May 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981) CrossRefGoogle Scholar
  23. 23.
    Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2009) CrossRefGoogle Scholar
  24. 24.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Proceedings, Principles of Programming Languages, POPL, Austin, TX, USA, January 1983, pp. 117–126. ACM, New York (1983) Google Scholar
  25. 25.
    Clarke, E.M., Fehnker, A., Jha, S.K., Veith, H.: Temporal-logic model checking. In: Hristu-Varsakelis, D., Levine, W.S. (eds.) Handbook of Networked and Embedded Control Systems, pp. 539–558. Birkhäuser, Basel (2005) CrossRefGoogle Scholar
  26. 26.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) Google Scholar
  27. 27.
    Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings, Logic in Computer Science, LICS, Copenhagen, Denmark, July 22–25 July 2002, pp. 19–29. IEEE, Piscataway (2002) Google Scholar
  28. 28.
    Clarke, E.M., Schlingloff, B.-H.: Model checking. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1635–1790. Elsevier/MIT Press, Amsterdam/Cambridge (2001) CrossRefGoogle Scholar
  29. 29.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Principles of Programming Languages, POPL, Los Angeles, CA, USA, January 1977, pp. 238–252. ACM, New York (1977) Google Scholar
  30. 30.
    Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45–80 (2001) CrossRefGoogle Scholar
  31. 31.
    Desai, A., Gupta, V., Jackson, E.K., Qadeer, S., Rajamani, S.K., Zufferey, D.: P: safe asynchronous event-driven programming. In: Boehm, H-J., Flanagan, C. (eds.) Proceedings, Programming Language Design and Implementation, PLDI, Seattle, WA, USA, June 16–19, 2013, pp. 321–332. ACM, New York (2013) Google Scholar
  32. 32.
    Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859–866 (1972) CrossRefGoogle Scholar
  33. 33.
    Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995–1072. MIT Press, Cambridge (1990) Google Scholar
  34. 34.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear-time temporal logic. J. ACM 33(1), 151–178 (1986) MathSciNetCrossRefGoogle Scholar
  35. 35.
    Fisher, J., Harel, D., Henzinger, T.A.: Biology as reactivity. Commun. ACM 54(10), 72–82 (2011) CrossRefGoogle Scholar
  36. 36.
    Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings, Mathematical Aspects of Computer Science: American Mathematical Society Symposia, Providence, RI, USA, vol. 19, pp. 19–31. AMS, Providence (1967) CrossRefGoogle Scholar
  37. 37.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) Proceedings, Programming Language Design and Implementation, PLDI, Chicago, IL, USA, June 12–15, 2005, pp. 213–223. ACM, New York (2005) Google Scholar
  38. 38.
    Grumberg, O., Veith, H.: 25 Years of Model Checking: History, Achievements, Perspectives. LNCS, vol. 5000. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  39. 39.
    Gulwani, S., Hernández-Orallo, J., Kitzelmann, E., Muggleton, S.H., Schmid, U., Zorn, B.G.: Inductive Programming meets the real world. Commun. ACM 58(11), 90–99 (2015) CrossRefGoogle Scholar
  40. 40.
    Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. CoRR (2015). arXiv:1501.02155 [abs]
  41. 41.
    Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987) MathSciNetCrossRefGoogle Scholar
  42. 42.
    Harel, D., Marelly, R.: Come, Let’s Play. Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003) Google Scholar
  43. 43.
    Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci. Res. Dev. 28(4), 331–344 (2013) CrossRefGoogle Scholar
  44. 44.
    Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D’Argenio, P.R., Melgratti, H.C. (eds.) Proceedings, Concurrency Theory, CONCUR, Buenos Aires, Argentina, August 27–30, 2013. LNCS, vol. 8052, pp. 273–287. Springer, Heidelberg (2013) Google Scholar
  45. 45.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) CrossRefGoogle Scholar
  46. 46.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, New York (1995) Google Scholar
  47. 47.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004) Google Scholar
  48. 48.
    Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-Based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2007) CrossRefGoogle Scholar
  49. 49.
    Karamanolis, C.T., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model checking of workflow schemas. In: Proceedings, Enterprise Distributed Object Computing, EDOC, Makuhari, Japan, September 25–28, 2000, pp. 170–181. IEEE, Piscataway (2000) Google Scholar
  50. 50.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976) MathSciNetCrossRefGoogle Scholar
  51. 51.
    Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS micro-kernel. ACM Trans. Comput. Syst. 32(1), 2 (2014) CrossRefGoogle Scholar
  52. 52.
    Kozen, D.: Results on the propositional \(\mu\)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983) MathSciNetCrossRefGoogle Scholar
  53. 53.
    Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1–14 (1959) MathSciNetCrossRefGoogle Scholar
  54. 54.
    Kropf, T.: Introduction to Formal Hardware Verification. Springer, Heidelberg (1999) CrossRefGoogle Scholar
  55. 55.
    Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994) zbMATHGoogle Scholar
  56. 56.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 2, 125–143 (1977) MathSciNetCrossRefGoogle Scholar
  57. 57.
    Lee, E.A., Seshia, S.: Introduction to Embedded Systems, A Cyber-physical Systems Approach, 2nd edn. MIT Press, Cambridge (2015) zbMATHGoogle Scholar
  58. 58.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Proceedings, Runtime Verification, RV, St. Julian’s, Malta, November 1–4, 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  59. 59.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009) CrossRefGoogle Scholar
  60. 60.
    Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995) Google Scholar
  61. 61.
    Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. In: Van Deusen, M.S., Galil, Z., Reid, B.K. (eds.) Principles of Programming Languages, POPL, New Orleans, LA, USA, January 1985, pp. 97–107. ACM, New York (1985) Google Scholar
  62. 62.
    Manna, Z.: Introduction to Mathematical Theory of Computation. McGraw-Hill, New York (1974) zbMATHGoogle Scholar
  63. 63.
    Manna, Z., Peled, D. (eds.): Time for Verification, Essays in Memory of Amir Pnueli. LNCS, vol. 6200. Springer, Heidelberg (2010) zbMATHGoogle Scholar
  64. 64.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992) CrossRefGoogle Scholar
  65. 65.
    Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal-logic specifications. In: Kozen, D. (ed.) Proceedings, Logics of Programs, Yorktown Heights, NY, USA, May 1981. LNCS, vol. 131, pp. 253–281. Springer, Heidelberg (1981) CrossRefGoogle Scholar
  66. 66.
    McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems. Studies in Logic and the Foundations of Mathematics, vol. 35, pp. 33–70. Elsevier, Amsterdam (1963) CrossRefGoogle Scholar
  67. 67.
    McMillan, K.L.: Symbolic Model Checking. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  68. 68.
    Nielson, F., Riis Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999) CrossRefGoogle Scholar
  69. 69.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  70. 70.
    Panda, A., Argyraki, K.J., Sagiv, M., Schapira, M., Shenker, S.: New directions for network verification. In: Ball, T., Bodík, R., Krishnamurthi, S., Lerner, B.S., Morrisett, G. (eds.) Proceedings, Summit on Advances in Programming Languages, SNAPL, Asilomar, CA, USA, May 3–6, 2015. LIPIcs, vol. 32, pp. 209–220. Schloss Dagstuhl, Wadern (2015) Google Scholar
  71. 71.
    Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  72. 72.
    Pnueli, A.: The temporal logic of programs. In: Proceedings, Foundations of Computer Science, FOCS, Providence, RI, USA, October 31–November 1, 1977, pp. 46–57. IEEE, Piscataway (1977) Google Scholar
  73. 73.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings, Principles of Programming Languages, POPL, Austin, TX, USA, January 11–13, 1989, pp. 179–190. ACM, New York (1989) Google Scholar
  74. 74.
    Priami, C., Morine, M.J.: Analysis of Biological Systems. Imperial College Press, London (2015) CrossRefGoogle Scholar
  75. 75.
    Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proceedings, International Symposium on Programming, Torino, Italy, April 6–8, 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982) CrossRefGoogle Scholar
  76. 76.
    Rabin, M.O.: Automata on Infinite Objects and Church’s Problem. AMS, Providence (1972) CrossRefGoogle Scholar
  77. 77.
    Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989) CrossRefGoogle Scholar
  78. 78.
    Raychev, V., Bielik, P., Vechev, M.T., Krause, A.: Learning programs from noisy data. In: Bodík, R., Majumdar, R. (eds.) Proceedings, Principles of Programming Languages, POPL, St. Petersburg, FL, USA, January 20–22, 2016, pp. 761–774. ACM, New York (2016) Google Scholar
  79. 79.
    Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74, 358–366 (1953) MathSciNetCrossRefGoogle Scholar
  80. 80.
    Solar-Lezama, A.: Program sketching. Softw. Tools Technol. Transf. 15(5–6), 475–495 (2013) CrossRefGoogle Scholar
  81. 81.
    Tabuada, P.: Verification and Control of Hybrid Systems. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  82. 82.
    Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42, 230–265 (1937) MathSciNetCrossRefGoogle Scholar
  83. 83.
    van der Aalst, W.M.P.: Process Mining—Data Science in Action, 2nd edn. Springer, Heidelberg (2016) CrossRefGoogle Scholar
  84. 84.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings, Logic in Computer Science, LICS, Cambridge, MA, USA, June 16–18, 1986, pp. 322–331. IEEE, Piscataway (1986) Google Scholar
  85. 85.
    Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS, vol. 3600. Springer, Heidelberg (2006) Google Scholar
  86. 86.
    Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings, Foundations of Computer Science, FOCS, Tucson, AZ, USA, November 7–9, 1983, pp. 185–194. IEEE, Piscataway (1983) Google Scholar
  87. 87.
    Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. Commun. ACM 54(12), 123–131 (2011) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Edmund M. Clarke
    • 1
  • Thomas A. Henzinger
    • 2
  • Helmut Veith
    • 3
  1. 1.Carnegie Mellon UniversityPittsburghUSA
  2. 2.IST AustriaKlosterneuburgAustria
  3. 3.Technische Universität WienViennaAustria

Personalised recommendations