Abstract
The analysis of complex distributed systems requires dedicated software tools. The mCRL language and toolset have been developed to support such analysis. We highlight changes and improvements made to the toolset in recent years. On the one hand, these affect the scope of application, which has been broadened with extended support for data structures like infinite sets and functions. On the other hand, considerable progress has been made regarding the performance of our tools for state space generation and model checking, due to improvements in symbolic reduction techniques and due to a shift towards parity game-based solving. We also discuss the software architecture of the toolset, which was well suited to accommodate the above changes, and we address a number of case studies to illustrate the approach.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arbab, F.: Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), 329–366 (2004)
Barnat, J., Brim, L., Ročkai, P.: DiVinE Multi-Core – A Parallel LTL Model-Checker. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 234–239. Springer, Heidelberg (2008)
van Beek, D.A., et al.: Syntax and consistent equation semantics of hybrid Chi. Journal of Logic and Algebraic Programming 68(1-2), 129–210 (2006)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Bhat, G., Cleaveland, R.: Efficient model checking via the equational μ-calculus. In: LICS, pp. 304–312. IEEE Computer Society (1996)
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)
Blom, S., Fokkink, W., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: μCRL: A Toolset for Analysing Algebraic Specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)
Bodei, C., et al.: Automatic validation of protocol narration. In: CSFW 2003, pp. 126–140. IEEE (2003)
Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 120–135. Springer, Heidelberg (2007)
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)
Cranen, S.: Model Checking the FlexRay Startup Phase. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 131–145. Springer, Heidelberg (2012)
Cranen, S., Groote, J.F., Reniers, M.A.: A linear translation from CTL* to the first-order modal μ-calculus. Theoretical Computer Science 412, 3129–3139 (2011)
Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: Stuttering Mostly Speeds Up Solving Parity Games. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 207–221. Springer, Heidelberg (2011)
Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: A Cure for Stuttering Parity Games. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 198–212. Springer, Heidelberg (2012)
Cranen, S., Gazda, M.W., Wesselink, J.W., Willemse, T.A.C.: Abstraction in parameterised boolean equation systems. Technical Report 13-01, Eindhoven University of Technology (2013)
De Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science 37, 245–267 (1985)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: FOCS 1991, pp. 368–377. IEEE (1991)
Franek, B., Gaspar, C.: SMI++ object-oriented framework for designing and implementing distributed control systems. IEEE Transactions on Nuclear Science 52(4), 891–895 (2005)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Groote, J.F., Ponse, A., Usenko, Y.S.: Linearization in parallel pCRL. Journal of Logic and Algebraic Programming 48(1-2), 39–70 (2001)
Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Science of Computer Programming 56(3), 251–273 (2005)
Groote, J.F., Willemse, T.A.C.: Parameterised Boolean equation systems. Theoretical Computer Science 343(3), 332–369 (2005)
van Ham, F., van de Wetering, H., van Wijk, J.J.: Visualization of state transition graphs. In: Andrews, K., et al. (eds.) INFOVIS 2001, pp. 59–63 (2001)
Holzmann, G.J.: The SPIN model checker: Primer and reference manual. Addison-Wesley (2003)
Janin, D., Lenzi, G.: Relating levels of the mu-calculus hierarchy and levels of the monadic hierarchy. In: LICS 2001, pp. 347–356. IEEE (2001)
Jurdziński, M.: Small Progress Measures for Solving Parity Games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Kant, G., van de Pol, J.: Efficient instantiation of parameterised boolean equation systems to parity games. In: Proc. GRAPHITE 2012. EPTCS, vol. 99, pp. 50–65 (2012)
Keiren, J.J.A., Willemse, T.A.C.: Bisimulation Minimisations for Boolean Equation Systems. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 102–116. Springer, Heidelberg (2011)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002)
Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universität München (1997)
Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model-Driven Architecture. Addison-Wesly (2002)
van den Nieuwelaar, N.J.M.: Supervisory Machine Control by Predictive-reactive Scheduling. PhD thesis, Eindhoven University of Technology (2004)
Orzan, S., Wesselink, W., Willemse, T.A.C.: Static Analysis Techniques for Parameterised Boolean Equation Systems. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 230–245. Springer, Heidelberg (2009)
Orzan, S.M., Willemse, T.A.C.: Invariants for parameterised Boolean equation systems. Theoretical Computer Science 411(11-13), 1338–1371 (2010)
Ploeger, B., Wesselink, W., Willemse, T.A.C.: Verification of reactive systems via instantiation of parameterised Boolean equation systems. Information and Computation 209(4), 637–663 (2011)
van de Pol, J.: JITty: A Rewriter with Strategy Annotations. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 367–370. Springer, Heidelberg (2002)
van de Pol, J., Espada, M.V.: Modal Abstractions in μCRL. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 409–425. Springer, Heidelberg (2004)
Pretorius, A.J., van Wijk, J.J.: Bridging the semantic gap: Visualizing transition graphs with user-defined diagrams. IEEE Computer Graphics and Applications 27, 58–66 (2007)
Remenska, D., Willemse, T.A.C., Verstoep, K., Fokkink, W., Templon, J., Bal, H.: Using model checking to analyze the system behavior of the LHC production grid. In: CCGrid 2012, pp. 335–343. IEEE (2012)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1998)
Shoham, S., Grumberg, O.: 3-valued abstraction: more precision at less cost. Information and Computation 206(11), 1313–1333 (2008)
Stappers, F.P.M.: Bridging Formal Models: An Engineering Perspective. PhD thesis, Eindhoven University of Technology (2012)
Stappers, F.P.M., Reniers, M.A., Weber, S.: Transforming SOS Specifications to Linear Processes. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 196–211. Springer, Heidelberg (2011)
Stappers, F.P.M., Weber, S., Reniers, M.A., Andova, S., Nagy, I.: Formalizing a Domain Specific Language Using SOS: An Industrial Case Study. In: Sloane, A., Aßmann, U. (eds.) SLE 2011. LNCS, vol. 6940, pp. 223–242. Springer, Heidelberg (2012)
Stappers, F.P.M., Reniers, M.A., Groote, J.F., Weber, S.: Dogfooding the formal semantics of mCRL2. In: Bowen, J., Zhu, H. (eds.) 35th SEW. IEEE (2012) (to appear)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Weber, M., Kindler, E.: The Petri Net Markup Language. In: Ehrig, H., Reisig, W., Rozenberg, G., Weber, H. (eds.) Petri Net Technology for Communication-Based Systems. LNCS, vol. 2472, pp. 124–144. Springer, Heidelberg (2003)
van de Weerdenburg, M.: Efficient Rewriting Techniques. PhD thesis, Eindhoven University of Technology (2009)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cranen, S. et al. (2013). An Overview of the mCRL2 Toolset and Its Recent Advances. In: Piterman, N., Smolka, S.A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. Lecture Notes in Computer Science, vol 7795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36742-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-36742-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36741-0
Online ISBN: 978-3-642-36742-7
eBook Packages: Computer ScienceComputer Science (R0)