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.