Verification of Digital Twins through Statistical Model Checking

Since its inception as abstract notion in 2002, Digital Twins (DTs) have received increased attention over the last 5 to 10 years, in both industry and academia. Most definitions of DTs focus on the existence of a virtual entity (VE) which faithfully represents a real-world physical entity (PE), and typically consist of a number of inter-connected models, undergoing changes continuously owing to the synchronization with its PE. During cosimulation, interactions between the various components making up a VE can be stochastic and time-critical in nature, which could lead to undesired (and unexpected) behavior. The continuous evolution of VE might further affect the nature of these interactions and corresponding model execution times, which could possibly affect its overall functioning during run-time. This creates a need to perform (continuous) verification of the VE, to ensure that it behaves consistently during execution by adhering to desired properties of interest such as timeliness, functional correctness, deadlock freeness and others. In this paper we propose to use statistical model checking (SMC) as a technique to verify a VEat runtime. For that purpose, we propose to use a stochastic timed automata (STA) model of the VE and its interacting components, and verify it using UPPAAL SMC. We present our observations and f indings from applying this technique on the cosimulation of a DT of an autonomously driving truck.