Abstract
This paper presents a disk-based explicit-state model checking algorithm that uses an approach called layered duplicate detection. In this approach, states encountered during a breadth-first traversal of the graph of the transition system are stored in memory according to the layer of the graph in which they are first encountered. With this layered organization of memory, transition locality is exploited by checking only the most recent layers for duplicates. In RAM, exploiting transition locality in this way saves time. In external memory, it saves space. In addition, a layered structure allows an easy method of counterexample reconstruction in disk-based model checking. We prove a worst-case linear bound on the redundant work performed by our approach. Experimental results indicate that average case redundant work is much better than the worst-case. The implemented model checker has been used to verify a transition system that required more than 275 GBs of disk storage.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Stern, U., Dill, D.L.: Using magnetic disk instead of main memory in the Murφ verifier. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)
Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 526–540. Springer, Heidelberg (2005)
Korf, R., Schultze, P.: Large-scale parallel breadth-first search. In: Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2005), pp. 1380–1385 (2005)
Pelánek, R.: Typical structural properties of state spaces. In: [25], pp. 5–22
Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 259–274. Springer, Heidelberg (2001)
Gastin, P., Moro, P.: Minimal counterexample generation for spin. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 24–38. Springer, Heidelberg (2007)
Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. Formal Methods in System Design 7(3), 227–241 (1995)
Geldenhuys, J.: State caching reconsidered. In: [25], pp. 23–38
Kristensen, L.M., Mailund, T.: A compositional sweep-line state space exploration method. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 327–343. Springer, Heidelberg (2002)
Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)
Parashkevov, A.N., Yantchev, J.: Space efficient reachability analysis through use of pseudo-root states. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 50–64 (1997)
Zhou, R., Hansen, E.: Breadth-first heuristic search. Artificial Intelligence 170, 385–408 (2006)
Bao, T.: Empirical comparison of algorithms for model checking with magnetic disk. Technical Report VV-0402, Department of Computer Science, Brigham Young University (2004)
Jabbar, S., Edelkamp, S.: Parallel external directed model checking with linear I/O. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 237–251. Springer, Heidelberg (2005)
Penna, G.D., Intrigila, B., Tronci, E., Zilli, M.V.: Exploiting transition locality in the disk based Murφ verifier. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 202–219. Springer, Heidelberg (2002)
Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Integrating RAM and disk based verification within the Murphi verifier. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 277–282. Springer, Heidelberg (2003)
Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Exploiting transition locality in automatic verification of finite-state concurrent systems. International Journal on Software Tools for Technology Transfer 6(4), 320–341 (2004)
Zhou, R., Hansen, E.: Structured duplicate detection in external-memory graph search. In: McGuinness, D.L., Ferguson, G. (eds.) Proceedings of the 19th National Conference on Artificial Intelligence (AAAI 2004), San Jose, CA, pp. 683–688. AAAI Press / MIT Press (2004)
Hammer, M., Weber, M.: To Store or not to Store Reloaded: Reclaiming memory on demand. In: 11th International Workshop on Formal Methods for Industrial Critical Systems. Springer, Heidelberg (2006)
Dill, D.L.: The Murφ verification system. In: Alur, R., Henzinger, T. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Kumar, R., Mercer, E.G.: Load balancing parallel explicit state model checking. Electr. Notes Theor. Comput. Sci. 128(3), 19–34 (2005)
Lenoski, D.: DASH Prototype System. PhD thesis, Stanford University (1992)
Emerson, A.E., German, S., Havlicek, J., Venkataramani, A.: Model checking a parameterized directory-based cache protocol (2002)
Graf, S., Mounier, L. (eds.): SPIN 2004. LNCS, vol. 2989. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lamborn, P., Hansen, E.A. (2008). Layered Duplicate Detection in External-Memory Model Checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)