Abstract
In this chapter we discuss the methodology used in explicit-state logic model checking, specifically as applied to asynchronous software systems. As the name indicates, in an explicit-state model checker the state descriptor for a system is maintained in explicit, and not symbolic, form, as are all state transitions. Abstraction techniques and partial-order reduction algorithms are used to reduce the search space to a minimum, and advanced storage techniques can be used to extend the reach of this form of verification to very large system sizes. The basic algorithms for explicit-state model checking date from the late 1970s and early 1980s. More advanced versions of these algorithms remain an active area of research.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
The game of tic-tac-toe. http://f2.org/maths/ttt.html
Avrunin, G., Corbett, J., Dwyer, M., Pasareanu, C., Siegel, S.: Benchmarking finite-state verifiers. Int. J. Softw. Tools Technol. Transf. 2(4), 317–320 (2000)
Barnet, J., Brim, L., Rockai, P.: DiVinE multi-core, a parallel LTL model checker. In: Liu, Z., Ravn, A.P. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 5799, pp. 234–239. Springer, Heidelberg (2009)
Bloom, B.: Spacetime trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422–426 (1970)
Bosnacki, D.: Enhancing state space reduction techniques for model checking. Ph.D. thesis, Eindhoven University of Technology (2001)
Clarke, E., Emerson, E., Jha, S., Sistla, A.: Symmetry reduction in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998)
Corbett, J.: Evaluating deadlock detection methods for concurrent software. Trans. Softw. Eng. 22(3), 161–180 (1996)
Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1(2–3), 275–288 (1992)
Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)
Etessami, K., Holzmann, G.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) Proc. 11th Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)
Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pp. 3–18. Chapman & Hall, London (1996)
Hajek, J.: Automatically verified data transfer protocols. In: Intl. Conf. on Computer Communication (ICCC), pp. 749–756 (1978)
Holzmann, G.: PAN: a protocol specification analyzer. Tech. Rep. TM81-11271-5, AT&T Bell Laboratories, (1981)
Holzmann, G.: An improved reachability analysis technique. Softw. Pract. Exp. 18(2), 137–161 (1988)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
Holzmann, G.: Parallelizing the Spin model checker. In: Donaldson, A.F., Parker, D. (eds.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol. 7385, pp. 155–171. Springer, Heidelberg (2012)
Holzmann, G.: Proving properties of concurrent programs. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol. 7976, pp. 18–23. Springer, Heidelberg (2013)
Holzmann, G., Bosnacki, D.: The design of a multi-core extension of the Spin model checker. Trans. Softw. Eng. 33(10), 659–674 (2007)
Holzmann, G., Florian, M.: Model checking with bounded context switching. Form. Asp. Comput. 23(3), 365–389 (2011)
Holzmann, G., Joshi, R., Gorce, A.: Swarm verification techniques. Trans. Softw. Eng. 37(6), 845–857 (2011)
Holzmann, G., Peled, D.: An improvement in formal verification. In: Proc. of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 197–211. Chapman & Hall, London (1995)
Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: Grégoire, J.C., Holzmann, G., Peled, D. (eds.) The Spin Verification System. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 23–32. DIMACS/AMS, Providence (1996)
Ip, C., Dill, D.: Better verification through symmetry. Form. Methods Syst. Des. 9(1–2), 41–75 (2006)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-Conference on Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Peled, D.: Partial-order reduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)
Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46–57. IEEE, Piscataway (1977)
Tanenbaum, A.: Computer Networks, 1st edn. Prentice Hall, New York (1981)
Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994). Journal version of a conference paper first published in 1983
West, C.: General technique for communications protocol validation. IBM J. Res. Dev. 22(3), 393–404 (1978)
West, C., Zafiropulo, P.: Automated validation of a communications protocol: the CCITT X.21 recommendation. IBM J. Res. Dev. 22(1), 60–71 (1978)
Wolper, P.: Specifying interesting properties of programs in propositional temporal logic. In: Symp. on Principles of Programming Languages (POPL), pp. 184–193. ACM, New York (1986)
Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)
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
Holzmann, G.J. (2018). Explicit-State Model Checking. 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_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-10575-8_5
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)