More Web Proxy on the site http://driver.im/

Article

An overview of the mCRL2 toolset and its recent advances

Authors:

Jan Friso Groote,

Jeroen J. A. Keiren,

Frank P. M. Stappers,

Erik P. de Vink,

Wieger Wesselink,

Tim A. C. WillemseAuthors Info & Claims

TACAS'13: Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems

Pages 199 - 213

https://doi.org/10.1007/978-3-642-36742-7_15

Published: 16 March 2013 Publication History

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.

References

[1]

Arbab, F.: Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), 329-366 (2004)

Digital Library

[2]

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)

Digital Library

[3]

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)

[4]

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)

[5]

Bhat, G., Cleaveland, R.: Efficient model checking via the equational µ-calculus. In: LICS, pp. 304-312. IEEE Computer Society (1996)

Digital Library

[6]

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)

Digital Library

[7]

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)

Digital Library

[8]

Bodei, C., et al.: Automatic validation of protocol narration. In: CSFW 2003, pp. 126-140. IEEE (2003)

[9]

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)

Digital Library

[10]

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)

Digital Library

[11]

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)

[12]

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)

[13]

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)

Digital Library

[14]

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)

Digital Library

[15]

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)

[16]

De Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science 37, 245-267 (1985)

[17]

Emerson, E. A., Jutla, C. S.: Tree automata, mu-calculus and determinacy. In: FOCS 1991, pp. 368-377. IEEE (1991)

Digital Library

[18]

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)

[19]

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)

Digital Library

[20]

Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)

Digital Library

[21]

Groote, J. F., Ponse, A., Usenko, Y. S.: Linearization in parallel pCRL. Journal of Logic and Algebraic Programming 48(1-2), 39-70 (2001)

[22]

Groote, J. F., Willemse, T. A.C.: Model-checking processes with data. Science of Computer Programming 56(3), 251-273 (2005)

Digital Library

[23]

Groote, J. F., Willemse, T. A.C.: Parameterised Boolean equation systems. Theoretical Computer Science 343(3), 332-369 (2005)

Digital Library

[24]

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)

Digital Library

[25]

Holzmann, G. J.: The SPIN model checker: Primer and reference manual. Addison-Wesley (2003)

Digital Library

[26]

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)

[27]

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)

Digital Library

[28]

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)

[29]

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)

Digital Library

[30]

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)

Digital Library

[31]

Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universität München (1997)

[32]

Mellor, S. J., Balcer, M. J.: Executable UML: A Foundation for Model-Driven Architecture. Addison-Wesly (2002)

Digital Library

[33]

van den Nieuwelaar, N. J. M.: Supervisory Machine Control by Predictive-reactive Scheduling. PhD thesis, Eindhoven University of Technology (2004)

[34]

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)

Digital Library

[35]

Orzan, S. M., Willemse, T. A.C.: Invariants for parameterised Boolean equation systems. Theoretical Computer Science 411(11-13), 1338-1371 (2010)

Digital Library

[36]

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)

Digital Library

[37]

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)

Digital Library

[38]

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)

[39]

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)

Digital Library

[40]

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)

Digital Library

[41]

Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice Hall (1998)

Digital Library

[42]

Shoham, S., Grumberg, O.: 3-valued abstraction: more precision at less cost. Information and Computation 206(11), 1313-1333 (2008)

Digital Library

[43]

Stappers, F. P. M.: Bridging Formal Models: An Engineering Perspective. PhD thesis, Eindhoven University of Technology (2012)

[44]

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)

Digital Library

[45]

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.) SLE2011. LNCS, vol. 6940, pp. 223-242. Springer, Heidelberg (2012)

Digital Library

[46]

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)

Digital Library

[47]

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)

Digital Library

[48]

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)

[49]

van de Weerdenburg, M.: Efficient Rewriting Techniques. PhD thesis, Eindhoven University of Technology (2009)

[50]

Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135-183 (1998)

Digital Library

Cited By

van Laarhoven JBunte Ovan Gool LWillemse T(2024)Formalising the Industrial Language SMMT in mCRL2Formal Methods for Industrial Critical Systems10.1007/978-3-031-68150-9_4(63-79)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68150-9_4
Dilley NLange JGrundy J(2021)Automated verification of go programs via bounded model checkingProceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE51524.2021.9678571(1016-1027)Online publication date: 15-Nov-2021
https://dl.acm.org/doi/10.1109/ASE51524.2021.9678571
Wolf FArquint LClochard MOortwijn WPereira JMüller P(2021)Gobra: Modular Specification and Verification of Go ProgramsComputer Aided Verification10.1007/978-3-030-81685-8_17(367-379)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_17
Show More Cited By

An overview of the mCRL2 toolset and its recent advances
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation

Recommendations

Experiences in developing the mCRL2 toolset

This paper presents practices and experiences in developing the formal methods toolset mCRL2. Findings are presented based on years of experiences in developing tools in an academic environment. Practical problems and ways to solve them are discussed. ...
The TASM toolset: specification, simulation, and formal verification of real-time systems
CAV'07: Proceedings of the 19th international conference on Computer aided verification

In this paper, we describe the features of the Timed Abstract State Machine toolset. The toolset implements the features of the Timed Abstract State Machine (TASM) language, a specification language for reactive real-time systems. The TASM language ...
An Easily Extensible Toolset for Tabular Mathematical Expressions
TACAS '99: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems

We describe the design of an open ended set of tools for manipulating multi-dimensional tabular expressions. The heart of the toolset is a set of modules that makes it possible to add new tools to the toolset without having detailed knowledge of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS'13: Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems

March 2013

643 pages

ISBN:9783642367410

Editors:
Nir Piterman
Department of Computer Science, University of Leicester, University Road, Leicester, UK
,
Scott A. Smolka
Department of Computer Science, State University of New York at Stony Brook, University Road, Stony Brook, NY

Sponsors

Sapienza: Sapienza University of Rome

In-Cooperation

EAPLS: European Association for Programming Languages and Systems
EATCS: European Association for Theoretical Computer Science
European Association of Software Science and Technology

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 16 March 2013

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

van Laarhoven JBunte Ovan Gool LWillemse T(2024)Formalising the Industrial Language SMMT in mCRL2Formal Methods for Industrial Critical Systems10.1007/978-3-031-68150-9_4(63-79)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68150-9_4
Dilley NLange JGrundy J(2021)Automated verification of go programs via bounded model checkingProceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE51524.2021.9678571(1016-1027)Online publication date: 15-Nov-2021
https://dl.acm.org/doi/10.1109/ASE51524.2021.9678571
Wolf FArquint LClochard MOortwijn WPereira JMüller P(2021)Gobra: Modular Specification and Verification of Go ProgramsComputer Aided Verification10.1007/978-3-030-81685-8_17(367-379)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_17
Sprenger CKlenze TEilers MWolf FMüller PClochard MBasin D(2020)Igloo: soundly linking compositional refinement and separation logic for distributed system verificationProceedings of the ACM on Programming Languages10.1145/34282204:OOPSLA(1-31)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428220
Basile Dter Beek MFantechi AFerrari AGnesi SMasullo LMazzanti FPiattino ATrentini D(2020)Designing a Demonstrator of Formal Methods for Railways Infrastructure ManagersLeveraging Applications of Formal Methods, Verification and Validation: Applications10.1007/978-3-030-61467-6_30(467-485)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-61467-6_30
Lapauw RBruynooghe MDenecker M(2020)Improving Parity Game Solvers with JustificationsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_21(449-470)Online publication date: 16-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39322-9_21
Scalas AYoshida NBenussi EBrachthäuser JRyu SNystrom N(2019)EffpiProceedings of the Tenth ACM SIGPLAN Symposium on Scala10.1145/3337932.3338812(27-31)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.1145/3337932.3338812
Beek MDamiani FLienhardt MMazzanti FPaolini L(2019)Static Analysis of Featured Transition SystemsProceedings of the 23rd International Systems and Software Product Line Conference - Volume A10.1145/3336294.3336295(39-51)Online publication date: 9-Sep-2019
https://dl.acm.org/doi/10.1145/3336294.3336295
Abadi MKeidar-Barner SPidan DVeksler T(2019)Verifying Parallel Code After Refactoring Using Equivalence CheckingInternational Journal of Parallel Programming10.1007/s10766-017-0548-447:1(59-73)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10766-017-0548-4
Basile Dter Beek MPugliese R(2019)Bridging the Gap Between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and ChoreographiesCoordination Models and Languages10.1007/978-3-030-22397-7_8(129-147)Online publication date: 17-Jun-2019
https://dl.acm.org/doi/10.1007/978-3-030-22397-7_8
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten