Formal Verification of Digital Twins with TLA and Information Leakage Control

• URL: http://arxiv.org/abs/2411.18798v1
• Date: Wed, 27 Nov 2024 22:52:36 GMT
• Title: Formal Verification of Digital Twins with TLA and Information Leakage Control
• Authors: Luwen Huang, Lav R. Varshney, Karen E. Willcox,
• Abstract summary: 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. This paper presents a methodology to specify and verify digital twin behavior, translating uncertain processes into a formally verifiable finite state machine. 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.
• Score: 15.387256204743407
• License:
• Abstract: Verifying the correctness of a digital twin provides a formal guarantee that the digital twin operates as intended. Digital twin verification is challenging due to the presence of uncertainties in the virtual representation, the physical environment, and the bidirectional flow of information between physical and virtual. A further challenge is that a digital twin of a complex system is composed of distributed components. This paper presents a methodology to specify and verify digital twin behavior, translating uncertain processes into a formally verifiable finite state machine. We use the Temporal Logic of Actions (TLA) to create a specification, an implementation abstraction that defines the properties required for correct system behavior. Our approach includes a novel weakening of formal security properties, allowing controlled information leakage while preserving theoretical guarantees. 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.

Related papers

• Know Where You're Uncertain When Planning with Multimodal Foundation Models: A Formal Framework [54.40508478482667]
  We present a comprehensive framework to disentangle, quantify, and mitigate uncertainty in perception and plan generation. We propose methods tailored to the unique properties of perception and decision-making. We show that our uncertainty disentanglement framework reduces variability by up to 40% and enhances task success rates by 5% compared to baselines.
  arXiv  Detail & Related papers  (2024-11-03T17:32:00Z)
• Med-Real2Sim: Non-Invasive Medical Digital Twins using Physics-Informed Self-Supervised Learning [15.106435744696013]
  A digital twin is a virtual replica of a real-world physical phenomena that uses mathematical modeling to characterize and simulate its defining features. We propose a method to identify digital twin model parameters using only noninvasive patient health data.
  arXiv  Detail & Related papers  (2024-02-29T23:04:42Z)
• 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)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity. We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
  arXiv  Detail & Related papers  (2023-12-13T21:53:32Z)
• Probabilistic machine learning based predictive and interpretable digital twin for dynamical systems [0.0]
  Two approaches for updating the digital twin are proposed. In both cases, the resulting expressions of updated digital twins are identical. The proposed approaches provide an exact and explainable description of the perturbations in digital twin models.
  arXiv  Detail & Related papers  (2022-12-19T04:25:59Z)
• 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)
• Knowledge Equivalence in Digital Twins of Intelligent Systems [3.7953718547499045]
  The paper focuses in particular on digital twin models of intelligent systems where the systems are knowledge-aware but with limited capability. The modelling of such an intelligent physical system requires replicating the knowledge-awareness capability in the virtual space. This paper proposes the notion of knowledge equivalence and an equivalence maintaining approach by knowledge comparison and updates.
  arXiv  Detail & Related papers  (2022-04-15T14:31:17Z)
• 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)
• gradSim: Differentiable simulation for system identification and visuomotor control [66.37288629125996]
  We present gradSim, a framework that overcomes the dependence on 3D supervision by leveraging differentiable multiphysics simulation and differentiable rendering. Our unified graph enables learning in challenging visuomotor control tasks, without relying on state-based (3D) supervision.
  arXiv  Detail & Related papers  (2021-04-06T16:32:01Z)
• 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)

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.