Pacing Types: Safe Monitoring of Periodic and Conditional Streams
Florian Kohn
Runtime monitoring is a safety assurance mechanism that validates a system’s behavior against a formal specification at runtime. In stream-based monitoring, a monitor aggregates and transforms input streams, such as sensor readings or system metrics, into output streams that provide temporal or statistical assessments of system health. In practice, input streams may arrive at different rates because sensors operate at different frequencies, requiring the monitor to correctly handle asynchronous data arrival. Frameworks such as RTLola address this through pacing annotations, which specify precisely when streams must be evaluated.
Since the monitor is part of a safety-critical system, preventing runtime errors is essential. However, inconsistent pacing annotations can introduce subtle errors that result in attempts to access unavailable stream values.
This thesis extends RTLola’s type-based analysis to support periodic and conditionally evaluated streams, both of which are needed to specify complex real-time behavior. Conditionally evaluated streams use when clauses to refine evaluation time points based on boolean conditions. This allows, for example, the exclusion of time points where a division by zero would occur. Periodic streams emit values at fixed intervals, enabling the monitor to compute system verdicts independently of input arrival, such as for detecting deadlocks or failed sensors. We encode periodically paced streams as a special case of when clauses and prove type-system soundness with respect to RTLola’s relational semantics. This guarantees that pacing annotations are consistent such that specifications can be safely monitored without invalid data accesses.
Master Thesis.