Stream-based monitoring is a runtime verification approach where a monitor aggregates streams of input data from sensors and other sources to give real-time statistics and assessments of a system's health. One of the central challenges in designing reliable stream-based monitors is to deal with the asynchronous nature of data streams: in concrete applications, the different sensors being monitored produce values at different speeds, and it is the monitor's responsibility to correctly react to the asynchronous arrival of different streams of values. To ease this process, modern frameworks for stream-based monitoring such as RTLola enable users to finely specify data synchronization policies via a system of pacing annotations. While this feature simplifies the design of monitors, it can also lead users to write inconsistent policies, where synchronization between two streams is explicitly requested via annotations, but cannot always be achieved. To mitigate this issue, this paper presents pacing types, a novel type system implemented in RTLola to ensure that monitors for asynchronous streams are free of timing inconsistencies. We give a formal semantics to pacing annotations for a core fragment of RTLola, and present a soundness proof of the pacing type system. For an additional level of guarantees, we machine-checked the soundness proof using the Rocq proof assistant.

翻译：基于流的监控是一种运行时验证方法，其中监控器聚合来自传感器及其他来源的输入数据流，以实时提供系统运行状态的统计与评估。在设计可靠的流式监控器时，核心挑战之一在于应对数据流的异步特性：具体应用中，不同被监控传感器的数据生成速率各异，监控器需正确应对不同数值流的异步到达。为简化此过程，RTLola等现代流式监控框架允许用户通过分步标注系统精细指定数据同步策略。尽管该特性简化了监控器设计，但也可能导致用户编写不一致的策略——即通过标注显式请求两数据流同步，却无法始终实现。为解决此问题，本文提出分步类型（pacing types），一种在RTLola中实现的新型类型系统，确保异步流监控器不存在时序不一致性。我们为RTLola核心片段的分步标注给出了形式化语义，并证明了分步类型系统的正确性。为提供更高层次保障，我们使用Rocq证明助手对正确性证明进行了机器验证。