Abstract
Model checking is widely used as an automatic exhaustive verification technique to check properties of complex systems. However, it is difficult to operate in the context of today’s emerging systems that combine distribution (and asynchronous communications) together with a large size (and a hierarchical composition of components – and thus, of specifications).
This paper combines existing techniques tackling the known combinatorial explosion of model checking. To achieve this, we exploit the structure of such distributed systems (symmetries and hierarchical composition), thus allowing a better compression factor and calculus factorization in favorable cases. We present these techniques and assess their impact on some benchmark examples.
This work was partially supported by a grant from the Direction Générale pour l’Armement.
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
Babar, J., Beccuti, M., Donatelli, S., Miner, A.S.: GreatSPN Enhanced with Decision Diagram Data Structures. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 308–317. Springer, Heidelberg (2010)
Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic Counter Abstraction for Concurrent Software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 64–78. Springer, Heidelberg (2009)
Bošnački, D., Holzmann, G.J.: Improving Spin’s Partial-Order Reduction for Breadth-First Search. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 91–105. Springer, Heidelberg (2005)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., Mcmillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 States and beyond. Information and computation 98(2), 142–170 (1992)
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed coloured nets for symmetric modelling applications. IEEE Transactions on Computers 42(11), 1343–1360 (1993)
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)
Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1), 77–104 (1996)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Crocodile: A Symbolic/Symbolic Tool for the Analysis of Symmetric Nets with Bag. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol. 6709, pp. 338–347. Springer, Heidelberg (2011)
Colange, M., Kordon, F., Thierry-Mieg, Y., Baarir, S.: State Space Analysis using Symmetries on Decision Diagrams. In: 12th International Conference on Application of Concurrency to System Design (ACSD 2012), pp. 164–172. IEEE Computer Society, Hamburg (2012)
Cosyverif: a verification environment (2012), http://www.cosyverif.org
Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data Decision Diagrams for Petri Net Analysis. In: Esparza, J., Lakos, C. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 101–120. Springer, Heidelberg (2002)
Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical Decision Diagrams to Exploit Model Structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443–457. Springer, Heidelberg (2005)
Girault, C., Valk, R.: Petri Nets for Systems Engineering. Springer (2003) ISBN: 3-540-41217-4
Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, LICS 1991, pp. 406–415 (July 1991)
GreatSPN: Petri nets suite (2012), http://www.di.unito.it/~greatspn
Haddad, S., Kordon, F., Petrucci, L., Pradat-Peyre, J., Treves, L.: Efficient state-based analysis by introducing bags in petri nets color domains. In: American Control Conference, ACC 2009, pp. 5018–5025. IEEE (2009)
Hamez, A., Thierry-Mieg, Y., Kordon, F.: Building efficient model checkers using hierarchical set decision diagrams and automatic saturation. Fundamenta Informaticae 94(3-4), 413–437 (2009)
Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a Hierarchical Static Order for Decision Diagram-Based Representation from P/T Nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 121–140. Springer, Heidelberg (2012)
Jensen, K.: Coloured Petri nets and the invariant-method. Theor. Comput. Sci. 14, 317–336 (1981)
Jensen, K., Kristensen, L.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer (2009) ISBN: ISBN 978-3-642-00283-0
Junttila, T.: On the Symmetry Reduction Method for Petri Nets and similar formalisms. Ph.D. thesis, Helsinki University of Technology, Espoo, Finland (2003)
libits (2012), http://move.lip6.fr/software/DDD
Muschevici, R., Proença, J., Clarke, D.: Modular Modelling of Software Product Lines with Feature Nets. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 318–333. Springer, Heidelberg (2011)
Tanenbaum, A.: Operating Systems: Design and Implementation. Prentice Hall (1987)
Thierry-Mieg, Y., Dutheillet, C., Mounier, I.: Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 82–101. Springer, Heidelberg (2003)
Thierry-Mieg, Y., Ilié, 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)
Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical Set Decision Diagrams and Regular Models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 1–15. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colange, M., Hillah, LM., Kordon, F., Parutto, P. (2012). Extreme Symmetries in Complex Distributed Systems: The Bag-Oriented Approach. In: Calinescu, R., Garlan, D. (eds) Large-Scale Complex IT Systems. Development, Operation and Management. Monterey Workshop 2012. Lecture Notes in Computer Science, vol 7539. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34059-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-34059-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34058-1
Online ISBN: 978-3-642-34059-8
eBook Packages: Computer ScienceComputer Science (R0)