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.

翻译：基于流的监控是复杂信息物理系统（如无人机）的一种实时安全保障机制。监控器聚合来自传感器及其他来源的输入数据流，以提供系统健康状况的实时统计与评估。由于监控器属于安全关键组件，必须确保其在运行时不出现错误。当监控器需要处理无界数据域（例如无限数量的空域参与者）时，提供此类保证尤为困难，这要求使用动态数据结构。本文提出了一种将参数化流类型安全地集成到基于流的监控框架RTLola中的方法。参数化流将独立流推广至包含无限数量流实例的集合，并提供系统化的内存管理机制。我们证明，运行时错误的缺失性在一般情况下是不可判定的，但可通过精化类型系统有效确保——该系统保证所有内存引用要么成功执行，要么具有默认值作为后备。我们报告了类型分析在各类基准测试示例规范上的性能表现，包括来自自主飞行器监控的规范。