Best Paper Award for Jan Friso Groote, Tim Willemse, and Wieger Wesselink
From September 18 to September 20, the International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS-AVOCS) 2017 took place in Turin. A paper written by Full Professor Jan Friso Groote, Associate Professor Tim Willemse, and Assistant Professor Wieger Wesselink of the Model Driven Software Engineering section, was awarded with the 2017 Best Paper Award.
The paper, Formalising the Dezyne Modelling Language in mCRL2, was written in collaboration with Verum Software Tools. It describes the Dezyne modelling language, which is used by Verum to specify system behavior. It discusses how Dezyne specifications are encoded into mCRL2 specifications. The paper was very well received by the reviewers of the conference. They praised the authors on the way the paper was written, structured, and how the ideas are explained. The presented work is interesting, significant and relevant to this conference.
Dezyne is an industrial language with an associated set of tools, allowing users to model interface behaviours and implementations of reactive components and generate executable code from these. The tool and language succeed the successful ASD:Suite tool set, which, in addition to modelling reactive components, offers a set of verification capabilities allowing users to check the conformance of implementations to their interfaces. In this 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.