MLTL（Multi-type）：一种用于网络物理系统的类型化逻辑

《ACM Transactions on Embedded Computing Systems》：MLTL Multi-type: A Typed Logic for Cyber-Physical Systems

针对复杂系统验证中不同信号类型和采样率问题，提出基于MLTL的多类型时间逻辑（MLTLM），在保持直观性的同时支持多源信号验证，优化内存使用，提升嵌入式系统验证效率。

　　

摘要

现代的网络物理系统（CPSoS）运行在复杂的系统体系中，这些系统需要无缝协作以控制安全或任务关键功能。线性时序逻辑（LTL）和任务时序逻辑（MLTL）能够直观地表达CPSoS的需求，用于自动化系统验证和确认。然而，LTL和MLTL都假设公式中变量的所有信号都以相同的采样率和类型（例如时间或距离）进行采样，并且使用标准的“时间”步长。网络物理系统的形式化验证需要验证在不同类型的（子）系统信号上表达的需求，例如在不同时间尺度、距离或抽象层次上采样的信号，而这些信号都包含在同一公式中。之前的研究开发了更具表达能力的逻辑来处理这些类型差异，但牺牲了LTL的直观简洁性。然而，如果能够实现语言规范与形式化规范之间清晰的一一对应关系，将有助于简化验证过程、减少错误、提高效率，并使项目从构思到实现的工作流程更加线性化。验证既需要满足人类解读的透明度，也需要满足自动化推理的可行性，因为CPSoS通常运行在资源有限的嵌入式系统中。为了解决这些挑战，我们提出了任务时序逻辑多类型（MLTLM，Hariharan等人，2022年数值软件验证研讨会），这是一种基于MLTL的逻辑框架。MLTLM允许针对不同类型的有限输入信号（例如传感器信号和本地计算）编写形式化需求，同时保持与LTL和MLTL相同的简洁性。此外，MLTLM还保持了语言需求与其对应形式化规范之间的直接对应关系。另外，在资源受限的硬件上，以预期类型（例如每小时一次的频率对应每小时一次的形式化推理，每秒一次的频率对应每秒一次的形式化推理）进行推理时，所需的内存会显著减少。本文在以下方面扩展了之前的研究：（1）提供了更多关于在同一规范中表达不同类型（例如时间和空间）的示例；（2）省略了研讨会版本中的部分证明内容；（3）证明了MLTLM相比MLTL的简洁性；（4）提供了将最优长度的规范转换为MLTL的最小化方法。