预测性Varanus：结合CSP一致性监控与预测性LTL运行时验证

中文摘要 AI 辅助

运行时验证非常适合自主和机器人系统，因为它检查执行期间实际观察到的行为。然而，其主要局限性在于它通常是反应式的：监控器只有在系统已经执行了不良事件之后才能检测到违规。在故障代价高昂或不安全的领域，这可能为时已晚。在本文中，我们提出了预测性Varanus，一个两阶段验证流水线，它将Varanus（一个使用进程代数通信顺序进程（CSP）编写的模型的运行时验证器）与LTL的预测性运行时验证相结合。首先使用CSP模型作为观察事件轨迹上的一致性门；然后将同一模型转换为Büchi自动机，该自动机约束预测性LTL监控器探索的未来。通过这种方式，模型外行为被立即拒绝，而模型一致的前缀可以被分类为已经保证满足、已经强制违反或对于被监控的时间属性仍不确定。我们形式化了组合监控器，解释了其实现，并在一个用于核仓库检查的机器人漫游车上说明了该方法。案例研究展示了CSP验证和预测性LTL的组合如何能够比标准运行时监控提供更早的判定，同时重用现有的设计时CSP模型。

英文摘要

Runtime Verification is well suited to autonomous and robotic systems because it checks the behaviour that is actually observed during execution. Its main limitation, however, is that it is usually reactive: the monitor detects a violation only after the system has already performed a bad event. This can be too late in domains where failures are costly or unsafe. In this paper we present PREDICTIVE VARANUS, a two-stage verification pipeline that combines VARANUS, a runtime verifier that uses models written in the process algebra Communicating Sequential Processes (CSP), with predictive runtime verification for LTL. A CSP model is first used as a conformance gate over the observed event trace; the same model is then translated into a Buchi automaton that constrains the futures explored by a predictive LTL monitor. In this way, out-of-model behaviour is rejected immediately, while model-consistent prefixes can be classified as already guaranteeing satisfaction, already forcing violation, or still being inconclusive for the monitored temporal property. We formalise the combined monitor, explain its implementation, and illustrate the approach on a robotic rover for nuclear-store inspection. The case study shows how the combination of CSP validation and predictive LTL can provide earlier verdicts than standard runtime monitoring while reusing an existing design-time CSP model.

发表机构

• University of Modena and Reggio Emilia（摩德纳与雷焦艾米利亚大学）
• University of Nottingham（诺丁汉大学）
• University of York（约克大学）

机构由 AI 辅助整理，请以论文原文为准。