The mCRL2 toolset

Modeling and analysis of communicating systems (book)

mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols. It can be run on Windows, Linux, Apple MacOS and FreeBSD.

The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.

The mCRL2 toolset is developed at the department of Mathematics and Computer Science of the Technische Universiteit Eindhoven, in collaboration with the University of Twente.

Warning

In the latest release, mCRL2 202407.1, the tool lpsxsim does not work on Ubuntu. This will be fixed in the next release, but in the meantime the nightly builds can be used.

Note

The latest release, mCRL2 202407.1, is now available from the Download mCRL2 page. This release contains a critical bug fix for the mCRL2 ide. See the changelog for a detailed list of changes.

Note

Listen to the Parallel Rhapsody (thanks to Frederik Gosewehr and Gert Veltink).

Note

Understanding Behaviour of Distributed Systems using mCRL2 (book)

A new introductory book appeared, describing the mCRL2 specification language, the modal mu-calculus and the extensive toolset around these. The book is full of examples, varying from games to distributed algorithms. It is shown how such games can be solved, and how the (in)correctness of such algorithms can be understood.

Note

FORTE 2022 Best Artefact Award: Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2. By Arshad, Horne, Johansen, Owe and Willemse.

Note

A tool paper explaining the latest developments in mCRL2 was published in TACAS2019. The new features include counterexamples, probabilistic processes and efficient algorithms for several types of behavioural relations. As part of the review process, mCRL2 was tested and accepted by the TACAS artefact evaluation committee. The paper is available under open access.

Note

On Coursera four consecutive courses consisting of approximately 60 lectures provide an introduction into the theory and practical use of the mCRL2 toolset. It is based on the book ‘Modeling and Analysis of Communicating Systems’ shown above. The courses are:

The slides used to make these courses are available by contacting J.F.Groote@tue.nl. They can also be downloaded from MIT Press.

Note

mCRL2 is used by the company Verum as their verification engine. Verum provides model based software development environments for the languages ASD and Dezyne that allow to program proven correct embedded software with much less effort than “classical” programming. As it stands Verum is the industry leader in reliable software design.

The mCRL2 project uses TeamCity for regression testing during development and building the daily snapshots.