Contract-based Verification of Digital Twins

TL;DR

This paper presents a novel black-box verification method for neural network-based digital twins using system-level contracts and model checking, enabling effective validation without access to internal model details.

Contribution

It introduces an automated, contract-based verification approach integrating model checking with digital twin models in Simulink, applicable in a black-box setting.

Findings

Successfully verified a boiler system digital twin

Identified prediction errors through contract violations

Demonstrated effectiveness of model checking integration

Abstract

Digital twins are becoming powerful tools in industrial applications, offering virtual representations of cyber-physical systems. However, verification of these models remains a significant challenge due to the potentially large datasets used by the digital twin. This paper introduces an innovative methodology for verifying neural network-based digital twin models, in a black-box fashion, by integrating model checking into the process. The latter relies on defining and applying system-level contracts that capture the system's requirements, to verify the behavior of digital twin models, implemented in Simulink. We develop an automated solution that simulates the digital twin model for certain inputs, and feeds the predicted outputs together with the inputs to the contract model described as a network of timed automata in the UPPAAL model checker. The latter verifies whether the predicted outputs fulfill the specified contracts. This approach allows us to identify scenarios where the digital twin's behavior fails to meet the contracts, without requiring the digital twin's design technicalities. We apply our method to a boiler system case study for which we identify prediction errors via contract verification. Our work demonstrates the effectiveness of integrating model checking with digital twin models for continuous improvement.