Easy property specification for Cordis 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.

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

Currently, requirements about Cordis models need to be specified directly as modal mu-calculus formulas. This is quite far removed from the low-code models that engineers design using the Cordis modeler. In this project, we aim to implement an approach to specifying and verifying properties in a way that it becomes easy for the engineer that also develops the Cordis model. Several questions are important for this. First of all, what is a suitable way to express properties, that is close to the low-code development philosophy in Cordis modeler. Second, if a property has been verified, and it turns out the property does not hold, the mCRL2 toolset can generate a counterexample. This counterexample is expressed in terms of a labelled transition system, that is much more detailed than the original UML state machine diagram. How can this counterexample be translated back to concepts in the original UML state machine diagram, and how can it be presented to the user?

Some inspiration for this project in the context of the verification of UML models can be found in [1] and [2]. However, there are also other high-level approaches to specifying properties, e.g., property specification patterns.

[1] D. Remenska, T.A.C. Willemse, J. Templon, K. Verstoep and H.E. Bal, Property Specification Made Easy: Harnessing the Power of Model Checking in UML designs. In E. Abraham and C. Palamidessi (eds.), FORTE 2014, Lecture Notes in Computer Science 8461, Springer, pp. 17-32, 2014. https://doi.org/10.1007/978-3-662-43613-4_2

[2] Daniela Remenska, Jeff Templon, Tim A.C. Willemse, Philip Homburg, Kees Verstoep , Adria Casajus and Henri Bal. From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems. In Guillaume Brat, Neha Rungta, Arnaud Venet (eds.), NFM 2013, Lecture Notes in Computer Science 7871, Springer, pp. 244-260, 2013. https://doi.org/10.1007/978-3-642-38088-4_17