A language and tool set to study communicating processes with data
µCRL (micro CRL - written as mCRL if the symbol µ is not available) is a process algebraic language that was especially developed to take account of data in the study of communicating processes. It is basically intended to study description and analysis techniques for (large) distributed systems.
Basic process algebras such as CCS, CSP, and ACP are well suited for the study of elementary behavioural properties of communicating systems. However, when it comes to the study of more realistic systems these languages turn out to be less adequate. One main problem is that process algebras tend to lack the ability to handle data. To accommodate data in these theories one has to take resort to infinite sets of equations where variables are indexed with data values.
µCRL solves this problem in a simple but powerful way. Data are defined by means of equational abstract data types. Data of this kind are integrated in the process algebra ACP, by allowing process variables and actions to be parameterised with data. Moreover a conditional (if-then-else construct) can be used to have data influence the course of a process, and alternative quantification is added to sum over possibly infinitely many data elements of some data type.
µCRL turns out to be remarkably apt for the analysis of large distributed systems. It has been the basis for the development of a proof theory and proof methodology (the cone and foci method) that can be used to verify communication protocols in a precise logical way (allowing the proof to be checked by proof checkers such as Coq and PVS). The use of this method slowly turns verification into a routine.
The cone and foci method was applied to leader election protocols, distributed summing protocols, production cells, remote control protocols, etc..... We found that all these protocols contained flaws of a more or less serious nature and that µCRL was well suited to detect these problems.
More recently, the language has been extended with features to express time. Time could be added to µCRL by introducing just one single main operator, and one single auxiliary operator. This new language turned out sufficiently versatile to model hybrid systems and prove these correct. Systems with a complex control structure (which is generally absent in hybrid systems) give more difficulties.
The use of µCRL is supported by a collection of tools, the µCRL toolset. This toolset is built around a linearized form of µCRL, the so called Linear Process Operator (LPO) format. The µCRL toolset currently comprises a well-formedness checker, a linearizer, a simulator, a state space generator as well as a few tools to analyze and optimize LPOs. The generated state space can be read, visualized and manipulated by VASY's Cæsar/Aldébaran Development Package (CADP).
The µCRL toolkit is available from our download page under the conditions stated in the license. A tutorial is included in the distribution and manual pages are available on line