运行时验证

监控一条观测轨迹 ​

运行时验证接收系统产生的有限事件前缀

并用监控器更新状态。与路径语义公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。中的全行为集合不同，它只观察本次运行已发生的事件，不能直接量化其他未执行路径。

对 regular finite-trace property，可由有限状态自动机公理库有限状态自动机Finite-state automaton · Finite automaton · Finite-state machine以有限状态压缩输入前缀信息、沿带标号转移读取有限字的通用自动机骨架。实现监控器：

状态摘要此前全部相关历史，使每个新事件只需局部更新。若性质需要无界数据关联，纯有限状态监控器不够，需寄存器、参数化实例或外部存储。

监控器 determinization 可让每个事件只有一个下一状态，便于在线常数时间更新；由 LTL/正则表达式生成的 automaton 可能指数增长。保持 NFA state set 可延迟确定化，但每步需更新一组候选状态。

事件 alphabet 必须包含足够观察。只记录 grant 而不记录对应 request id，无法验证一一响应；加入所有 payload 又可能造成无限字母表，需要 symbolic guard 或参数化 monitor。

三值前缀语义 ​

对无限行为性质，有限前缀常既未证明满足也未证明违反。三值语义可返回

若前缀所有延伸都满足，返回 true；若所有延伸都违反，返回 false；否则 inconclusive。

安全性质 G not bad 一旦观察到 bad 就永久 false，却通常无法在持续系统的任意安全前缀上返回永久 true。co-safety 性质 F done 看到 done 后可永久 true，却无法因暂未看到而返回 false。

把 inconclusive 当作通过，会把尚未发生的活性义务误判为已兑现。

monitorability 问每条无限行为是否有某个有限前缀最终给出稳定 verdict。纯 safety/co-safety 常可单向决定，一般 LTL 性质可能存在永远 inconclusive 的行为，例如请求和授权持续交错而未来仍可改变结论。

有限 trace 语义可以强制日志结束时评价所有义务，但这改变了原无限规格。end 是真实系统终止事件、观测窗口关闭还是日志丢失，必须区分。

请求—响应状态轨迹 ​

监控 G(request -> F grant) 时，可维护 outstanding request 集。事件 request(id) 加入 id，grant(id) 删除对应 id。

轨迹

request(7), request(9), grant(7)

结束时 id 9 仍 outstanding。若日志截断只是观察暂时停止，结论是 inconclusive；若 end 表示系统正式终止，有限 trace 语义可判违反。

只维护一个布尔 pending 会把多个并发请求合并，grant(7) 可能错误清除 request(9) 的义务。监控状态必须匹配事件参数和需求的关联量词。

参数化监控通常为每个 id 建实例。实例可在义务完成后回收，但若性质还允许未来事件引用旧 id，过早 GC 会漏违反；回收条件需从 automaton 的终态和参数作用域证明。

高基数攻击者可不断制造新 id 使监控表无界。容量保护应发出 overflow/unknown，并记录丢弃范围，不能静默淘汰后继续返回 true。

Instrumentation 与观察缺口 ​

监控正确性分两层：从完整事件序列到 verdict 的 automaton 正确；instrumentation 还要保证真实相关事件都被捕获、顺序和参数准确。

异步日志可能重排跨线程事件，采样会漏事件，时钟漂移会改变实时约束。监控器对输入 trace 的正确结论，不能补偿 trace 本身不忠实。

插桩也可能改变调度，隐藏原竞态或引入延迟。低开销与可观察完整性是工程权衡，应在保证中说明 drop policy。

分布式日志只有偏序。不同节点时间戳不能在有漂移时直接给出真实全序；监控器可枚举与 happens-before 一致的线性化，或使用 partial-order semantics。任取一个排序可能把“先认证后访问”判反。

网络重复、重传和 exactly-once 假设也影响事件语义。若同一 logical request 出现两条日志，监控需用唯一标识去重，不能把它们当两个独立义务。

在线、离线与可执行动作 ​

在线监控随系统运行，能及时告警或触发恢复；离线监控分析已保存日志，可用更多内存和双向扫描。两者使用同一性质也可能因日志结束语义不同给出不同 verdict。

enforcement monitor 若阻止、延迟或改写动作，已从观察升级为控制。只有可通过此类编辑保持的性质才能透明 enforcement，且干预本身要进入系统语义。

实时监控使用 event time 还是 processing time 会改变窗口。迟到事件的 watermark 策略必须说明何时关闭窗口；关闭后到达的合法 grant 若被丢弃，可能产生假警报。

对 duration 约束，单调时钟、时钟回拨和跨机同步误差需要预算。普通事件自动机没有这些数值时间假设。

边界 ​

一次运行通过不能证明所有未来或所有输入都通过。运行时验证补充静态证明与模型检查，主要价值是对部署中的实际 trace 给出形式化诊断。

监控器内存也可能无界，例如要关联任意多未完成请求。给表设置容量并丢弃旧义务会改变 soundness；应返回 unknown/overflow，而非继续声称完整验证。

监控器本身可通过模型检查、代码生成证明或 differential testing 验证。若 specification compiler 有 bug，同一错误可能同时存在于生成器和测试 oracle；保留独立语义解释器或证书能缩小共同失效。

隐私场景中对 payload 脱敏可能删除验证所需关系。应先证明抽象事件映射保存性质，再应用最小化，而不是事后发现监控无法区分关键状态。