Type-safe Monitoring of Parameterized Streams

TL;DR

This paper introduces a type-safe approach to monitoring parameterized streams in real-time safety-critical systems, ensuring error-free operation despite unbounded data domains using a refinement type system.

Contribution

It extends the RTLola monitoring framework with parameterized streams and a refinement type system to guarantee memory safety in unbounded data scenarios.

Findings

Type analysis effectively prevents runtime errors in benchmarks.

The approach scales to autonomous aircraft monitoring specifications.

Memory safety is achieved through systematic refinement types.

Abstract

Stream-based monitoring is a real-time safety assurance mechanism for complex cyber-physical systems such as unmanned aerial vehicles. The monitor aggregates streams of input data from sensors and other sources to give real-time statistics and assessments of the system's health. Since the monitor is a safety-critical component, it is mandatory to ensure the absence of runtime errors in the monitor. Providing such guarantees is particularly challenging when the monitor must handle unbounded data domains, like an unlimited number of airspace participants, requiring the use of dynamic data structures. This paper provides a type-safe integration of parameterized streams into the stream-based monitoring framework RTLola. Parameterized streams generalize individual streams to sets of an unbounded number of stream instances and provide a systematic mechanism for memory management. We show that the absence of runtime errors is, in general, undecidable but can be effectively ensured with a refinement type system that guarantees all memory references are either successful or backed by a default value. We report on the performance of the type analysis on example specifications from a range of benchmarks, including specifications from the monitoring of autonomous aircraft.