Verification of Digital Twins using Classical and Statistical Model Checking

TL;DR

This work tackles the challenge of runtime verification for digital twins (DTs) with highly stochastic and time-critical interactions. It proposes a hybrid verification framework that combines classical model checking (CMC) and statistical model checking (SMC) and applies it to an autonomously driving truck DT using UPPAAL tooling. The study finds that CMC can verify deadlock freeness and several functional properties, while SMC yields probabilistic timing insights such as worst-case reaction time, though timeliness properties may still fail and results can diverge due to differences in temporal modeling. The paper provides a comparative analysis of CMC and SMC, highlighting their complementary strengths and limitations, and outlines challenges and future work to automate model extraction and broaden evaluation across more DT case studies.

Abstract

With the increasing adoption of digital techniques, the concept of digital twin (DT) has received a widespread attention in both industry and academia. While several definitions exist for a DT, most definitions focus on the existence of a virtual entity (VE) of a real-world object or process, often comprising interconnected models which interact with each other, undergoing changes continuously owing to the synchronization with the real-world object. These interactions might lead to inconsistencies at execution time, due to their highly stochastic and/or time-critical nature, which may lead to undesirable behavior. In addition, the continuously varying nature of VE owing to its synchronization with the real-world object further contributes to the complexity arising from these interactions and corresponding model execution times, which could possibly affect its overall functioning at runtime. This creates a need to perform (continuous) verification of the VE, to ensure that it behaves consistently at runtime by adhering to desired properties such as deadlock freeness, functional correctness, liveness and timeliness. Some critical properties such as deadlock freeness can only be verified using classical model checking; on the other hand, statistical model checking provides the possibility to model actual stochastic temporal behavior. We therefore propose to use both these techniques to verify the correctness and the fulfillment of desirable properties of VE. We present our observations and findings from applying these techniques on the DT of an autonomously driving truck. Results from these verification techniques suggest that this DT adheres to properties of deadlock freeness and functional correctness, but not adhering to timeliness properties.