Model Checking Machine-Control Applications

Software systems are becoming increasingly more complex to develop, understand and analyse. Low-code development platforms (LCDPs) allow us to create graphical models of the software that is developed, reducing development times and improving understandability. If the semantics is well-understood, the models can be automatically translated to the languages used by state-of-the-art model checkers to be analysed. Model checking is an automated technique to establish whether formally defined requirements hold for a model of a system, increasing confidence in its correctness.

The Cordis SUITE is an LCDP for machine-control applications. Cordis models define the static structure and the behaviour of the modelled machines using UML class and state machine diagrams. In this thesis we describe how to model check machine-control applications developed using the Cordis SUITE.

To enable model checking of Cordis models, we analyse their structure and define their syntax and semantics. We define the formal operational semantics of Cordis models in terms of labelled transition systems.

To apply model checking, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. We demonstrate the feasibility of model checking machine-control applications using the mCRL2 model checker by a small Cordis model. When the models increase in size and complexity the running time increases due to the so-called state space explosion problem.

One of the key contributing factors for the state space explosion is the use of data in the models. Nevertheless, complex data types are often used to create concise and easy to read models. To this end, we present a general technique to replace variables of complex data types by multiple variables of simpler data types. We demonstrate that our technique can reduce the time required for state space exploration.

A model checker provides a yes/no answer to the model checking problem indicating whether the requirements hold or not for the system. This answer alone does not explain why the requirement does or does not hold. To this end, model checkers provide an explanation (witness / counterexample) to the answer. Obtaining an explanation to the model checking problem is available for various logics such as LTL and (Probabilistic) CTL. For the mu-calculus, we can obtain an explanation for explicit model checking only. To provide the necessary explanation in symbolic model checking we propose an efficient two-step approach to generate evidence in mCRL2. We demonstrate the correctness of the approach and experimentally demonstrate its effectiveness.