Contract-based Verification of Digital Twins

• URL: http://arxiv.org/abs/2506.10993v1
• Date: Mon, 07 Apr 2025 10:33:10 GMT
• Title: Contract-based Verification of Digital Twins
• Authors: Muhammad Naeem, Cristina Seceleanu,
• Abstract summary: This paper introduces an innovative methodology for verifying neural network-based digital twin models.<n>The latter relies on defining and applying system-level contracts that capture the system's requirements.<n>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.
• Score: 1.6238978627325962
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Continuously Updating Digital Twins using Large Language Models [49.7719149179179]
  Digital twins are models of real-world systems that can simulate their dynamics in response to potential actions.<n>Current approaches struggle in this regard, as they require fixed, well-defined modelling environments.<n>We develop CALM-DT, a Context-Adaptive Language Model-based Digital Twin that can accurately simulate across diverse state-action spaces.
  arXiv  Detail & Related papers  (2025-06-11T14:45:28Z)
• Formal Verification of Digital Twins with TLA and Information Leakage Control [15.387256204743407]
  Digital twin verification is challenging due to uncertainties in the virtual representation, the physical environment, and the bidirectional flow of information between physical and virtual.<n>This paper presents a methodology to specify and verify digital twin behavior, translating uncertain processes into a formally verifiable finite state machine.<n>We demonstrate this approach on a digital twin of an unmanned aerial vehicle, verifying synchronization of physical-to-virtual and virtual-to-digital data flows to detect unintended misalignments.
  arXiv  Detail & Related papers  (2024-11-27T22:52:36Z)
• From Digital Twins to Digital Twin Prototypes: Concepts, Formalization, and Applications [55.57032418885258]
  There is no consensual definition of what a digital twin is. Our digital twin prototype (DTP) approach supports engineers during the development and automated testing of embedded software systems.
  arXiv  Detail & Related papers  (2024-01-15T22:13:48Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Enhanced multi-fidelity modelling for digital twin and uncertainty quantification [0.0]
  Data-driven models play a crucial role in digital twins, enabling real-time updates and predictions. The fidelity of available data and the scarcity of accurate sensor data often hinder the efficient learning of surrogate models. We propose a novel framework that begins by developing a robust multi-fidelity surrogate model.
  arXiv  Detail & Related papers  (2023-06-26T05:58:17Z)
• The Executable Digital Twin: merging the digital and the physics worlds [0.0]
  Key building blocks such as model order reduction, real-time models, state estimation and co-simulation are reviewed. These include virtual sensing, hybrid testing and hardware-in-the loop, model-based control and model-based diagnostics.
  arXiv  Detail & Related papers  (2022-10-25T08:35:08Z)
• Automatic digital twin data model generation of building energy systems from piping and instrumentation diagrams [58.720142291102135]
  We present an approach to recognize symbols and connections of P&ID from buildings in a completely automated way. We apply algorithms for symbol recognition, line recognition and derivation of connections to the data sets. The approach can be used in further processes like control generation, (distributed) model predictive control or fault detection.
  arXiv  Detail & Related papers  (2021-08-31T15:09:39Z)
• A Probabilistic Graphical Model Foundation for Enabling Predictive Digital Twins at Scale [0.0]
  We create an abstraction of the asset-twin system as a set of coupled dynamical systems. We demonstrate how the model is instantiated to enable a structural digital twin of an unmanned aerial vehicle.
  arXiv  Detail & Related papers  (2020-12-10T17:33:59Z)
• Digital Twins: State of the Art Theory and Practice, Challenges, and Open Research Questions [62.67593386796497]
  This work explores the various DT features and current approaches, the shortcomings and reasons behind the delay in the implementation and adoption of digital twin. The major reasons for this delay are the lack of a universal reference framework, domain dependence, security concerns of shared data, reliance of digital twin on other technologies, and lack of quantitative metrics.
  arXiv  Detail & Related papers  (2020-11-02T19:08:49Z)
• Man, machine and work in a digital twin setup: a case study [77.34726150561087]
  A digital twin as a virtual counterpart of a physical human-robot assembly system is built as a front-runner for validation and control through design, build, and operation. The forms of digital twins along the system life cycle, the building blocks, and potential advantages are presented.
  arXiv  Detail & Related papers  (2020-06-15T20:54:43Z)
• The role of surrogate models in the development of digital twins of dynamic systems [0.0]
  Digital twin technology has significant promise, relevance and potential of widespread applicability. Digital twins are expected to exploit data and computational methods. We have explored the possibility of using surrogate models within the digital twin technology.
  arXiv  Detail & Related papers  (2020-01-25T10:48:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.