Type-safe Monitoring of Parameterized Streams
This work addresses safety assurance for complex systems like unmanned aerial vehicles, but it is incremental as it builds on the existing RTLola framework.
The paper tackled the challenge of ensuring runtime error absence in safety-critical stream-based monitors for cyber-physical systems, particularly with unbounded data domains, by integrating parameterized streams into RTLola with a refinement type system, achieving effective error prevention as demonstrated in benchmarks including autonomous aircraft monitoring.
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.