Dezyne: Paving the Way to Practical Formal Software Engineering

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