×

Transfer of model checking to industrial practice. (English) Zbl 1392.68256

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). 763-793 (2018).
Summary: This chapter traces the practical challenges that were overcome in order to transfer model-checking theory to industrial practice. In retrospect, this transfer provided a lesson in how to, and how not to accomplish technology transfer. The methodology changes required for industrial model checking were achieved through a succession of steps, each of which was small enough to avoid unacceptable disruption of existing methodologies, while significant enough to demonstrate value.
For the entire collection see [Zbl 1390.68001].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ABC; Esterel; CESAR; CBMC; SLAM
Full Text: DOI

References:

[1] 1.
[2] 2. Accellera Property Specification Language Reference Manual (version 1.01).
[3] 3. Ahrens, F.: Why It’s So Hard For Toyota To Find Out What’s Wrong. The Washington Post p. G01 (2010). see
[4] 4. Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509-516 (1978) · Zbl 0377.94038 · doi:10.1109/TC.1978.1675141
[5] 5. Alur, R.: Model checking: from tools to theory. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 89-106. Springer, Heidelberg (2008) · Zbl 1142.68429 · doi:10.1007/978-3-540-69850-0_6
[6] 6. Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. In: von Bochmann, G., Probst, D. (eds.) Proc. CAV’92. LNCS, vol. 663, pp. 137-150. Springer, Heidelberg (1993). Also Inf. Comput. 118(1), 142-157 (1995) · Zbl 0939.68705
[7] 7.
[8] 8. Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) Symposium on Principles of Programming Languages (POPL), pp. 1-3. ACM, New York (2002)
[9] 9. Barr, M.: Unintended acceleration and other embedded software bugs (2011).
[10] 10. Berry, G., Gonthier, G.: The ESTEREL synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87-152 (1992) · Zbl 0772.68013 · doi:10.1016/0167-6423(92)90005-V
[11] 11. Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 66-75 (2010) · doi:10.1145/1646353.1646374
[12] 12. Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Design Automation Conference, pp. 317-320. IEEE, Piscataway (1999)
[13] 13. Blau, J.: AT&T’s frame relay crash highlights vulnerable nature of data networks. Total Telcom (1998).
[14] 14. Bledsoe, W.W., Loveland, D.W. (eds.): Automated Theorem Proving: After 25 Years, vol. 29. AMS, Providence (1984). Especially the paper “Proof-Checking, Theorem-Proving and Program Verification” by R.S. Boyer and J.S. Moore, 119-132
[15] 15. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Proc. VMCAI 2011. LNCS, vol. 6538, pp. 70-87. Springer, Heidelberg (2011) · Zbl 1317.68109
[16] 16. Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Tonilli, T., Cook, B., Jackson, P. (eds.) Proc. CAV’10. LNCS, vol. 6174, pp. 24-40. Springer, Heidelberg (2010)
[17] 17. Bryant, R.: Computer-aided verification prize awarded. Not. Am. Math. Soc. 56(11), 1456-1457 (2009)
[18] 18. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677-691 (1986) · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819
[19] 19. Bryant, R.E., Kukula, J.H.: Formal methods for functional verification. In: Kuehlmann, A. (ed.) The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, pp. 3-16. Kluwer Academic, Norwell (2003) · doi:10.1007/978-1-4615-0292-0_1
[20] 20. Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Methodology and Philosophy of Science, Proc., 1960 Stanford Intern. Congr., pp. 1-11. Stanford University Press, Stanford (1962) · Zbl 0147.25103
[21] 21. Church, A.: Application of recursive arithmetics to the problem of circuit synthesis. In: Summaries of Talks Presented at the Summer Institute for Symbolic Logic, pp. 3-50 (1957). Communications Research Division, Institute for Defense Analysis · Zbl 0206.47902
[22] 22. Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1-26. Springer, Heidelberg (2008) · Zbl 1142.68046 · doi:10.1007/978-3-540-69850-0_1
[23] 23. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7-34 (2001) · Zbl 0985.68038 · doi:10.1023/A:1011276507260
[24] 24. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Proc. Logic of Programs Workshop. LNCS, vol. 131, pp. 52-71. Springer, Heidelberg (1982) · Zbl 0546.68014 · doi:10.1007/BFb0025774
[25] 25. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752-794 (2003). A preliminary version was published as “Counterexample-Guided Abstraction Refinement”. In: Emerson, E.A., Prasad, A. (eds.) Proc. CAV’00. LNCS, vol. 1855, pp. 154-169. Springer, Heidelberg (2000) · Zbl 1325.68145 · doi:10.1145/876638.876643
[26] 26. Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). LNCS, vol. 2988, pp. 168-176. Springer, Heidelberg (2004) · Zbl 1126.68470
[27] 27. NASA’s metric confusion caused Mars orbiter loss (1999).
[28] 28. Coe, T.: Inside the Pentium FDIV bug. Dr. Dobb’s J. 20, 129-135 (1995)
[29] 29. Cousot, P., Cousot, R.: Basic concepts of abstract interpretation. In: Jacquard, R. (ed.) Building the Information Society, pp. 359-366. Kluwer Academic, Norwell (2004) · Zbl 1325.68061 · doi:10.1007/978-1-4020-8157-6_27
[30] 30.
[31] 31. Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522-525. IEEE, Piscataway (1992)
[32] 32. Emanuelsson, P., Nilsson, U.: A comparative study of industrial static analysis tools. Electron. Notes Theor. Comput. Sci. 217, 5-21 (2008). doi: · doi:10.1016/j.entcs.2008.06.039
[33] 33. Emerson, E.A.: The beginning of model checking: a personal perspective. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 27-45. Springer, Heidelberg (2008) · Zbl 1142.68047 · doi:10.1007/978-3-540-69850-0_2
[34] 34. Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional
[35] 35. Fiskio-Lasseter, J., Sabry, A.: Putting operational techniques to the test: a syntactic theory for behavioral Verilog. Electron. Notes Theor. Comput. Sci. 26, 34-51 (1999) · Zbl 0959.68020 · doi:10.1016/S1571-0661(05)80282-8
[36] 36. Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol. 19, pp. 19-32 (1967) · Zbl 0189.50204 · doi:10.1090/psapm/019/0235771
[37] 37. Lucent’s Bell introduces FormalCheck. Electronic News (1997)
[38] 38. Foster, H.: Prologue: the 2010 Wilson research group functional verification study (2011).
[39] 39. Foster, H.D., Krolnik, A.C., Lacey, D.J.: Assertion Based Design, 2nd edn. Kluwer Academic, Norwell (2004)
[40] 40. Goldstine, H.H., von Neumann, J.: Planning and Coding of the Problems for an Electronic Computing Instrument. Institute for Advanced Study, Princeton (1947)
[41] 41. Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78 (1979) · Zbl 0421.68039
[42] 42. · JFM 33.0136.01
[43] 43. Grumberg, O.: McMillan receives CAV award. Not. Am. Math. Soc. 57(10), 1318 (2010)
[44] 44. Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008) · Zbl 1139.68003
[45] 45. Gupta, A.: Alur and Dill receive computer-aided verification award. Not. Am. Math. Soc. 55(11), 1429 (2008)
[46] 46. Hoare, C.A.R.: An axiomatic basis for programming. Commun. ACM 12(10), 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[47] 47. Huuck, R., Lukoschus, B., Frehse, G., Engell, S.: Compositional verification of continuous-discrete systems. In: Engell, S., Frehse, G., Schnieder, E. (eds.) Modelling, Analysis, and Design of Hybrid Systems. LNCS, vol. 279, pp. 225-244. Springer, Heidelberg (2002) · Zbl 1003.93001 · doi:10.1007/3-540-45426-8_13
[48] 48. Toyota shareholders in US sue over fallen stock price. JapanToday (2010).
[49] 49. Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S. (eds.) Proc. CAV’05. LNCS, vol. 3576, pp. 39-51. Springer, Heidelberg (2005) · Zbl 1081.68622
[50] 50. Kaufmann, M., Moore, J.S.: Some key research problems in automated theorem proving for hardware and software verification. Rev. R. Acad. Cienc. Exactas Fís. Nat., Ser. a Mat. 98(1), 185-195 (2004) · Zbl 1103.68800
[51] 51. Khasidashvili, Z., Gavrielov, G., Melham, T.: Assume-guarantee validation for STE properties within an SVA environment. In: Biere, A., Pixley, C. (eds.) Proc. FMCAD’09, pp. 108-115. IEEE, Piscataway (2009)
[52] 52. · JFM 24.0683.05
[53] 53. Kozen, D.: Results on propositional · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6
[54] 54. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994) · Zbl 0822.68116
[55] 55. Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. DAC’97, vol. 34, pp. 258-262 (1997)
[56] 56. Kurshan, R.P.: Program verification. Not. Am. Math. Soc. 47(5), 534-545 (2000) · Zbl 1040.68060
[57] 57. Kurshan, R.P.: Scaling commercial verification to larger systems. In: Yorav, K. (ed.) Hardware and Software: Verification and Testing. LNCS, vol. 4899, pp. 8-13. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-77966-7_2
[58] 58. Kurshan, R.P.: Verification technology transfer. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 46-64. Springer, Heidelberg (2008) · Zbl 1142.68437 · doi:10.1007/978-3-540-69850-0_3
[59] 59. Lee, C.Y.: Representations of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985-999 (1959) · doi:10.1002/j.1538-7305.1959.tb01585.x
[60] 60. Leveson, N.G., Turner, C.S.: An investigation of the Therac-25 accidents. IEEE Comput. 26(7), 18-41 (1993) · doi:10.1109/MC.1993.274940
[61] 61. Lions, J.L.: Ariane 5 flight 501 failure (1996).
[62] 62. Lohr, S.: AT&T data network fails and commerce takes a hit. The New York Times (1998).
[63] 63. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic, Norwell (1993) · Zbl 0784.68004 · doi:10.1007/978-1-4615-3190-6
[64] 64. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Proc. CAV’03. LNCS, vol. 2725, pp. 1-13. Springer, Heidelberg (2003) · Zbl 1278.68184
[65] 65. McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) Proc. TACAS’03. LNCS, vol. 2619, pp. 2-17. Springer, Heidelberg (2003) · Zbl 1031.68520
[66] 66. Mead, C., Conway, L.: Introduction to VLSI Systems. Addison-Wesley, Reading (1979)
[67] 67. Naur, P.: Proof of algorithms by general snapshots. BIT 6(4), 310-316 (1966) · doi:10.1007/BF01966091
[68] 68. · Zbl 0191.46202
[69] 69. Pnueli, A.: The temporal logic of programs. In: Proc. Eighteenth FOCS, pp. 46-57. IEEE, Piscataway (1977)
[70] 70.
[71] 71. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proc. Intl. Symp. on Programming. LNCS, vol. 137, pp. 337-351. Springer, Heidelberg (1982) · Zbl 0482.68028 · doi:10.1007/3-540-11494-7_22
[72] 72. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 114-125 (1959) · Zbl 0158.25404 · doi:10.1147/rd.32.0114
[73] 73. Robinson, J.A.: Machine-oriented logic based on the resolution principle. J. ACM 12, 23-41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253
[74] 74. Rudin, H., West, C.: A validation technique for tightly coupled protocols. IEEE Trans. Comput. 31(7), 630-636 (1982) · doi:10.1109/TC.1982.1676060
[75] 75. Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Form. Methods Syst. Des. 6(2), 147-190 (1995) · doi:10.1007/BF01383966
[76] 76. Shannon, C.E.: The synthesis of two-terminal switching circuits. Bell Syst. Tech. J. 28, 59-98 (1949) · doi:10.1002/j.1538-7305.1949.tb03624.x
[77] 77. Sterling, B.: PART ONE: crashing the system (1990).
[78] 78. Travis, P.: Why the AT&T network crashed. Telephony 218(4), 11 (1990). See also
[79] 79. Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42 (1936) · JFM 62.1059.03
[80] 80. Vardi, M.: Ball and Rajamani receive 2011 CAV award. Not. Am. Math. Soc. 58(11), 1597 (2011)
[81] 81. Vardi, M.Y.: From Church and Prior to PSL. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 150-171. Springer, Heidelberg (2008) · Zbl 1142.68051 · doi:10.1007/978-3-540-69850-0_10
[82] 82. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. (1st) IEEE Symposium on Logic in Computer Science (LICS), pp. 322-331 (1986)
[83] 83. Waxer, C.: The hidden cost of IT security. Network Security Journal (2006).
[84] 84. West, C.: Generalized technique for communication protocol validation. IBM J. Res. Dev. 22, 393-404 (1978) · doi:10.1147/rd.224.0393
[85] 85. Whitehead, A.N., Russell, B.: Principia Mathematica. Cambridge University Press, Cambridge (1910-1913) · JFM 41.0083.02
[86] 86. Yuan, J., Pixley, C., Aziz, A.: Constraint-Based Verification. Springer, Heidelberg (2006) · Zbl 1093.68058
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.