有时属性的分布式监控
软件工程
2024-10-02 v1
摘要
在形式化验证中，运行时监控 consist in observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property。我们考虑分布式设置下的监控问题，适用于给定为可达性定时自动机的属性。在此设置下，系统由多个组件组成，每个组件配备自己的本地时钟和监控器.监控器观察其关联组件上发生的事件，并通过FIFO信道接收来自其他监控器的时间戳事件。由于时钟是本地的，无法实现完美同步，导致时刻不精确。因此，必须将其视为区间，迫使监控器考虑事件可能的重排序。在此背景下，每个监控器旨在基于接收到的事件，在可能的不完整和不精确知识下，尽快为其监控的属性提供一个 verdict。本文提出了一种针对时序属性的在线监控算法，抗时序不精确和来自远程组件的部分信息。我们首先识别监控器可以安全计算 verdict 的日期。随后我们提出一种监控算法，当新信息到达时更新该日期，维护属性可能驻留的状态集合，并相应地更新其 verdict。
引用
@article{arxiv.2410.00465,
title = {Distributed Monitoring of Timed Properties},
author = {Léo Henry and Thierry Jéron and Nicolas Markey and Victor Roussanaly},
journal= {arXiv preprint arXiv:2410.00465},
year = {2024}
}