利用假设在部分可观测性下有效监控实时性质
形式语言与自动机理论
2025-07-30 v2
摘要
时序性质的运行时验证对于确保实时系统的正确性和可靠性至关重要,特别是在信息物理系统中。该领域的一个重大挑战是有效预测性质的失败或成功,尤其是在处理部分可观测系统时。本文通过为连续实时环境开发一种基于假设的运行时验证(ABRV)方法来解决这些挑战。我们的方法利用关于系统行为的假设(指定为时间自动机),使监控器能够预测未来结果并处理不可观测的系统部分,例如内部故障。待监控的性质使用度量区间时序逻辑(MITL)指定。该方法还包括使用时间约束序列对具有数据和时间不确定性的观测进行形式化。我们提出了一种基于区域的在线算法来计算监控判定,该算法在UPPAAL工具之上实现。在概念验证案例上的实验评估证明了该方法的可行性和有效性,说明了假设如何促进更早的判定、实现对依赖于不可观测事件的性质的监控,并提供对可扩展性的见解。
引用
@article{arxiv.2409.05456,
title = {Exploiting Assumptions for Effective Monitoring of Real-Time Properties under Partial Observability},
author = {Alessandro Cimatti and Thomas M. Grosen and Kim G. Larsen and Stefano Tonetta and Martin Zimmermann},
journal= {arXiv preprint arXiv:2409.05456},
year = {2025}
}