Dezyne: Paving the Way to Practical Formal Software Engineering
This addresses the problem of high software failure costs in industrial equipment by providing a practical formal method tool for software engineers, though it is incremental as it builds on existing mCRL2 technology.
The paper tackles the challenge of designing and testing concurrent industrial control software by introducing the Dezyne language and tooling, which uses formal methods to verify correctness and completeness, resulting in decreased development time and field defects at high-tech equipment manufacturers.
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.