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.