使用古典模型检验与统计模型检验验证数字孪生体

随着数字技术的不断普及，数字孪生体（digital twin，DT）概念在产业界和学术界受到广泛关注。虽然存在多种关于数字孪生体的定义，但大多数定义都聚焦于实物对象或过程的虚拟实体（virtual entity，VE）的存在，这些实体通常由相互关联的模型组成，这些模型彼此交互，并因与真实世界对象持续同步而不断发生变化。这些交互可能在执行时导致不一致，由于其高度随机性和/或时间关键性，可能导致不可取的行为。此外，VE因与真实世界对象同步而持续变化的特性进一步增加了这些交互及其相应模型执行时间带来的复杂性，这可能影响其在运行时的整体功能。由此需要对VE进行（连续）验证，以确保其在运行时行为一致，通过遵循如死锁自由、功能正确性、活性和及时性等期望属性来实现。在某些关键属性（如死锁自由）只能使用古典模型检验来验证；而统计模型检验则提供了建模实际随机时间行为的可能性。因此，我们提出使用这两种技术来验证VE的正确性以及满意于期望属性的能力。我们呈现将这些技术应用于自动驾驶卡车数字孪生体的观察和发现。来自这些验证技术的结果表明，该数字孪生体符合死锁自由和功能正确性，但不符合及时性属性。