测量噪声下基于流的在线与离线监控
Stream-based Online and Offline Monitoring under Measurement Noise
浏览论文内容
中文总结 AI 辅助
针对网络物理系统传感器测量噪声导致监控误差放大的问题，提出鲁棒流监控扩展RLola，实现带恒定内存的在线监控与可检测在线遗漏违规的离线监控，在RTLola框架中验证了算法性能。
中文摘要 AI 辅助
基于流的监控是一种用于网络物理系统的运行时验证方法，它将传感器读数等输入数据流转换为聚合统计量和关于系统安全性的判定结果。通常假设输入流上的值代表物理世界的完全准确测量值，但实际上，物理传感器易受测量噪声和误差影响，这些误差会被监控器内的处理与聚合步骤进一步放大。本文介绍RLola，它是流规范语言Lola的鲁棒扩展，RLola纳入了松弛变量的概念，松弛变量可符号化表示测量噪声，同时避免区间算术的混叠问题。我们提出了针对RLola规范的在线和离线监控算法。由于监控RLola规范通常可能需要无界内存，我们识别出RLola的一个丰富片段，该片段可自动转换为在线监控时具有保证恒定内存使用的监控器。在线RLola监控器观测实时系统并提供关于指定断言当前状态的实时反馈；基于可满足性模理论的离线算法分析完整系统轨迹，确定是否存在在所有时间点满足所有断言的假设真实轨迹，因此离线算法可检测到在线算法可能遗漏的违规情况。我们在现有RTLola框架中实现这些算法，并基于一个综合示例评估它们的精度和运行时间。
英文摘要
Stream-based monitoring is a runtime verification approach for cyber-physical systems that translates streams of input data, such as sensor readings, into streams of aggregate statistics and verdicts about the safety of the system. It is usually assumed that the values on the input streams represent fully accurate measurements of the physical world. In reality, however, physical sensors are prone to measurement noise and errors. These errors are further amplified by the processing and aggregation steps within the monitor. This paper introduces RLola, a robust extension of the stream-based specification language Lola. RLola incorporates the concept of slack variables, which symbolically represent measurement noise while avoiding the aliasing problem of interval arithmetic. We present algorithms for both online and offline monitoring of RLola specifications. Since monitoring RLola specifications may require unbounded memory in general, we identify a rich fragment of RLola that can be automatically translated into monitors with guaranteed constant memory usage for online monitoring. An online RLola monitor observes a live system and provides real-time feedback on the current status of specified assertions. A satisfiability-modulo-theories-based offline algorithm analyzes complete system traces and determines whether a hypothetical ground-truth trace exists that satisfies all assertions at all time points. The offline algorithm can therefore detect violations that the online algorithm may miss. We implement these algorithms in the existing RTLola framework and evaluate their precision and running time based on a comprehensive example.
