The model checking capabilities of the mCRL2 tool set
Companies increasingly rely on model driven engineering for developing their software systems. This approach raises the level of abstraction, resulting in an increased productivity and higher dependability of the developed artefacts. Formal verification of these models may help to further reduce development costs by detecting issues early and by further increasing the overall reliability of the system. However, the success of formal verification is directly linked to the maturity of the tooling used for performing the analysis. Most of the available tooling requires highly skilled and experienced verification engineers to tackle complex industrial problems.
From ASD:Suite to Dezyne
Verum has created the ASD:Suite tool suite in the past, in which an intuitive integrated development environment for specifying complex, concurrent, industrial systems is offered. While ASD:Suite is easy to use for both novice and experienced system designers, it limits more experienced designers in constructing more complex models and accessing the full power of formal verification and model checking. In an effort to move beyond these limitations, Verum has designed a new, open modelling language called Dezyne, that is richer in terms of constructs and facilities. The open nature of the language enables offering alternative verification technology through other back-ends. This will allow Verum and others to offer new services for expert users.
Dezyne and mCRL2
In this paper, we provide an encoding of the Dezyne modelling language in the mCRL2 process algebra, thus giving a formal semantics to Dezyne models.
Furthermore, you will learn more about:
- the mCRL2 language;
- the transformation of Dezyne models to mCRL2 process expressions;
- the technology that we used to program the transformation between Dezyne and mCRL2;
- how the connection to mCRL2 and its analysis tool set can be used as the basis for future verification services;
- using the advanced model checking capabilities and refinement checks of the mCRL2 tool set;
- the advanced behavioural visualisation tooling to end-users we offer.
Like to learn more? Download the full paper here!