Search papers, labs, and topics across Lattice.
This paper introduces a type-safe extension to the RTLola stream-based monitoring framework to handle parameterized streams, which represent unbounded sets of stream instances. The key idea is to use a refinement type system to statically guarantee the absence of runtime errors, particularly those related to memory management when dealing with unbounded data domains. While proving the absence of runtime errors is generally undecidable, the refinement type system ensures that all memory references are either successful or have a default value.
Guarantee runtime safety in complex cyber-physical systems with unbounded data domains using a refinement type system for parameterized streams, even though it's generally undecidable.
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.
