Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

技术摘要：利用 STL 重访同步观测器用于 Lustre 的运行时验证

问题陈述
信号时序逻辑 (STL) 是定义赛博物理系统 (CPS) 时间安全性属性的标准形式化方法，尤其适用于运行时验证。然而，现有的 STL 工具通常运行在预录制或模拟信号、或抽象自动机模型上，而非运行在实际部署的可执行代码上。因此，对于嵌套 STL 属性，缺乏一种能够与被监测系统同步运行的、具有可执行运行时等价语义的方法。此外，虽然像 Lustre 这样的同步语言使用“同步观测器”进行静态验证，但这些观测器在运行时验证方面的潜力尚未得到充分探索。一个具体的挑战在于处理在线监测中的“三值”特性：由于有界时间算子会向未来观察，监测器无法在每个时钟滴答（tick）时立即做出判定，这导致在得出确定性结论之前存在延迟。

方法论
作者提出了一种技术，将同步片段 STL (SSTL) 直接编译为 Lustre 中的同步观测器。该方法的核心是将嵌套公式“展开”（unrolling）为一组有限的非嵌套义务，每个义务监测一个固定的离散时间滴答窗口。

1. 三值流式语义： 该方法采用了 Kleene 三值语义（def_true、def_false、unknown）。在每个滴答，观测器根据目前观察到的前缀发出判定。Unknown 表示公式的时间视界（horizon）尚未结束。这通过代表确定真值和确定假值的两个布尔信号 (pos, neg) 来实现。
2. 原语构建 (until_leaf)： 作者合成了一个单一且可重用的 Lustre 节点 until_leaf，它实现了有界“直到”（until）算子 ($U_{[a,b]}$)。该原语跟踪一个前置条件（“存活”信号）和一个后置条件（“发现”信号）在特定窗口内的表现。它在找到见证者时发出 def_true，并在提前终止（前置条件失败）或窗口到期时发出 def_false。
3. 递归合成： 嵌套公式通过自底向上进行合成。系统为外层算子所需的每一个起始偏移量实例化对应的 until_leaf 原语副本。这些副本使用 Kleene 逻辑规则（包括与、或、非运算）连接在一起。
   • 对于有界算子 ($\square_{[a,b]}$, $\diamond_{[a,b]}$)，合成过程会将公式展开为对应于区间内每个起始偏移量的叶子集合。
   • 对于在自由运行系统中常见的无界全局算子 ($\square$)，作者引入了一种移位寄存器结构。该结构不实例化无限个观测器，而是使用大小为 $H+1$（其中 $H$ 是内部视界）的寄存器进行状态回收，从而使监测器能够无限期地跟踪内部公式的“存活”副本。
4. 可视化： 提供了一个基于浏览器的交互式工具，用于在可编辑的轨迹上渲染嵌套观测器的三值判定，以辅助复杂、嵌套时间行为的调试与直观理解。

核心贡献

1. 可执行在线监测： 该技术合成的观测器与系统在同一种同步语言 (Lustre) 中编译在一起，与实际的可执行代码同步运行，而非运行在模拟数据上。
2. 任意嵌套的模块化编译： 与以往工作（如 Bellanger 等人）仅限于非嵌套算子的不同，本方法支持任意嵌套的有界 SSTL 属性。
3. 无界外层算子： 该方法允许使用全局无界外层算子 ($\square$)，适用于监测自由运行系统，同时保持内部结构的有界性。
4. 双重用途： 生成的观测器具有双重用途：它们既作为运行时监测器，同时也作为 Kind2 模型检查器的静态验证义务（其生成过程无需单独的模型）。
5. 用于运行时的三值语义： 实现提供了因果 Kleene 判定，允许监测器在轨迹允许的情况下尽早提交确定性答案，通常在达到完整的公式视界之前即可完成。

结果与评估
作者在两个案例研究上评估了该技术：弹簧-质量块系统以及包含紧急制动的跟车自适应巡航控制 (ACC) 场景。

• 正确性： 所有合成的观测器均通过 Kind2 模型检查器进行了验证。运行时判定与静态判定在每个属性上均保持一致（包括互斥不变性 $pos \land neg = \text{false}$）。
• 性能： 观测器被编译为 C 代码并通过 lv6 解释器执行。每个滴答的执行成本经测量在纳秒级（根据复杂度在 ~6.7 ns 至 ~206.5 ns 之间），远低于典型的毫秒级控制周期，证实了其在线部署的可行性。
• 提前终止： 三值语义证明是有效的；在案例研究中，有界属性在达到其理论视界之前就已确定了结论。例如，一个深度嵌套的属性 ($P3$) 提前 15 个滴答完成了判定。
• 无界行为： 无界 $\square$ 算子作为一个仅限证伪的机制运行，当发生违规时（例如间距跌破安全阈值）能正确锁定为 def_false，否则保持为 unknown。

意义与主张
本文声称弥合了同步 CPS 中形式化规范与可执行运行时监测之间的鸿沟。通过在系统的语言中直接合成观测器，作者消除了在抽象模型上进行验证与部署代码之间存在的“建模差距”。该工作证明了复杂的嵌套时间属性可以在低延迟和高可靠性的条件下进行在线监测。作者将此工作定位为 Bellanger 等人 [5] 的扩展，专门解决了关于嵌套深度以及侧重于静态验证的局限性。该贡献被呈现为一种系统性的合成技术，在显式三值语义下具有完备性和可靠性，并通过运行时执行和静态模型检查得到了验证。

局限性
作者承认存在三个主要局限：

1. 状态爆炸： 叶子节点的数量是窗口宽度的乘积，这会导致观测器规模随大区间（例如 $\diamond_{[0,100]}$）呈指数级增长。
2. 封闭系统假设： 案例研究将受控对象（Plant）在 Lustre 内部建模为一个封闭系统。监测带有外部传感器输入的真实开放系统仍是未来的研究步骤。
3. 离散域： 当前方法严格在采样、离散化的领域内运行，尚未支持连续的 STL 鲁棒性语义。