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.
翻译:设计控制工业设备的软件具有挑战性,特别是由于其固有的同时性质。测试这类事件驱动的控制软件是困难的,而且由于可能执行的情景众多,实际上只实现低动态测试覆盖率。这反过来又不可取,因为这类设备软件故障成本高。我们在本文件中描述Dezyne语言和工具;Dezyne是一种程序设计语言,旨在帮助软件工程师设计大型工业控制软件。我们讨论了其基本的两个层次和构成方法,该方法能够获取正规方法的好处,因此大力支持软件工程的指导原则。Dezyne的核心使用mCRL2语言和模型检查器(Jan Friso Groote等人)来核查所有可能的执行情景的正确性和完整性。Dezyne IDE基于语言服务器协议,允许与例如视觉工作室代码和Emacs等顺利融合,并经过若干自动生成的互动式图形视图扩展。我们向几个大型高技术设备制造商报告了Dezyne及其前身的引入情况,从而减少了软件开发时间和报告的实地缺陷。