Dezyne 2.8.0, "Plus ça change, plus c'est la même chose"

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 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.

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. 

For more information about Dezyne 2.8.0 please contact us.