Abstract
In the last 25 years, the notion of performing software verification with logic model checking techniques has evolved from intellectual curiosity to accepted technology with significant potential for broad practical application. In this paper we look back at the main steps in this evolution and illustrate how the challenges have changed over the years, as we sharpened our theories and tools. Next we discuss a typical challenge in software verification that we face today – and that perhaps we can look back on in another 25 years as having inspired the next logical step towards a broader integration of model checking into the software development process.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Kaufmann, M., Manolios, P., Strother Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (July 2000), http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex lines. Comm. ACM 12(5), 260–265
Bochmann, G.V.: Finite state description of communication protocols, Publ. 236, Dept. d’Informatique, University of Montreal (July 1976)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. On Programming Languages and Systems 8(2), 244–263 (1986)
Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Software Engineering Notes 31(3), 25–37 (2006)
http://www.st.cs.uni-sb.de/dd/ on delta debugging techniques
Goldstein, H.H., Von Neumann, J.: Planning and coding problems for an electronic computing instrument. Part II, vol. 1, Princeton ( April 1947)
Holzmann, G.J.: PAN: a protocol specification analyzer, Tech Report TM81-11271-5, AT&T Bell Laboratories (March 1981)
Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proc. 7th Int. Conf. on Formal Description Techniques (FORTE) 1994, pp. 197–211. Chapman and Hall (1994)
Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal 5(2), 72–87 (2000)
Holzmann, G.J.: Static source code checking for user-defined properties. In: Proc. 6th World Conference on Integrated Design & Process Technology (IDPT), Pasadena CA, USA (June 2002)
Holzmann, G.J., Joshi, R.: Model-Driven Software Verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 77–92. Springer, Heidelberg (2004)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2003)
Holzmann, G.J., Joshi, R.: A mini grand challenge: build a verifiable file-system (position paper), Grand Challenge in Verified Software – Theories, Tools, Experiments, Zurich, Switzerland (October 2005)
Holzmann, G.J.: The Power of Ten: rules for developing safety critical code. IEEE Computer (June 2006)
McKeeman, W.M.: Differential testing for software. Digital Technical Journal 10(1), 100–107 (1998)
Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Proc. Fifth Symposium on Operating Systems Design and Implementation, OSDI (December 2002)
Rajamani, S.K., Ball, T.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057. Springer, Heidelberg (2001)
Sunshine, C.A.: Interprocess Communication Protocols for Computer Networks, Ph.D. Thesis, Dept. of Computer Science, Stanford Univ., Stanford, CA (1975)
Vardi, M., Wolper, P.: An authomata-theoretic approacj to automatic program verification. In: Proc. 1st Annual Symposium on Logic in Computer Science, LICS, pp. 332–344 (1986)
Grand Challenge in Verified Software – Theories, Tools, Experiments (VSTTE), Zurich, Switzerland (October 2005), http://vstte.ethz.ch/
West, C.H., Zafiropulo, P.: Automated validation of a communications protocol: the CCITT X. 21 recommendation, IBM J. Res. Develop. 22(1), 60–71 (1978)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Holzmann, G.J., Joshi, R., Groce, A. (2008). New Challenges in Model Checking. In: Grumberg, O., Veith, H. (eds) 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69850-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-69850-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69849-4
Online ISBN: 978-3-540-69850-0
eBook Packages: Computer ScienceComputer Science (R0)