基于理性监视器的 imperfect 信息下运行时验证
形式语言与自动机理论
2024-08-22 v1 计算机科学中的逻辑
软件工程
摘要
信任软件系统，尤其是自主系统，具有挑战性。为此，我们可以使用形式化验证技术来确保这些系统按预期行为运行。运行时验证 (Runtime Verification, RV) 是一种领先且轻量级的验证方法，能够在执行期间验证系统行为。然而，传统的 RV 假设监控器拥有完美的信息，即监控组件能够准确地感知一切。这一假设在特别是自主系统在真实环境中运行时常常不成立，因为传感器可能存在故障。此外，传统的 RV 认为监控器是被动的，缺乏解释系统信息的能力，因而无法处理不完整的数据。在本工作中，我们将标准的线性时序逻辑 (Linear Temporal Logic) 属性 RV 扩展到监控器拥有 imperfect 信息且具有理性行为的情景中。我们概述了更新验证管道所需的工程步骤，并通过涉及机器人系统的案例研究展示了我们的实现。
引用
@article{arxiv.2408.11627,
title = {Runtime Verification via Rational Monitor with Imperfect Information},
author = {Angelo Ferrando and Vadim Malvone},
journal= {arXiv preprint arXiv:2408.11627},
year = {2024}
}