Jeroen Keiren

Formal methods researcher at TU/e

Objective

This assignment aims to formalize the semantics of the Structured Text (ST) programming language within the data types of the mCRL2 model checker. The goal is to bridge the gap between high-level programming constructs and formal verification methods, enhancing the reliability and correctness of software systems.

Background

Structured Text is a high-level programming language widely used for Programmable Logic Controllers (PLC) in industrial automation and control systems. mCRL2 is a formal specification language and toolset designed for modeling, validation, and verification of concurrent systems and protocols. When formalizing systems that use structured text, different choices can be made w.r.t. their formalization:

  1. Code fragments can be translated as processes with a program counter, and an action is generated for every statement in the code fragment.
  2. The effect of a code fragment can be completely captured in mCRL2’s data types, such that no intermediate actions are introduced in the model.

There potentially is a tradeoff between these two approaches: in the first approach, computations regarding data types are limited, but the size of the state space increases, whereas in the second approach, more computation needs to be done, but the state space size is smaller.

Industrial Context

Cordis models are UML-like models developed within the Cordis SUITE, a low-code development platform designed for creating complex machine-control applications. These models use extensions of UML class diagrams to describe the static structure and UML state machine diagrams to capture the dynamic behavior of systems. Additionally, Cordis models incorporate elements of the Structured Text programming language.

We have developed translation of Cordis models into mCRL2, such that formal verification methods can be leveraged to ensure correctness of these systems. Currently, the first approach described above is used in the translation. In this project, you develop the second approach and compare it to the existing implementation.

Supervision

This project will be supervised by Jeroen Keiren and Maurice Laveaux.

Possibilities of doing this internship at Cordis can be discussed.