Abstract
In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a distance-preserving abstraction for concurrent systems that allows one to compute an interesting estimate of the error distance without hitting the state explosion problem. Our experiments show a dramatic reduction both in the number of states explored by the model checker and in the total runtime.
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.
Similar content being viewed by others
References
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in uppaal. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)
Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Design Automation Conference, pp. 29–34 (2000)
Dierks, H.: Comparing model checking and logical reasoning for real-time systems. Formal Aspects of Computing 16(2), 104–120 (2004)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Software Tools for Technology Transfer (2003)
Edelkamp, S., Lluch-Lafuente, A.: Abstraction databases in theory and model checking. In: Proc. ICAPS Workshop on Connecting Planning Theory with Practice (June 2004)
Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. Electr. Notes Theor. Comput. Sci. 55(3) (2001)
Graf, S., Steffen, B., Lüttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computing 8, 607–616 (1996)
Groce, A., Visser, W.: Heuristics for model checking Java programs. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 242–245. Springer, Heidelberg (2002)
Kaltenbach, M., Misra, J.: A theory of hints in model checking. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 423–438. Springer, Heidelberg (2003)
Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Baer, A.: The UniForM workbench, a universal development environment for formal methods. In: Wing, J., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, p. 1186. Springer, Heidelberg (1999)
Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 35–52. Springer, Heidelberg (2006)
Lafuente, A.L.: Directed Search for the Verification of Communication Protocols. PhD thesis, Institute of Computer Science, University of Freiburg (June 2003)
Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. STTT – International Journal on Software Tools for Technology Transfer 1(1, 2), 134–152 (1997)
Matsumoto, M., Nishimura, T.: Mersenne Twister: A 623-dimensionally equidistributed uniform pseudo-random number generator. ACM Transactions on Modeling and Computer Simulation 8(1), 3–30 (1998)
Pearl, J.: Heuristics. Morgan Kaufmann, San Francisco (1983)
Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 497–511. Springer, Heidelberg (2004)
Sabnani, K.K., Lapone, A.M., Uyar, M.Ü.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940–948 (1989)
Seitz, C.: Ideas about arbiters. Lambda, 10–14 (1980)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Design Automation Conference, pp. 599–604 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dräger, K., Finkbeiner, B., Podelski, A. (2006). Directed Model Checking with Distance-Preserving Abstractions. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_2
Download citation
DOI: https://doi.org/10.1007/11691617_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33102-5
Online ISBN: 978-3-540-33103-2
eBook Packages: Computer ScienceComputer Science (R0)