Stream-based monitoring assesses the health of safety-critical systems by transforming input streams of sensor measurements into output streams that determine a verdict. These inputs are often treated as accurate representations of the physical state, although real sensors introduce calibration and measurement errors. Such errors propagate through the monitor's computations and can distort the final verdict. Affine arithmetic with symbolic slack variables can track these errors precisely, but independent measurement noise introduces a fresh slack variable upon each measurement event, causing the monitor's state representation to grow without bound over time. Therefore, any bounded-memory monitoring algorithm must unify slack variables at runtime in a way that generates a sound approximation. This paper introduces zonotopes as an abstract domain for online monitoring of RLola specifications. We demonstrate that zonotopes precisely capture the affine state of the monitor and that their over-approximation produces a sound bounded-memory monitor. We present a comparison of different zonotope over-approximation strategies in the context of runtime monitoring, evaluating their performance and false-positive rates.

翻译：流式监控通过将传感器测量值的输入流转化为判定结果的输出流，以评估安全关键系统的运行状态。尽管实际传感器存在校准与测量误差，这些输入通常被视作物理状态的精确表征。此类误差会在监控器的计算过程中传播，并可能扭曲最终判定结果。采用符号松弛变量的仿射运算虽能精确追踪这些误差，但独立测量噪声会在每次测量事件中引入新的松弛变量，导致监控器的状态表征随时间无限增长。因此，任何有限内存的监控算法必须在运行时以生成可靠近似的方式统一松弛变量。本文引入zonotope作为在线监控RLola规范的抽象域。我们证明zonotope能精确捕获监控器的仿射状态，且其超近似可产生可靠的有限内存监控器。我们在运行时监控背景下比较了不同zonotope超近似策略，评估了其性能表现与误报率。