使用mCRL2对工业类UML模型进行形式化验证（扩展版）

低代码开发平台正日益普及。本质上，这类平台允许从编码转向图形化建模，有助于提高质量并缩短开发时间。Cordis SUITE是一个低代码开发平台，它采用统一建模语言（UML）来设计复杂的机器控制应用程序。在本文中，我们介绍了Cordis模型及其语义。为了实现形式化验证，我们定义了从Cordis模型到进程代数规约语言mCRL2的自动转换。作为概念验证，我们描述了由Cordis开发的工业气缸模型的控制软件需求，并展示了如何使用模型检验来验证这些需求。我们证明，我们的验证方法能有效发现工业模型及其实现中的细微问题。