用于组合数字孪生验证的体系体系案例研究
A System-of-Systems Case Study for the Verification of Composed Digital Twins
AI总结：
本研究以VDM-RT建模的数字孪生驱动温室体系体系为案例，明确了SoS环境下数字孪生验证框架的基础挑战，提出将单个数字孪生制品形式化的方法，为组合推理提供支撑。
AI中文摘要：
当前，用于构建信息物理系统可靠数字孪生（Digital Twins, DTs）的方法，缺乏关于如何将相关性、可验证性、可替代性和保真度等特性形式化并进行验证的实用指导。在体系体系（System-of-Systems, SoS）中，由于依赖数字孪生的组合，这一需求更为迫切。本研究旨在确定数字孪生验证框架在体系体系环境中应解决的基础挑战，并研究将单个数字孪生制品形式化以推进组合推理的步骤。我们开展了一项基于数字孪生驱动的温室体系体系的案例研究，该体系体系采用VDM-RT（维也纳开发方法实时版）建模，包含可执行形式模型、数字孪生特性的基于属性的说明，以及在体系体系层面尝试组合这些制品时出现的障碍分析。我们探讨了如何将数字孪生特性可操作化为可验证属性集合，识别了支持其验证的形式建模与分析技术及工具。研究揭示，数字孪生特性的解释必须适配不同架构角色，且局部特性保证构成组合推理的假设。体系体系组合的完全形式化与验证被确定为未来工作。
英文摘要：
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.
