The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability
Reasoning about the correctness of parallel and distributed systems requires automated tools. By now, the mCRL2 toolset and language have been developed over a course of more than fifteen years. In this paper, we report on the progress and advancements over the past six years. Firstly, the mCRL2 language has been extended to support the modelling of probabilistic behaviour. Furthermore, the usability has been improved with the addition of refinement checking, counterexample generation and a user-friendly GUI. Finally, several performance improvements have been made in the treatment of behavioural equivalences. Besides the changes to the toolset itself, we cover recent applications of mCRL2 in software product line engineering and the use of domain specific languages (DSLs).
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | |||
10:30 30mTalk | Multi-Core On-The-Fly Saturation TACAS Link to publication | ||
11:00 30mTalk | Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude TACAS Link to publication | ||
11:30 30mTalk | The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability TACAS Olav Bunte , Jan Friso Groote , Jeroen J.A. Keiren , Maurice Laveaux , Thomas Neele , Erik P. de Vink , Wieger Wesselink , Anton Wijs Eindhoven University of Technology, Tim A.C. Willemse Link to publication | ||
12:00 30mTalk | Checking Deadlock-Freedom of Parametric Component-Based Systems TACAS Marius Bozga Verimag/CNRS, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Joseph Sifakis Verimag/CNRS Link to publication |