Specifying verifiable low code models

Context

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 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.

Objective

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 of a real-world industrial production system.

Supervision

This project will be supervised by Jeroen Keiren

References

[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.