mCRL: A Toolset to Analyse Algebraic Specifications

Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


mCRL is a language for specifying and verifying distributed systems in an algebraic fashion. It targets the specification of system behaviour in a process-algebraic style and of data elements in the form of abstract data types. The mCRL toolset supports the analysis and manipulation of mCRL specifications. A mCRL specification can be automatically transformed into a linear process operator (LPO). All other tools in the mCRL toolset use LPOs as their starting point. The simulator allows the interactive simulation of an LPO. There are a number of tools that allow optimisations on the level of LPOs. The instantiator generates a labelled transition system from an LPO, which can be visualised, analysed and minimised.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems