Type-safe Monitoring of Parameterized Streams

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.

Figures (10)

• Figure 1: Inference rule examples for stream expressions
• Figure 2: Inference rules for the stream instance evaluation
• Figure 3: Evaluation Results
• Figure 4: RTLola value type inference rules
• Figure 5: Value type rules for streams

Theorems & Definitions (18)

• definition 1: Specification
• definition 2: Pacing Types
• definition 3: Specification Semantics
• definition 4: Specification Safety
• definition 5: Stream-Activation
• lemma 1: Failable Semantics
• theorem 1: Abstract-Safety
• theorem 2: Typechecked-Safety
• theorem 3: RTLola Undecidability
• proof