在参数化通信延迟条件下实时系统的有效运行时验证

《Formal Aspects of Computing》：Efficient Runtime Verification of Real-Time Systems under Parametric Communication Delays

Timed Büchi自动机为实时系统需求提供高度 expressive 形式化描述，其符号执行可在线监控测试嵌入式系统。但实际应用中因监测设备电路引入的波动性参数延迟导致直接构造失效，本文提出纯基于区域划分的在线监控算法，可精确处理此类延迟而不需重复参数化时序自动机验证，并在Uppaal工具上验证了有效性。

　　

摘要

定时Büchi自动机为表达实时系统的需求提供了一种非常强大的形式化方法。通过对系统产生的轨迹进行符号执行，可以实现嵌入式实时系统的在线监控和主动测试。然而，这种直接构建方法只有在轨迹观测是即时进行的情况下才有效，即监控器（或测试工具）能够为其观测到的操作分配精确的时间戳。实际上，由于连接被观测系统与监控或测试设备的电路引入了大量的、且不断变化的参数延迟，这种情况很少发生。

我们提出了基于区域的在线监控和测试算法，这些算法能够精确处理这些参数延迟，而无需采用成本高昂的参数化定时自动机验证程序。我们已在实时模型检查工具Uppaal的基础上实现了这些算法，并报告了初步的积极结果。