Abstract
We encountered some limits when using the GreatSPN model checker on life-size models, both in time and space complexity. Even when the exponential blow-up of state space size is adequately handled by the tool thanks to the use of a canonization function that allows to exploit system symmetries, time complexity becomes critical. Indeed the canonization procedure is computationally expensive, and verification time for a single property may exceed 2 days (without exhausting memory).
Using the GreatSPN model-checking core, we have built a distributed model-checker, dmcG, to benefit from the aggregated resources of a cluster. We built this distributed version using a flexible software architecture dedicated to parallel and distributed model-checking, thus allowing full reuse of GreatSPN source code at a low development cost. We report performances on several specifications that show we reach the theoretical linear speedup w.r.t. the number of nodes. Furthermore, through intensive use of multi-threading, performances on multi-processors architectures reach a speedup linear to the number of processors.
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
Burch, J., Clarke, E., McMillan, K.: Symbolic model checking: 1020 states and beyond. Information and Computation (Special issue for best papers from LICS90) 98(2), 153–181 (1992)
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: On well-formed coloured nets and their symbolic reachability graph. In: Jensen, K., Rozenberg, G. (eds.) Procedings of the 11th International Conference on Application and Theory of Petri Nets (ICATPN’90), Reprinted in High-Level Petri Nets, Theory and Application, Springer, Heidelberg (1991)
Ciardo, G., Luettgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)
Barnat, J., Forejt, V., Leucker, M., Weber, M.: DivSPIN - a SPIN compatible distributed model checker. In: Leucker, M., van de Pol, J., eds.: 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC’05), Lisbon, Portuga (2005)
Stern, U., Dill, D.L.: Parallelizing the Murϕ verifier. In: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 256–278. Springer, Heidelberg (1997)
Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol. 1680, Springer, Heidelberg (1999)
Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in eddy. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol. 3925, pp. 108–125. Springer, Heidelberg (2006)
Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. vol. 2057 (2001)
Thierry-Mieg, Y., llié, J.M., Poitrenaud, D.: A symbolic symbolic state space representation. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 276–291. Springer, Heidelberg (2004)
GreatSPN V2.0 (2007) http://www.di.unito.it/~greatspn/index.html
Hugues, J., Thierry-Mieg, Y., Kordon, F., Pautet, L., Baarir, S., Vergnaud, T.: On the Formal Verification of Middleware Behavioral Properties. In: 9th International Workshop on Formal Methods for Industrial Critical Systems (FMICS’04), pp. 139–157. Elsevier, Amsterdam (2004)
Bonnefoi, F., Hillah, L., Kordon, F., Frémont, G.: An approach to model variations of a scenario: Application to Intelligent Transport Systems. In: Workshop on Modelling of Objects, Components, and Agents (MOCA’06), Turku, Finland (2006)
Hamez, A., Kordon, F., Thierry-Mieg, Y.: libDMC: a library to Operate Efficient Distributed Model Checking. In: Workshop on Performance Optimization for High-Level Languages and Libraries - associated to IPDPS’2007, Long Beach, California, USA, IEEE Computer Society, Washington (2007)
Rangarajan, M., Dajani-Brown, S., Schloegel, K., Cofer, D.D.: Analysis of distributed spin applied to industrial-scale models. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol. 2989, pp. 267–285. Springer, Heidelberg (2004)
Message Passing Interface (2007) http://www.mpi-forum.org/
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley Longman Publishing Co., Inc.,, Boston, MA, USA (1995)
Duret-Lutz, A., Poitrenaud, D.: Spot: an extensible model checking library using transition-based generalized Büchi automata. In: Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS’04), Volendam, The Netherlands, pp. 76–83. IEEE Computer Society Press, Washington (2004)
Koufaty, D., Marr, D.T.: Hyperthreading Technology in the Netburst Microarchitecture. IEEE Micro 23(2), 56–65 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Hamez, A., Kordon, F., Thierry-Mieg, Y., Legond-Aubry, F. (2007). dmcG: A Distributed Symbolic Model Checker Based on GreatSPN. In: Kleijn, J., Yakovlev, A. (eds) Petri Nets and Other Models of Concurrency – ICATPN 2007. ICATPN 2007. Lecture Notes in Computer Science, vol 4546. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73094-1_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-73094-1_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73093-4
Online ISBN: 978-3-540-73094-1
eBook Packages: Computer ScienceComputer Science (R0)