Decentralized Runtime Verification of LTL Specifications in Distributed Systems
Decentralized Runtime Verification of LTL Specifications in Distributed Systems
复制标题
分布式系统中 LTL 规范的去中心化运行时验证
DOI：
10.1109/ipdps.2015.95
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Borzoo Bonakdarpour
中科院分区：
文献类型：
--
作者：
Menna Mostafa;Borzoo Bonakdarpour
运行时验证是一种用于基于规范的运行时监控以及大型现实世界系统的轻巧自动化的形式方法。尽管存在许多用于顺序程序的运行时验证的技术，但基于规范的分布式系统的监视，几乎没有工作。在本文中，我们提出了第一种声音和完整的方法，用于为在程序的全局状态下定义的LTL规范的3值语义的异步分布式程序进行运行时验证。我们评估LTL属性的技术的灵感来自分布式计算切片，这是一种将相对于给定谓词提取分布式计算的方法。我们的监视技术已完全分散，因为在检查中分布式程序中的每个过程都保持了监视器自动机的复制品。每个监视器可以根据并发事件的存在维护一组可能的验证判决。我们对模拟飞行无人机群的运行时间监视的实验表明，由于我们的算法设计，监视开销仅按照需要监视的过程和事件的线性顺序增长。
Runtime verification is a lightweight automated formal method for specification-based runtime monitoring as well as testing of large real-world systems. While numerous techniques exist for runtime verification of sequential programs, there has been very little work on specification-based monitoring of distributed systems. In this paper, we propose the first sound and complete method for runtime verification of asynchronous distributed programs for the 3-valued semantics of LTL specifications defined over the global state of the program. Our technique for evaluating LTL properties is inspired by distributed computation slicing, an approach for abstracting distributed computations with respect to a given predicate. Our monitoring technique is fully decentralized in that each process in the distributed program under inspection maintains a replica of the monitor automaton. Each monitor may maintain a set of possible verification verdicts based upon existence of concurrent events. Our experiments on runtime monitoring of a simulated swarm of flying drones show that due to the design of our Algorithm, monitoring overhead grows only in the linear order of the number of processes and events that need to be monitored.