A In the setting of digital twins, real world systems and virtual models are kept in sync. If the implementation and the models share a common source of truth, such as a low-code model, this allows for a very tight integration of the different aspects of digital twins. In a collaboration with, among others, Eindhoven University, Cordis SUITE and TNO ESI, an environment was developed in which Cordis SUITE’s low code models are used to as ground truth. On the one hand, these models are used to generate code for machine control applications, with the necessary instrumentation to observe the state of the system and the data for digital twinning. On the other hand, the models are used for formal verification purposes.

In this talk I will describe the general overview of this digital twin environment. Subsequently, I will focus on the application of the mCRL2 model checker for the formal verification of the low code models, and how the verification results can be fed back into the digital twin environment.

The results presented in this talk are part of the ITEA3 MACHINAIDE and the OPZuid Verification Base Remote & Secure Maintenance solutions projects.