信号一阶逻辑的量化监控

运行时监控在执行期间检查部分信号是否满足其规范。信号一阶逻辑（SFO）提供了对此类信号的富有表达力的实时规范，但目前仅支持布尔语义且缺乏工具支持。我们提供了SFO的首个基于鲁棒性的量化语义，使能够表达和评估超越现有形式（如Signal Temporal Logic）的丰富实时属性。为实现在线监控，我们识别了SFO的过去时片段，并给出一种将有界响应SFO公式转化为该片段中等价公式的过去化程序。随后我们开发了一个高效的运行时监控算法，用于该过去时片段，并在一组基准测试上评估其性能，展示了方法的实用性和有效性。据我们了解，这是首个可公开获取的用于在线量化监控完整SFO的原型系统。