Verification of Digital Twins using Classical and Statistical Model Checking

TL;DR

This paper explores the verification of digital twins using classical and statistical model checking techniques to ensure their correctness and property adherence during runtime, demonstrated on an autonomous truck DT.

Contribution

It introduces a combined approach of classical and statistical model checking for verifying digital twins, addressing both deterministic and stochastic properties.

Findings

The digital twin of an autonomous truck is deadlock free and functionally correct.

The DT does not meet timeliness requirements.

Verification techniques effectively identify property adherence and violations.

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.