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及其前身的引入情况,从而减少了软件开发时间和报告的实地缺陷。

0
下载
关闭预览

相关内容

《工程》是中国工程院(CAE)于2015年推出的国际开放存取期刊。其目的是提供一个高水平的平台,传播和分享工程研发的前沿进展、当前主要研究成果和关键成果;报告工程科学的进展,讨论工程发展的热点、兴趣领域、挑战和前景,在工程中考虑人与环境的福祉和伦理道德,鼓励具有深远经济和社会意义的工程突破和创新,使之达到国际先进水平,成为新的生产力,从而改变世界,造福人类,创造新的未来。 期刊链接:https://www.sciencedirect.com/journal/engineering
最新《联邦学习Federated Learning》报告,Federated Learning
专知会员服务
86+阅读 · 2020年12月2日
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
知识图谱推理,50页ppt,Salesforce首席科学家Richard Socher
专知会员服务
105+阅读 · 2020年6月10日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
carla无人驾驶模拟中文项目 carla_simulator_Chinese
CreateAMind
3+阅读 · 2018年1月30日
【推荐】YOLO实时目标检测(6fps)
机器学习研究会
20+阅读 · 2017年11月5日
深度学习医学图像分析文献集
机器学习研究会
18+阅读 · 2017年10月13日
【推荐】Python机器学习生态圈(Scikit-Learn相关项目)
机器学习研究会
6+阅读 · 2017年8月23日
Arxiv
0+阅读 · 2021年10月4日
Arxiv
46+阅读 · 2021年10月4日
VIP会员
相关VIP内容
最新《联邦学习Federated Learning》报告,Federated Learning
专知会员服务
86+阅读 · 2020年12月2日
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
知识图谱推理,50页ppt,Salesforce首席科学家Richard Socher
专知会员服务
105+阅读 · 2020年6月10日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
carla无人驾驶模拟中文项目 carla_simulator_Chinese
CreateAMind
3+阅读 · 2018年1月30日
【推荐】YOLO实时目标检测(6fps)
机器学习研究会
20+阅读 · 2017年11月5日
深度学习医学图像分析文献集
机器学习研究会
18+阅读 · 2017年10月13日
【推荐】Python机器学习生态圈(Scikit-Learn相关项目)
机器学习研究会
6+阅读 · 2017年8月23日
Top
微信扫码咨询专知VIP会员