Views
User manual/Toolset overview
From MCRL2
| User manual |
|
Contents |
Introduction
An overview of the mCRL2 toolset is given in the picture below. It shows the main concepts that play a role (in blue) and the operations that can be performed on these concepts (in red). In the toolset, a file format is associated with every concept and operations are implemented in tools. In order to get a feeling for the relevant concepts and tools, we describe the workflow of a typical analysis using mCRL2 below.
All tools can be accessed via a command-line interface. Another possibility is to use the mcrl2-gui tool which provides access to the tools via a GUI.
mCRL2 specification and linearisation
Every analysis starts off by specifying the behaviour of the system being studied. This can be any kind of system, though the main application of mCRL2 is in distributed software systems. The specification can be seen as a model of the real system: it is a simplified, or abstracted version of reality. Obtaining a specification that is faithful to the real system is far from trivial and beyond the scope of this overview.
An mCRL2 specification is a plain-text file containing a model in the mCRL2 language. It can be created using any text editor. For a description of the mCRL2 language we refer to the Language reference.
Typically, the specification of a distributed system contains several processes that run in parallel. The first step in the mCRL2 analysis process is to linearise this specification to obtain a Linear Process Specification (LPS). This is an mCRL2 specification from which all parallelism has been removed. All that remains is a series of condition -- action -- effect rules that specify how the system as a whole reacts to certain stimuli given its current state. Because of its much simpler form, the LPS is much more suitable for automated analysis than an mCRL2 specification. Therefore, most tools in the mCRL2 toolset operate on LPSs.
The main tool for linearisation is mcrl22lps. Given an mCRL2 specification, it produces an equivalent LPS on which other tools can be run. We investigate these tools below.
LPS tools
An LPS is stored in a binary file format for efficiency. After having obtained an LPS, a very useful analysis method is by simulating the model. Starting from the initial state, sequences of actions can be performed which can quickly reveal unexpected or erroneous behaviour. It is also a good way of getting acquainted with the modelled behaviour.
The mCRL2 toolset contains two tools for simulation of an LPS: sim (command-line interface) and xsim (graphical user interface).
Some statistical information about an LPS can be collected using the lpsinfo tool. The LPS itself can also be printed in a pretty, human-readable format. The tool for this task is lpspp.
In essence, the LPS is a symbolic (or implicit) representation of the state space or labelled transition system (LTS) that describes the behaviour of the system explicitly. This LTS can be constructed from the LPS using a state space generator. In mCRL2 the tool that performs this task is lps2lts.
As state space generation can take a lot of time, it is often beneficial to reduce the LPS or make it more suitable for state space generation. Several tools are available for this, of which we mention a few here: lpssumelm, lpssuminst, lpsparelm, lpsconstelm and lpsrewr. Please refer to the manual pages of these tools for more information.
LTS tools
Once an LTS has been generated from an LPS, it can be visualised in several ways using interactive GUI tools. The most straightforward way of visualising an LTS is by showing it as a node-link diagram or graph. The ltsgraph tool performs this task. It can reorganise the produced image using a force-directed algorithm.
The picture produced by ltsgraph can become very cluttered for larger LTSs. Another LTS visualisation tool is ltsview which employs a clustering technique to reduce the complexity of the image. It produces a 3D visualisation of the LTS and aims to show symmetry in the behaviour of the system.
Diagraphica also clusters states to reduce complexity, producing a 2D image. It clusters states based on state parameter values, instead of on structural properties like ltsview.
Apart from these visualisation tools, a powerful tool is ltsconvert which can reduce an LTS modulo various equivalences. This often produces an LTS that is dramatically smaller than the original LTS, while important properties are maintained. The tool can also convert between various LTS file formats, some of which are textual, others binary.
An equally powerful tool is ltscompare which can check whether two LTSs are behaviourally equivalent or similar using various notions of equivalence/similarity.
The tool lts2lps can transform an LTS into an LPS, such that symbolic computation can be continued, e.g. after minimisation.
Model checking using PBESs
The aforementioned tools aid in getting more insight into the behaviour specified by an mCRL2 specification. However, a system's analysis often involves showing that the modelled system exhibits certain desired properties (or does not exhibit undesired ones). This can be done using model-checking techniques, which are very powerful verification methods.
In mCRL2, model checking is provided using parameterised boolean equation systems (PBESs). As mentioned before, the central notion in mCRL2 is the LPS. Not surprisingly, model checking also starts off with an LPS, which contains a symbolic specification of the system's behaviour.
The other input needed for model checking, is a formula expressing a desired property that the system should not violate (or satisfy). Such formulas are expressed in the regular modal μ-calculus (extended with data) and can be entered into a plain-text file using any text editor. The syntax of these formulas is described in the Language reference.
Given an LPS and a formula, the tool lps2pbes produces a PBES in which the model checking question of "does the formula hold for this LPS?" is encoded. The PBES is stored in a binary file format. By solving the PBES, an answer to this question can be found. The main tool for trying to solve a PBES is pbes2bool. It attempts to solve a given PBES and (if successful) returns either true or false.
Note that solving PBESs is generally undecidable, so the attempt may fail. In this case, more in-depth analysis of the PBES may be required. The tool pbespp is provided to pretty print a PBES in a human-readable format. Statistical information can be obtained using pbesinfo and the PBES can be simplified using pbesrewr. Furthermore some tools for simplifying the PBES are available, such as pbesparelm and pbesconstelm.
Import and export
The mCRL2 toolset also provides tools for converting system specifications in other languages to mCRL2. This can be done for Chi-models using chi2mcrl2, for Petri nets using pnml2mcrl2 and for typed LySa using lysa2mcrl2. Furthermore a μCRL linear process can be converted to an mCRL2 LPS using tbf2lps. Finally, an interface with the TorX tool is provided by lps2torx.
 Installation instructions
| Tool manual pages 
|
Copyright © 2005-2012 Technische Universiteit Eindhoven.
