Formal verification of an industrial UML-like model using mCRL2 (extended version)

TL;DR

This paper presents a method for formally verifying UML-like models in low-code platforms by translating them into mCRL2, enabling model checking to ensure correctness in industrial applications.

Contribution

It introduces a translation from Cordis UML-like models to mCRL2, facilitating formal verification of industrial control software.

Findings

Effective detection of subtle issues in industrial models

Successful verification of an industrial cylinder control software

Demonstration of model checking applicability in low-code platforms

Abstract

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.