基于 RTLola 的主动监控:一种规范引导的调度方法
计算机科学中的逻辑
2025-07-29 v1
摘要
基于流的监控是一种已确立的运行时验证方法,将表示被监控系统传感器读取的输入流与捕获过滤或聚合结果的输出流相关联。在此类方法中,监控器是一个被动的外部组件,不断接收被观察系统的传感器数据。这种 setup 假设系统不论监控器的当前需求如何,都决定发送什么数据以及何时发送。这在许多应用中都可能导致通信资源的低效使用——特别是当资源受限的环境中,如自动飞行器,由于能源、尺寸或重量有限。在本文中,我们提出使监控器成为一个主动组件,其基于当前内部状态决定查询哪些传感器以及查询频率。这种行为由规范中的调度注释驱动,这些注释引导带宽向最相关数据动态分配,从而提高监控效率。我们采用基于流的规范语言 RTLola 来演示我们的方法,并通过评估来自航空航天领域的规范来评估性能。与以固定频率采样所有输入的监控器相比,在相同带宽使用下,我们的方法能显著更快地检测到规范违规。
引用
@article{arxiv.2507.20615,
title = {Active Monitoring with RTLola: A Specification-Guided Scheduling Approach},
author = {Jan Baumeister and Bernd Finkbeiner and Frederik Scheerer},
journal= {arXiv preprint arXiv:2507.20615},
year = {2025}
}