Decentralised LTL monitoring
Decentralised LTL monitoring
复制标题
DOI：
10.1007/s10703-016-0253-8
复制
发表时间：
2011-11
影响因子：
0.8
通讯作者：
A. Bauer;Yliès Falcone
中科院分区：
文献类型：
--
作者：
A. Bauer;Yliès Falcone
想要监视分布式或基于组件的系统的用户通常将它们视为整体系统，从外部看，它们表现出统一的行为，而不是许多组件显示许多局部行为，这些局部行为共同构成了系统的全局行为。这种级别的抽象通常是合理的，对那些可能希望根据线性时间时态逻辑（LTL）公式指定系统全局行为的用户隐藏了实现细节。然而，随之而来的问题是，如何在一个没有中心数据收集点的分布式系统中监控这样的规范，在分布式系统中，所有组件的本地行为都是可观察的。在这种情况下，LTL规范需要分解成子公式，而子公式又需要分布在组件的本地附加监视器之间，每个监视器只能看到全局行为的不同部分。本文的主要贡献是一种用于分配和监控LTL公式的算法，使得局部监视器可以单独检测满足或违反规范。我们提出了一个实现，并表明我们的算法在检测满足/违反规范方面只引入了一个可以忽略不计的延迟。此外，我们的实际结果表明，本地监视器引入的通信开销通常低于需要发送到中央数据收集点的消息数量。此外，我们的实验强化了该算法在不同系统/通信拓扑和/或系统事件随时间分布的不同应用环境中表现良好的论点。
Users wanting to monitor distributed or component-based systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behaviour as opposed to many components displaying many local behaviours that together constitute the system’s global behaviour. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the system’s global behaviour in terms of a linear-time temporal logic (LTL) formula. However, the problem that arises then is how such a specification can actually be monitored in a distributed system that has no central data collection point, where all the components’ local behaviours are observable. In this case, the LTL specification needs to be decomposed into sub-formulae which, in turn, need to be distributed amongst the components’ locally attached monitors, each of which sees only a distinct part of the global behaviour. The main contribution of this paper is an algorithm for distributing and monitoring LTL formulae, such that satisfaction or violation of specifications can be detected by local monitors alone. We present an implementation and show that our algorithm introduces only a negligible delay in detecting satisfaction/violation of a specification. Moreover, our practical results show that the communication overhead introduced by the local monitors is generally lower than the number of messages that would need to be sent to a central data collection point. Furthermore, our experiments strengthen the argument that the algorithm performs well in a wide range of different application contexts, given by different system/communication topologies and/or system event distributions over time.