Dezyne: Paving the Way to Practical Formal Software Engineering

Rutger van Beusekom
(Verum Software Tools B.V., The Netherlands)
Bert de Jonge
(Verum Software Tools B.V., The Netherlands)
Paul Hoogendijk
(Verum Software Tools B.V., The Netherlands)
Jan Nieuwenhuizen
(Verum Software Tools B.V., The Netherlands)

Designing software that controls industrial equipment is challenging, especially due to its inherent concurrent nature. Testing this kind of event driven control software is difficult and, due to the large number of possible execution scenarios only a low dynamic test coverage is achieved in practice. This in turn is undesirable due to the high cost of software failure for this type of equipment.

In this paper we describe the Dezyne language and tooling; Dezyne is a programming language aimed at software engineers designing large industrial control software. We discuss its underlying two layered and compositional approach that enables reaping the benefits of Formal Methods, hereby strongly supporting guiding principles of software engineering. The core of Dezyne uses the mCRL2 language and model-checker (Jan Friso Groote et al.) to verify the correctness and completeness of all possible execution scenarios.

The IDE of Dezyne is based on the Language Server Protocol allowing a smooth integration with e.g., Visual Studio Code, and Emacs, extended with several automatically generated interactive graphical views. We report on the introduction of Dezyne and its predecessor at several large high-tech equipment manufacturers resulting in a decrease of software developing time and a major decrease of reported field defects.

In José Proença and Andrei Paskevich: Proceedings of the 6th Workshop on Formal Integrated Development Environment (F-IDE 2021), Held online, 24-25th May 2021, Electronic Proceedings in Theoretical Computer Science 338, pp. 19–30.
Published: 6th August 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: