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.

翻译：低码开发平台越来越受欢迎。 从本质上说,这些平台允许从编码转向图形模型,有助于提高质量和缩短开发时间。Cordis SUITE是一个低码开发平台,采用统一模型语言(UML)设计复杂的机器控制应用程序。在本文中,我们引入了Cordis模型及其语义。为了能够进行正式核查,我们定义了Cordis模型的自动翻译到进程代数规格语言 mCRL2。作为概念的证明,我们描述了Cordis开发的工业气瓶模型控制软件的要求,并展示了如何用模型检查来验证这些要求。我们展示了我们的核查方法对于发现工业模型及其实施中的微妙问题非常有效。