Abstract
In the life cycle of any software system, a crucial phase of formalization and validation by means of verification and/or testing leads to the identification of probable errors infiltrated during its design. Model checking is one of the formal verification techniques. This technique is very powerful, but limited by the state explosion problem that occurs when the model to be checked is too large, and cannot be verified for lack of memory space. In this article, we cite two solutions, parallel and distributed, which aim to reduce the state space explosion. A comparative study between these approaches is carried out on a counters model.
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
Adelson-Velskii, G. and Landis, E. M. An algorithm for the organization of in-formation. In Proceedings of the USSR Academy of Sciences, volume 45, pages:1259–1263, 1962.
Allal, L., Belalem, G., Dhaussy, P. and Teodorov, C. A parallel algorithm for the state space exploration. Scalable Computing: Practice and Experience, 17(2):129–142, 2016.
Clarke, E. M., Grumberg, O., Jha, S., Lu, Y. and Veith, H. Progress on the state explosion problem in model checking. In Informatics - 10 Years Back. 10 Years Ahead. pages 176–194, London, UK, UK, 2001. Springer-Verlag.
Clarke, E. M., Klieber, W., Novácek, M. and Zuliani, P. Model checking and the state explosion problem. In Proceedings of the 8th Laser Summer School on Software Engineering, volume 7682, pages 1–30, September 2011.
Gosling, J., Joy, B., Steele, G. L., Bracha, G. and Buckley, A. The Java Language Specification, Java SE 8 Edition. 2014.
Guan, N., Gu, Z., Yi, W. and Yu, G. Improving scalability of model-checking for minimizing buffer requirements of synchronous dataflow graphs. In Proceedings of the 14th Asia and South Pacific Design Automation Conference, ASP-DAC’09, pages 715–720, 2009.
Holzmann, G.J. Parallelizing the spin model checker. In Proceedings of the 19th International Conference on Model Checking Software, SPIN’12, pages 155–171, Berlin, 2012.
Jensen, K. Coloured petri nets-basic concepts analysis methods and practical use. Monographs in Theoretical Computer Science. An EATCS Series, 3, 1994.
Kristensen L.M. and Petrucci, L. An approach to distributed space exploration for coloured petri nets*. In Proceedings of the 25th International Conference on Applications and Theory of Petri Nets, volume 3099 of ICATPN’04, pages 474–483, June 2004.
Lerda, F. and Sisto, R. Distributed-memory model-checking with spin. In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, volume 1680, pages 22–39, July 1999.
Pelánek, R. Fighting state space explosion: Review and evaluation. In Proceedings of the 13th on Formal Methods for Industrial Critical Systems, volume 5596 of FMICS’08, pages 37–52, September 2008.
Saad, R.T., Zilio, S.D. and Berthomieu, B. A general lock free algorithm for parallel state space construction. In Proceedings of the 9th International Workshop on Parallel and Distributed Methods in Verification, PDMC-HIBI’10, pages 8–16, October 2010.
Subramoni, H., Petrini, F., Agarwal, V. and D. Pasetto. Intra-socket and inter-socket communication in multi-core systems. Computer Architecture Letters, 9(1):13–16, 2010.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Allal, L., Belalem, G., Dhaussy, P., Teodorov, C. (2018). Using Parallel and Distributed Reachability in Model Checking. In: Perez, G., Tiwari, S., Trivedi, M., Mishra, K. (eds) Ambient Communications and Computer Systems. Advances in Intelligent Systems and Computing, vol 696. Springer, Singapore. https://doi.org/10.1007/978-981-10-7386-1_12
Download citation
DOI: https://doi.org/10.1007/978-981-10-7386-1_12
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-7385-4
Online ISBN: 978-981-10-7386-1
eBook Packages: EngineeringEngineering (R0)