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 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 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 toolset can be used as the basis for future verification services;
  • using the advanced model checking capabilities and refinement checks of the mCRL2 toolset;
  • the advanced behavioural visualisation tooling to end-users we offer.
The model checking capabilities of the mCRL2 tool set

The model checking capabilities of the mCRL2 tool set

In this award winning paper, we describe the Dezyne language and a model transformation to the mCRL2 language, providing users access to advanced model checking capabilities and refinement checks of the mCRL2 tool set.

Presentation Connecting mCRL2 and Dezyne: Challenges and Opportunities

In this video you can see the presentation of Tim Willemse from the Formal System Analysis Group, TU/e in 2016 about Connecting mCRL2 and Dezyne: Challenges and Opportunities.

Related Articles

Enjoy this article? Don't forget to share.