Organising LTL monitors over distributed systems with a global clock
Organising LTL monitors over distributed systems with a global clock
复制标题
DOI：
10.1007/s10703-016-0251-x
复制
发表时间：
2014-09
影响因子：
0.8
通讯作者：
C. Colombo;Yliès Falcone
中科院分区：
文献类型：
--
作者：
C. Colombo;Yliès Falcone
想要监视分布式系统的用户通常喜欢通过直接指定全局系统行为的正确性属性来抽象系统的体系结构。为了支持这种抽象，属性的编译不仅涉及监控算法的典型选择，还涉及组件网络中子监控器的组织。现有的方法，考虑在分布式系统的LTL属性的上下文中与全球时钟，包括所谓的编排和迁移方法。在编排方法中，中央监视器接收来自所有子系统的事件。在迁移方法中，LTL公式在子系统之间传输以收集本地信息。我们提出了第三种组织子监视器的方法：编排，其中监视器被组织为分布式系统中的一棵树，每个孩子都将中间结果反馈给其父级。我们通过展示如何从LTL公式合成网络来形式化基于编排的去中心化监控，并给出了在LTL网络之上工作的去中心化监控算法。我们证明了算法的正确性，并实现了它在一个基准测试工具。我们还报告了一项实证调查，比较了这三种方法对分散监控的几个问题：由于通信延迟，交换的消息的数量和大小以及达到判决所需的执行步骤的数量而导致的判决延迟。
Users wanting to monitor distributed systems often prefer to abstract away the architecture of the system by directly specifying correctness properties on the global system behaviour. To support this abstraction, a compilation of the properties would not only involve the typical choice of monitoring algorithm, but also the organisation of submonitors across the component network. Existing approaches, considered in the context of LTL properties over distributed systems with a global clock, include the so-called orchestration and migration approaches. In the orchestration approach, a central monitor receives the events from all subsystems. In the migration approach, LTL formulae transfer themselves across subsystems to gather local information. We propose a third way of organising submonitors: choreography, where monitors are organised as a tree across the distributed system, and each child feeds intermediate results to its parent. We formalise choreography-based decentralised monitoring by showing how to synthesise a network from an LTL formula, and give a decentralised monitoring algorithm working on top of an LTL network. We prove the algorithm correct and implement it in a benchmark tool. We also report on an empirical investigation comparing these three approaches on several concerns of decentralised monitoring: the delay in reaching a verdict due to communication latency, the number and size of the messages exchanged, and the number of execution steps required to reach the verdict.