Abstract
This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values.
We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.
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
van der Berg, F.I., Laarman, A.W.: SpinS: Extending LTSmin with Promela through SpinJa. ENTCS 296(2012), 95–105 (2013); pASM/PDMC 2012
Blom, S., van de Pol, J.: Symbolic Reachability for Process Algebras with Recursive Data Types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81–95. Springer, Heidelberg (2008)
Blom, S., van de Pol, J., Weber, M.: Bridging the Gap between Enumerative and Symbolic Model Checkers. Technical Report CTIT, University of Twente, Enschede (2009), http://eprints.eemcs.utwente.nl/15703/
Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and Symbolic Reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991 (1991)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: LICS 1990. IEEE (1990)
Ciardo, G., Marmorstein, R., Siminiceanu, R.I.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)
Ciardo, G., Yu, A.J.: Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 146–161. Springer, Heidelberg (2005)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. STTT 2(4) (2000)
Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1–26. Springer, Heidelberg (2008)
Kordon, F., Linard, A., Beccuti, M., Buchs, D., Fronc, L., Hillah, L.M., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A.: et al.: Model Checking Contest @ Petri Nets, Report on the 2013 edition (2013), ArXiv: http://arxiv.org/abs/1309.2485v1
McMillan, K.L.: Symbolic model checking. Kluwer (1993)
Meijer, J.J.G.: Improving Reachability Analysis in LTSmin. Master’s thesis, University of Twente (2014)
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)
Rudell, R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. In: ICCAD 1993. IEEE (1993)
Skiena, S.S.: The Algorithm Design Manual. Springer (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Meijer, J., Kant, G., Blom, S., van de Pol, J. (2014). Read, Write and Copy Dependencies for Symbolic Model Checking. In: Yahav, E. (eds) Hardware and Software: Verification and Testing. HVC 2014. Lecture Notes in Computer Science, vol 8855. Springer, Cham. https://doi.org/10.1007/978-3-319-13338-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-13338-6_16
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-13337-9
Online ISBN: 978-3-319-13338-6
eBook Packages: Computer ScienceComputer Science (R0)