Abstract
Directed model checking uses distance functions to guide the state space exploration to efficiently find short error paths. Distance functions based on delete-relaxation have successfully been used for, e. g., model checking timed automata. However, such distance functions have not been investigated for formalisms with rich expression languages as provided by PROMELA. We present a generalization of delete-relaxation-based distance functions to a subclass of PROMELA. We have evaluated the resulting search behavior on a large number of models from the BEEM database within the HSF-SPIN model checker. Our experiments show significantly better guidance compared to the previously best distance function available in HSF-SPIN.
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
References
Bonet, B., Geffner, H.: Planning as heuristic search. AIJ 129(1–2), 5–33 (2001)
Bylander, T.: The computational complexity of propositional STRIPS planning. AIJ 69(1–2), 165–204 (1994)
Edelkamp, S., Leue, S., et al.: Directed explicit-state model checking in the validation of communication protocols. STTT 5(2–3), 247–267 (2004)
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)
Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster than Uppaal? In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 552–555. Springer, Heidelberg (2008)
Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)
Acknowledgments
The authors thank G. J. Holzmann for valuable clarifications of semantical and technical questions on PROMELA and SPIN.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Andisha, A.S., Wehrle, M., Westphal, B. (2015). Directed Model Checking for PROMELA with Relaxation-Based Distance Functions. In: Fischer, B., Geldenhuys, J. (eds) Model Checking Software. SPIN 2015. Lecture Notes in Computer Science(), vol 9232. Springer, Cham. https://doi.org/10.1007/978-3-319-23404-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-23404-5_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23403-8
Online ISBN: 978-3-319-23404-5
eBook Packages: Computer ScienceComputer Science (R0)