Search papers, labs, and topics across Lattice.
This paper introduces pacing types, a novel type system for the RTLola stream-based monitoring framework, designed to ensure the consistency of data synchronization policies in asynchronous data streams. The type system statically checks for timing inconsistencies arising from pacing annotations, which specify data synchronization policies between streams. The soundness of the pacing type system is formally proven and machine-checked using the Rocq proof assistant, providing strong guarantees about the absence of timing errors.
RTLola users can now catch subtle timing inconsistencies in asynchronous stream monitors *before* runtime, thanks to a new type system.
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.
