使用 TLA 和信息泄露控制进行数字孪生体形式化验证

对数字孪生体进行正确性验证可提供形式化保证，确保数字孪生体按预期运行。数字孪生体的验证因虚拟表示、物理环境中的不确定性以及物理与虚拟之间信息的双向流动而具有挑战性。进一步的挑战在于，复杂系统的数字孪生体由分布式组件组成。本文提出了一种方法，用于指定和验证数字孪生体行为，将不可确定的过程转化为可形式化验证的有限状态机。我们使用行动的时间逻辑(TLA)创建规范，该规范是一种实现抽象，定义正确系统行为所需的属性。我们的ethods 包括一种对形式安全属性的新型弱化，允许在保持理论保证的同时实现受控的信息泄露。我们在无人机数字孪生体上演示了此方法，验证了物理-虚拟和虚拟-数字数据流的同步，以检测意外的误对齐。