Abstract:

This thesis proposes a technique for specifying and verifying formal requirements in the context of the Cordis Modeler, bridging the gap between the high-level nature of Cordis
models and the complex construction of μ-calculus formulas.

Formal verification plays an important role in ensuring the correctness of complex systems. This thesis investigates how formal requirements can be described using UML state machines. Focusing on adapting finite state automata (FSA) templates from PROPEL [7, 25] to meet the needs of the Cordis Modeler. The primary goal is to reduce the difficulty of specifying properties by devising a framework for constructing properties at a level of abstraction similar to that of Cordis models.

We adapt PROPEL’s FSA-based templates to UML state machines by extending the defined templates to include absence, precedence, and response behaviours with ‘between’  scope. We define a method for expressing optionally accepting states in UML state machines and incorporating Cordis’ guard syntax on transitions. Furthermore, we create a mapping between PROPEL’s FSAs and μ-calculus formula patterns, enabling the automatic translation of templates for verification with the mCRL2 model checker.

The applicability of this technique is demonstrated through the FESTO automation cell case study. This representative example is used as an argument to expand the capabilities of PROPEL. In addition, simplifications were made in other areas to tailor it to the environment of the Cordis Modeler. For the translation to μ-calculus we introduce an algorithm and generalized pattern for handling variables exposed on self-loops within mCRL2 models. Using a proof-of-concept tool, we instantiate and translate the templates into μ-calculus formulas.

Finally, we propose and compare three potential pathways for integrating our proposed technique with the Cordis Modeler: through state machine diagrams, a requirement builder, and the documentation suite. These approaches are evaluated based on distinguishability from behavioural state machines, synchronization with Cordis models, and documentation of PROPEL-derived information.