×

Introduction to model checking. (English) Zbl 1392.68242

Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 1-26 (2018).
Summary: 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.
For the entire collection see [Zbl 1390.68001].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

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) · doi:10.1093/comjnl/bxp023
[2] 2. Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181-185 (1985) · Zbl 0575.68030 · doi:10.1016/0020-0190(85)90056-0
[3] 3. Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)
[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)
[5] 5. Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971-984 (2000) · doi:10.1109/5.871304
[6] 6. Appel, A.W.: Modern Compiler Implementation in C. Cambridge University Press, Cambridge (1998) · Zbl 0888.68036
[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) · Zbl 1183.68361 · doi:10.1007/978-1-84882-745-5
[8] 8. Baier, C., Katoen, J-P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076
[9] 9. Baresi, L., Di Nitto, E.: Test and Analysis of Web Services. Springer, Heidelberg (2007) · doi:10.1007/978-3-540-72912-9
[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) · doi:10.1007/3-540-63166-6_28
[11] 11. Ben-Ari, M.: Principles of the SPIN Model Checker. Springer, Heidelberg (2008) · Zbl 1142.68044
[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) · Zbl 1002.68029 · doi:http://scholar.google.com/scholar_lookup?title=Systems and Software Verification: Model-Checking Techniques and Tools&author=B.. B%C3%A9rard&author=M.. Bidoit&author=A.. Finkel&author=F.. Laroussinie&author=A.. Petit&author=L.. Petrucci&author=P.. Schnoebelen&publication_year=2001
[13] 13. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004) · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5
[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) · Zbl 1420.68119
[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) · Zbl 1354.68169 · doi:10.1145/2629686
[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) · doi:10.1007/978-3-319-23820-3_23
[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)
[18] 18. Cassandras, C.G., Lafortune, S.: Introduction to Discrete-Event Systems, 2nd edn. Springer, Heidelberg (2008) · Zbl 1165.93001 · doi:10.1007/978-0-387-68612-7
[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) · Zbl 1381.68040 · doi:10.1007/978-3-319-21668-3_11
[20] 20. Cerný, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21-35 (2012) · Zbl 1234.68253 · doi:10.1016/j.tcs.2011.08.002
[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) · Zbl 1301.68244
[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) · Zbl 0546.68014 · doi:10.1007/BFb0025774
[23] 23. Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74-84 (2009) · doi:10.1145/1592761.1592781
[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)
[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) · doi:10.1007/0-8176-4404-0_23
[26] 26. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) · Zbl 1423.68002
[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)
[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) · Zbl 1066.68075 · doi:10.1016/B978-044450813-3/50026-6
[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)
[30] 30. Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45-80 (2001) · Zbl 0985.68033 · doi:10.1023/A:1011227529550
[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)
[32] 32. Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859-866 (1972) · doi:10.1145/355604.361591
[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) · Zbl 0900.03030
[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) · Zbl 0629.68020 · doi:10.1145/4904.4999
[35] 35. Fisher, J., Harel, D., Henzinger, T.A.: Biology as reactivity. Commun. ACM 54(10), 72-82 (2011) · doi:10.1145/2001269.2001289
[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) · doi:10.1090/psapm/019/0235771
[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)
[38] 38. Grumberg, O., Veith, H.: 25 Years of Model Checking: History, Achievements, Perspectives. LNCS, vol. 5000. Springer, Heidelberg (2008) · Zbl 1139.68003 · doi:10.1007/978-3-540-69850-0
[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) · doi:10.1145/2736282
[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).
[41] 41. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231-274 (1987) · Zbl 0637.68010 · doi:10.1016/0167-6423(87)90035-9
[42] 42. Harel, D., Marelly, R.: Come, Let’s Play. Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
[43] 43. Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci. Res. Dev. 28(4), 331-344 (2013) · doi:10.1007/s00450-013-0251-7
[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) · Zbl 1390.68428
[45] 45. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[46] 46. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, New York (1995)
[47] 47. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
[48] 48. Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-Based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2007) · Zbl 1142.68024 · doi:10.1017/CBO9780511619540
[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)
[50] 50. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385-394 (1976) · Zbl 0329.68018 · doi:10.1145/360248.360252
[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) · doi:10.1145/2560537
[52] 52. Kozen, D.: Results on the propositional · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6
[53] 53. Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1-14 (1959) · Zbl 0091.00902 · doi:10.2307/2964568
[54] 54. Kropf, T.: Introduction to Formal Hardware Verification. Springer, Heidelberg (1999) · Zbl 0931.68018 · doi:10.1007/978-3-662-03809-3
[55] 55. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994) · Zbl 0822.68116
[56] 56. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 2, 125-143 (1977) · Zbl 0349.68006 · doi:10.1109/TSE.1977.229904
[57] 57. Lee, E.A., Seshia, S.: Introduction to Embedded Systems, A Cyber-physical Systems Approach, 2nd edn. MIT Press, Cambridge (2015) · Zbl 1371.68001
[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) · doi:10.1007/978-3-642-16612-9_11
[59] 59. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107-115 (2009) · doi:10.1145/1538788.1538814
[60] 60. Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)
[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)
[62] 62. Manna, Z.: Introduction to Mathematical Theory of Computation. McGraw-Hill, New York (1974) · Zbl 0353.68066
[63] 63. Manna, Z., Peled, D. (eds.): Time for Verification, Essays in Memory of Amir Pnueli. LNCS, vol. 6200. Springer, Heidelberg (2010) · Zbl 1194.68054
[64] 64. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992) · Zbl 0753.68003 · doi:10.1007/978-1-4612-0931-7
[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) · Zbl 0487.68027 · doi:10.1007/BFb0025786
[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) · Zbl 0203.16402 · doi:10.1016/S0049-237X(08)72018-4
[67] 67. McMillan, K.L.: Symbolic Model Checking. Springer, Heidelberg (1993) · Zbl 0784.68004 · doi:10.1007/978-1-4615-3190-6
[68] 68. Nielson, F., Riis Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999) · Zbl 0932.68013 · doi:10.1007/978-3-662-03811-6
[69] 69. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[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)
[71] 71. Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001) · Zbl 0980.68014 · doi:10.1007/978-1-4757-3540-6
[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)
[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) · Zbl 0686.68015
[74] 74. Priami, C., Morine, M.J.: Analysis of Biological Systems. Imperial College Press, London (2015) · doi:10.1142/p1004
[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) · Zbl 0482.68028 · doi:10.1007/3-540-11494-7_22
[76] 76. Rabin, M.O.: Automata on Infinite Objects and Church’s Problem. AMS, Providence (1972) · Zbl 0315.02037 · doi:10.1090/cbms/013
[77] 77. Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81-98 (1989) · doi:10.1109/5.21072
[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) · Zbl 1347.68092
[79] 79. Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74, 358-366 (1953) · Zbl 0053.00301 · doi:10.1090/S0002-9947-1953-0053041-6
[80] 80. Solar-Lezama, A.: Program sketching. Softw. Tools Technol. Transf. 15(5-6), 475-495 (2013) · doi:10.1007/s10009-012-0249-7
[81] 81. Tabuada, P.: Verification and Control of Hybrid Systems. Springer, Heidelberg (2009) · Zbl 1195.93001 · doi:10.1007/978-1-4419-0224-5
[82] 82. Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42, 230-265 (1937) · JFM 62.1059.03 · doi:10.1112/plms/s2-42.1.230
[83] 83. van der Aalst, W.M.P.: Process Mining—Data Science in Action, 2nd edn. Springer, Heidelberg (2016) · doi:10.1007/978-3-662-49851-4
[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)
[85] 85. Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS, vol. 3600. Springer, Heidelberg (2006)
[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)
[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) · doi:10.1145/2043174.2043197
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.