Game changing verification engine
As the complexity of software systems under development rapidly increases, Dezyne is being used to tackle ever more challenging verification and validation problems. To keep pace with the demand for more powerful verification, Verum has completed the integration of a completely new, game changing verification engine into Dezyne. Based on mCRL2 technology from the Eindhoven University of Technology (TU/e), the new engine already outperforms its predecessor and provides a platform for verifying larger, more complex problems in the future, including functional software verification.
In spite of having completely replaced the verification engine, the latest release of Dezyne (2.8.0) contains no significant changes for users and is entirely backwards compatible with the last FDR based release (2.6.x). Additionally, release 2.8.0 includes the new modelling keyword “async”, which complements the existing keywords “blocking” and “external”. All three keywords are used to define and control concurrency, where “async” is used to introduce concurrent behaviour and “blocking” is used to remove it. For this release the Verum support website has been greatly expanded to include better documentation, more tutorials, a wider range of examples and new use case articles.
Smart work achievement
The move to mCRL2 based verification is an achievement that has been several years in the making and ultimately made possible through some incredibly smart work by the Verum development team and experts from the TU/e, including Professor Jan Friso Groote, Associate Professor Tim Willemse and Assistant Professor Wieger Wesselink. Funding was provided from various sources, including TETRACOM and an RVO Innovatie Krediet.
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.