Model checking in the context of digital twins
Jeroen Keiren
TU Eindhoven
Abstract: 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 system and its digital twin. 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 first 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.
Speaker bio: Jeroen Keiren is assistant professor in the Formal System Analysis cluster at Eindhoven University of Technology, The Netherlands. Earlier, he had positions at the Open University of the Netherlands, VU Amsterdam, University of Maryland, as well as visiting researcher positions at Radboud University Nijmegen and TU Delft.
His research focuses on the development of formal methods for the design and application of correct and reliable software and hardware systems. Specific areas of expertise include model checking, parity games and timed systems. He is particularly interested in the application of such techniques to industry critical systems, and is currently the PI of two research projects that focus on the verification of machine control applications described using a variation of UML state machine diagrams.