Source-linked AI summary
A System-of-Systems Case Study for the Verification of Composed Digital Twins
Mennatullah T. Khedr, Mengwei Xu, John S. Fitzgerald, Peter Gorm Larsen
TL;DR
Dependable DT engineering lacks practical guidance for verifying qualities in composed SoS architectures. The paper models a greenhouse SoS in VDM-RT, formalises individual DT artefacts as property sets, and analyses composition challenges. It finds that quality meanings depend on architectural roles and that local guarantees must become explicit assumptions for future compositional verification.
Problem
Practical guidance remains limited for formalising and verifying DT qualities, especially when heterogeneous DTs are composed in SoS architectures.
Method
The study uses a VDM-RT greenhouse SoS case study to operationalise DT qualities as verifiable properties across individual artefacts.
Results
Quality interpretations vary by architectural role: substitutability concerns behavioural agreement for Pot Models but decision-impact preservation for DSMs.
Takeaways & Limitations
Compositional verification requires explicit dependencies and proof rules connecting constituent-level guarantees to SoS-level quality guarantees.
Takeaways & Limitations
The models are validated through simulation and controlled execution rather than physical-hardware deployment, and generalisability requires further case studies.
Abstract
from arXiv · showhide
Current approaches to engineering dependable Digital Twins (DTs) of Cyber-Physical Systems lack practical guidance on how qualities such as relevance, verifiability, substitutability and fidelity may be formalised and verified. This need is amplified in Systems-of-Systems (SoS), where reliance is placed on the composition of DTs. The goal of this study is to identify foundational challenges that a framework for DT validation and verification should address in an SoS setting, and to investigate the formalisation of individual DT artefacts as a step towards compositional reasoning. We present a case study based on a DT-enabled greenhouse SoS modelled in VDM-RT (Vienna Development Method, Real-Time), including executable formal models, a property-based account of DT qualities, and an analysis of the obstacles arising when attempting to compose these artefacts at the SoS level. We consider how DT qualities may be operationalised as sets of verifiable properties. Formal modelling and analysis techniques and tools supporting their verification are identified. The study reveals how interpretations of DT qualities must adapt to different architectural roles and how local quality guarantees form assumptions for compositional reasoning. Full formalisation and verification of SoS composition is identified as future work.
1 Introduction
Dependable DT engineering lacks practical methods for formalising and verifying qualities, and these difficulties intensify when heterogeneous DTs are composed in an SoS. The paper addresses this gap through a VDM-RT greenhouse case study focused on individual artefacts and compositional challenges.
- Heterogeneous assumptions and abstraction levels allow faults in one SoS DT to propagate to dependent DTs, complicating quality reasoning compared with isolated DTs.
- DT verification remains under-explored, with existing frameworks largely descriptive and limited guidance for formalising qualities such as relevance, verifiability, substitutability, and fidelity.
- Prior formal or semi-formal approaches demonstrate feasibility but generally address isolated qualities or coordination concerns rather than composed DT verification obligations.
- The study operationalises DT qualities as formally stated properties verifiable or refutable with machine support, using a VDM-RT greenhouse-inspired SoS case study.
- The contributions include an executable co-simulation case study, a property-based quality approach, artefact-specific quality analysis, and identified SoS composition challenges.
- The paper formalises individual DT artefacts and analyses composition obstacles, but does not provide full SoS-level coordination formalisation or composed-property verification.
2 Greenhouse System as a DT-enabled SoS
The greenhouse case study combines physical plant pots, individual predictive DTs, a shared environmental shadow, and SoS-level coordination. Local controllers retain safety authority while DTs provide contextualised prediction and optimisation, although only the individual-pot layer is formalised and verified.
- The minimal greenhouse SoS is structured for hierarchical reasoning across interdependent plant-pot systems, their DTs, and SoS-level coordination.
- Each plant pot combines a moisture sensor, pump actuator, and local controller enforcing safety-threshold logic.
- The EDS receives temperature, humidity, and light data and provides shared environmental context to the Pot DTs.
- The EDS supports live sensor-based evaporation-factor computation and simulation-based prediction of environmental trends.
- Each Pot DT predicts moisture evolution and recommends watering actions, while the physical controller retains safety enforcement and direct actuation.
- The SoS coordination layer aggregates water usage and enforces global resource constraints to support collective objectives such as peak-demand management and fairness.
- The study formalises and verifies individual Pot DTs but treats SoS-level coordination as a target architecture and source of future verification questions.
3 Formal Modelling with VDM-RT and FMI
VDM-RT was chosen to model executable DT-enabled CPSs with discrete control and data-centric state, while FMI-based FMU export supports co-simulation. Verification covered model functionality but left runtime FMI inputs unchecked and deployment unaddressed.
- 3.1 Why VDM-RT for DT-enabled CPS?: VDM-RT supports state variables, operations, invariants, and pre- and post-conditions for expressing DT qualities as verifiable properties.
- 3.2 VDM-RT Models Developed: The formalisation models three aspects: Pot behaviour, DSM optimisation logic, and EDS environmental dynamics and context.
- 3.2 VDM-RT Models Developed: The model sizes are 244 LOC for Pot-related files, 133 LOC for PotDSM.vdmrt, and 92 LOC for Environment.vdmrt.
- 3.2 VDM-RT Models Developed: 56 proof obligations were generated for Pot model files, with nearly half unchecked because FMI port values are runtime-determined and represented as uninterpreted terms.
- 3.3 From VDM-RT to FMUs and Co-simulation: VDM-RT models are exported as FMI 2.0-compliant FMUs, requiring explicit time handling, total operations, and shared states declared through ports.
- 3.3 From VDM-RT to FMUs and Co-simulation: The FMU architecture connects Pot inputs and outputs with environmental, DSM, and controller interactions through typed ports.
- 3.3 From VDM-RT to FMUs and Co-simulation: Initial co-simulation experiments demonstrate executability and architectural soundness, with RabbitMQ-based FMU integration ongoing for future live-data coupling.
- 3.3 From VDM-RT to FMUs and Co-simulation: At this stage, co-simulation validates model behaviour and interaction patterns rather than supporting full operational deployment.
4 DT Qualities as Structured Sets of Verifiable Properties
The paper treats DT qualities as structured sets of formal properties, verification evidence, and concrete artefact instantiations. Their verification obligations differ by architectural role: physical models emphasise behavioural agreement, DSMs decision impact, and EDS context fidelity without substitutability.
- The framework distinguishes conceptual qualities, formal properties, verification evidence, and their embedding within concrete DT components.
- Properties support structured arguments for quality claims, with modelling constructs providing actionable means to embed them in DT components.
- The four core qualities are relevance, verifiability, substitutability, and fidelity, covering domain basis, checkability, safe replacement, and behavioural closeness.
- VDM-RT invariants, operation contracts, and relational trace predicates provide evidence for relevance, verifiability, and substitutability arguments.
- Pot Model: Pot-model relevance uses physical-domain invariants, while verifiability uses proof obligations for invariant preservation and operation totality.
- Pot Model: Pot substitutability compares behavioural agreement under identical environmental inputs, while fidelity bounds deviation between simulated and measured moisture trajectories.
- Decision Service Model (DSM): DSM substitutability is decision-impact preservation rather than behavioural equivalence, requiring safety-invariant preservation and feasible commands.
- Environment Digital Shadow (EDS): EDS relevance and verifiability use sensor-domain constraints and deterministic non-negative derived factors, while substitutability is not applicable because the DS only provides context.
5 Implications for Compositional Verification
The case study shows that locally verified DT qualities may not survive SoS composition. Compositional verification must therefore address semantic interactions and practical scalability, using local guarantees as assumptions for higher-level reasoning.
- Local satisfaction of DT qualities does not guarantee their preservation at the SoS level.
- Fidelity can become an aggregate property when shared-resource interactions amplify deviations across constituent DTs.The example concerns water allocation across multiple plant pots.
- Relevance shifts from constituent-level physical state bounds to SoS-level contributions to sustainability, efficiency, or resilience.
- Substitutability becomes relational and architectural, requiring behavioural compatibility across interacting services rather than only physical equivalence.
- Composing multiple synchronised DTs introduces latency, state-synchronisation overhead, co-simulation bottlenecks, and verification costs that grow with the number of DTs.The architecture includes Pot DTs, a shared EDS, and an SoS coordinator issuing priority-based commands.
- Compositional proof strategies must address semantic fidelity amplification and scope shifts alongside practical performance and scalability constraints.Local DT guarantees should serve as formal assumptions for higher-level reasoning, with additional obligations at each composition layer.
6 Discussion
The discussion finds that verification obligations depend on DT architectural roles, while VDM-RT and FMI co-simulation provide a practical route for carrying formal evidence into industrial workflows. It also identifies explicit context assumptions and interaction-aware reasoning as requirements for future compositional verification.
- Operationalising DT qualities as verifiable properties reveals that verification obligations depend on the artefact’s architectural role.
- Relevance properties consistently concern state invariants that can be checked through static proof, whereas substitutability and fidelity vary by role.
- For the Pot Model, substitutability means behavioural agreement under identical inputs and matching qualitative effects of the physical pot.
- For the DSM, substitutability means preserving safety-related decision impacts while allowing optimised recommendations and retaining physical-controller safety authority.
- Pot Model fidelity properties depend on EDS accuracy through the evapFactor input, but the bounded-error assumption is not yet formalised as a contract.
- SoS-level fidelity reasoning must account for interaction patterns, shared-resource allocation, and timing dependencies rather than merely aggregating local guarantees and errors.
- VDM-RT formal constructs can be exported as FMUs while maintaining verification evidence, creating a pathway toward industrial co-simulation workflows.
7 Threats to Validity
The case study’s validity is constrained by simulation-based validation, domain-specific quality interpretations, and uncertain generalisability beyond greenhouse systems. These boundaries motivate further empirical validation and caution in extending the reported patterns.
- Internal validity: The VDM-RT models are validated through simulation and controlled execution traces rather than physical-hardware deployment.This abstracts away sensor noise, actuator delays, and other hardware imperfections affecting real-world behaviour.
- Construct validity: The four selected DT qualities and their property decompositions reflect one greenhouse-domain interpretation, while other domains may require additional qualities or alternatives.Examples of other qualities include maintainability, explainability, and security.
- External validity: The greenhouse case study’s shared environment and hierarchical control may not capture complexities in manufacturing or energy systems.Examples include safety-critical real-time constraints and legacy-system integration.
- External validity: Generalisability of the quality-instantiation patterns requires empirical validation through further case studies.
8 Conclusion
The study establishes a foundation for verifying individual Digital Twin qualities while identifying challenges that prevent complete compositional verification at the Systems-of-Systems level.
- 8 Conclusion: DT qualities are operationalised as formally verifiable properties instantiated in VDM-RT models.The approach targets relevance, verifiability, substitutability, and fidelity.
- 8 Conclusion: Quality decomposition depends on artefact role: substitutability concerns behavioural agreement, decision-impact preservation, or safe context replacement.These interpretations support role-specific modular verification strategies.
- 8 Conclusion: VDM-RT verification can integrate with industrial co-simulation through FMI-compliant FMU export.The integration connects formal analysis with industrial simulation workflows.
- 8 Conclusion: The case study identifies fidelity error amplification under resource constraints, scope-shifting relevance definitions, and substitutability evolving toward architectural compatibility.These challenges arise when DT artefacts are composed in an SoS.
- 8 Conclusion: Full SoS-level formalisation remains future work because collective behaviours, emergent phenomena, automation, and scalability require further development.The proposed agenda includes global resource constraints, proof automation, termination analysis, and trace comparison.