Abstract
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.
Preview
Unable to display preview. Download preview PDF.
References
http://www.absint.de/astree/ accessed 20 Oct 2013
Accellera Property Specification Language Reference Manual (version 1.01). http://www.eda.org/vfv/docs/psl_lrm-1.01.pdf accessed 20 Oct 2013
Ahrens, F.: Why It’s So Hard For Toyota To Find Out What’s Wrong. The Washington Post p. G01 (2010). see http://www.washingtonpost.com/wp-dyn/content/article/2010/03/06/AR2010030602448_pf.html accessed 20 Oct 2013
Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509–516 (1978)
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)
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)
http://www.astree.ens.fr/ accessed 20 Oct 2013
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)
Barr, M.: Unintended acceleration and other embedded software bugs (2011). http://embeddedgurus.com/barr-code/2011/03/unintended-acceleration-and-other-embedded-software-bugs/ accessed 20 Oct 2013
Berry, G., Gonthier, G.: The ESTEREL synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87–152 (1992)
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)
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)
Blau, J.: AT&T’s frame relay crash highlights vulnerable nature of data networks. Total Telcom (1998). http://www.totaltele.com/view.aspx?C=0&ID=433385 accessed 20 Oct 2013
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
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)
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)
Bryant, R.: Computer-aided verification prize awarded. Not. Am. Math. Soc. 56(11), 1456–1457 (2009)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)
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)
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)
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
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)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001)
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)
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)
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)
NASA’s metric confusion caused Mars orbiter loss (1999). http://www.cnn.com/TECH/space/9909/30/mars.metric/; see also http://www.thinkreliability.com/CM-MarsCO.aspx; both accessed 20 Oct 2013
Coe, T.: Inside the Pentium FDIV bug. Dr. Dobb’s J. 20, 129–135 (1995)
Cousot, P., Cousot, R.: Basic concepts of abstract interpretation. In: Jacquard, R. (ed.) Building the Information Society, pp. 359–366. Kluwer Academic, Norwell (2004)
http://www.coverity.com/products/static-analysis.html accessed 20 Oct 2013
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)
Emanuelsson, P., Nilsson, U.: A comparative study of industrial static analysis tools. Electron. Notes Theor. Comput. Sci. 217, 5–21 (2008). doi:10.1016/j.entcs.2008.06.039 accessed 20 Oct 2013
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)
Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional \(\mu\)-calculus. In: Proc. LICS, pp. 267–278. IEEE, Piscataway (1986)
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)
Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol. 19, pp. 19–32 (1967)
Lucent’s Bell introduces FormalCheck. Electronic News (1997)
Foster, H.: Prologue: the 2010 Wilson research group functional verification study (2011). http://blogs.mentor.com/verificationhorizons/blog/2011/03/30/prologue-the-2010-wilson-research-group-functional-verification-study/ accessed 20 Oct 2013
Foster, H.D., Krolnik, A.C., Lacey, D.J.: Assertion Based Design, 2nd edn. Kluwer Academic, Norwell (2004)
Goldstine, H.H., von Neumann, J.: Planning and Coding of the Problems for an Electronic Computing Instrument. Institute for Advanced Study, Princeton (1947)
Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78 (1979)
http://www.grammatech.com/products/codesonar/smashproof_analysis.html accessed 20 Oct 2013
Grumberg, O.: McMillan receives CAV award. Not. Am. Math. Soc. 57(10), 1318 (2010)
Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008)
Gupta, A.: Alur and Dill receive computer-aided verification award. Not. Am. Math. Soc. 55(11), 1429 (2008)
Hoare, C.A.R.: An axiomatic basis for programming. Commun. ACM 12(10), 576–580 (1969)
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)
Toyota shareholders in US sue over fallen stock price. JapanToday (2010). http://www.japantoday.com/category/business/view/toyota-shareholders-in-us-sue-over-fallen-stock-price accessed 06 Aug 2013
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)
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)
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)
http://docs.klocwork.com/Insight-9.6/Klocwork_Truepath accessed 15 Sep 2015
Kozen, D.: Results on propositional \(\mu\)-calculus. Theor. Comput. Sci. 27, 333–354 (1983)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. DAC’97, vol. 34, pp. 258–262 (1997)
Kurshan, R.P.: Program verification. Not. Am. Math. Soc. 47(5), 534–545 (2000)
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)
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)
Lee, C.Y.: Representations of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985–999 (1959)
Leveson, N.G., Turner, C.S.: An investigation of the Therac-25 accidents. IEEE Comput. 26(7), 18–41 (1993)
Lions, J.L.: Ariane 5 flight 501 failure (1996). http://web.archive.org/web/20000815230639/www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html accessed 20 Oct 2013
Lohr, S.: AT&T data network fails and commerce takes a hit. The New York Times (1998). http://www.nytimes.com/1998/04/15/business/at-t-data-network-fails-and-commerce-takes-a-hit.html accessed 20 Oct 2013
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic, Norwell (1993)
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)
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)
Mead, C., Conway, L.: Introduction to VLSI Systems. Addison-Wesley, Reading (1979)
Naur, P.: Proof of algorithms by general snapshots. BIT 6(4), 310–316 (1966)
http://www.parasoft.com/jsp/technologies/code_analysis.jsp accessed 20 Oct 2013
Pnueli, A.: The temporal logic of programs. In: Proc. Eighteenth FOCS, pp. 46–57. IEEE, Piscataway (1977)
http://www.mathworks.com/products/polyspace/ accessed 20 Oct 2013
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)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 114–125 (1959)
Robinson, J.A.: Machine-oriented logic based on the resolution principle. J. ACM 12, 23–41 (1965)
Rudin, H., West, C.: A validation technique for tightly coupled protocols. IEEE Trans. Comput. 31(7), 630–636 (1982)
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)
Shannon, C.E.: The synthesis of two-terminal switching circuits. Bell Syst. Tech. J. 28, 59–98 (1949)
Sterling, B.: PART ONE: crashing the system (1990). http://www.farcaster.com/sterling/part1.htm accessed 15 Sep 2015
Travis, P.: Why the AT&T network crashed. Telephony 218(4), 11 (1990). See also http://www.phworld.org/history/attcrash.htm and http://tech-insider.org/data-security/research/1990/0126.html, both accessed 15 Sep 2015
Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42 (1936)
Vardi, M.: Ball and Rajamani receive 2011 CAV award. Not. Am. Math. Soc. 58(11), 1597 (2011)
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)
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)
Waxer, C.: The hidden cost of IT security. Network Security Journal (2006). http://www.networksecurityjournal.com/features/hidden-cost-of-IT-security-041607/ accessed 20 Oct 2013
West, C.: Generalized technique for communication protocol validation. IBM J. Res. Dev. 22, 393–404 (1978)
Whitehead, A.N., Russell, B.: Principia Mathematica. Cambridge University Press, Cambridge (1910–1913)
Yuan, J., Pixley, C., Aziz, A.: Constraint-Based Verification. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Kurshan, R.P. (2018). Transfer of Model Checking to Industrial Practice. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-10575-8_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10574-1
Online ISBN: 978-3-319-10575-8
eBook Packages: Computer ScienceComputer Science (R0)