多属性时序逻辑监控

运行时验证允许对单个执行轨迹上的时序逻辑规范进行检查，为彻底的形式验证提供可扩展的替代方案。然而，实际系统需要同时满足数十到数百个时序属性；然而，现有方法在孤立监控每个属性，导致冗余计算和可扩展性有限。本文提出一种在线多属性监控框架，将past-time LTL和MTL规范编译为共享的有向无环图（DAG）的子公式，其中每个属性有一个输出。不同于构建独立监控器的先前方法，我们的方法将组合顺序网络基础的时序逻辑监控构造扩展到共享设置，实现跨属性复用中间结果的同时保持各自结构。我们方法的核心是一种基于arena分配、双缓冲布局的数据导动执行模型，存储每个子公式的中间结果于紧凑、连续内存中。该设计有利于空间局部性，实现最小开销的增量更新。实验结果表明，在多属性配置下，与传统单属性监控相比，单属性吞吐量提升达2倍至4.5倍，多属性配置下提升6倍至12倍，使大规模规范集的可扩展性得以实现，并可部署于高性能和资源受限系统。