论文标题
使用MCRL2（扩展版）对工业UML样模型的正式验证
Formal verification of an industrial UML-like model using mCRL2 (extended version)
论文作者
论文摘要
低代码开发平台正在越来越受欢迎。本质上，这样的平台可以从编码转向图形建模，有助于提高质量并减少开发时间。 Cordis Suite是一个低代码开发平台，它采用统一的建模语言（UML）来设计复杂的机器控制应用程序。在本文中，我们介绍了Cordis模型及其语义。为了启用正式验证，我们将cordis模型自动翻译为过程代数规范语言MCRL2。作为概念的证明，我们描述了Cordis开发的工业缸模型的控制软件的要求，并显示如何使用模型检查对其进行验证。我们表明，我们的验证方法有效地发现工业模型中的细微问题及其实施。
Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.
