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)

TL;DR
Dezyne is a formal methods-based programming language and tooling designed for industrial control software, improving correctness, reducing development time, and decreasing field defects through model checking and integrated development environment support.
Contribution
This paper introduces Dezyne, a novel language and tooling that integrates formal verification into industrial control software development, enhancing reliability and efficiency.
Findings
Reduced software development time at large manufacturers
Significant decrease in field defects reported
Effective integration of formal methods into practical engineering
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
