Specifying verifiable low code models

The Cordis modeler is a tool for the low code development of machine control applications. The structure of the controller is described using UML class diagrams. The behaviour of the components within the controller is described using a variation of UML state machine diagrams. Executable code, typically targeted to programmable logic controllers (PLCs), is automatically generated from these low code models.

In the OPZuid project “Verification Based Remote & Secure Maintenance Solutions” a translation of the behaviour of Cordis models to mCRL2 has been developed. A related project, MACHINAIDE, focuses on scaling up the verification of these mCRL2 models.

In practice, we observe that industrial low code models are not very suitable for verification. They suffer from the state space explosion problem, in part because verification was not a primary concern when developing the models. In this project, we aim to identify modelling guidelines for Cordis models that, for instance, help in keeping the state space explosion small, or that generate models with a cleaner structure, such that compositional verification becomes a suitable technique. Some general specification guidelines to avoid the state space explosion problem, not tied specifically to Cordis models, have previously been investigated [1]. You are expected to study modelling techniques and show their effect using an example case study called “Merry go round”. This is a demo system provided by Cordis, that consists of several conveyor belts, gantries, and platforms. In the current model, a single gantry alone has roughly 10^14 states.

[1] Groote, J.F., Kouters, T.W.D.M., Osaiweran, A.: Specification guidelines to avoid the state space explosion problem. Software Testing, Verification and Reliability. 25, 1, 4-33 (2015). https://doi.org/10.1002/stvr.1536.