Decentralized Runtime Verification for LTL Properties Using Global Clock
Decentralized Runtime Verification for LTL Properties Using Global Clock
复制标题
使用全局时钟对 LTL 属性进行去中心化运行时验证
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Ehsan Khamespanah
中科院分区：
文献类型：
--
作者：
M. A. Dorosty;Fathiyeh Faghih;Ehsan Khamespanah
运行时验证是验证大型复杂系统中关键行为属性的过程，在这种系统中，由于状态空间爆炸而无法进行形式验证。人们已经多次尝试设计用于运行时验证的有效算法。大多数这些算法都有一个正式定义的正确性属性作为参考，并检查系统是否始终满足该属性的要求，或者在运行时的某个时刻无法满足该属性。 LTL 是定义此类属性的常用语言，也是本文重点讨论的语言。运行时验证的主要目标系统之一是分布式系统，该系统由许多使用异步消息传递相互连接的进程组成。分布式系统中的运行时验证有两种方法。第一个由集中式算法组成，其中所有进程将其事件发送到特定的决策进程，该进程跟踪所有事件以评估指定的属性。第二种方法由分布式算法组成，其中进程协作检查指定的属性。集中式算法很简单，但通常涉及向决策过程发送大量消息。它们还面临单点故障以及一个进程的高流量负载问题。另一方面，分布式算法通常更复杂，但一旦实现，就会提供更高的效率。在本文中，我们关注一类异步分布式系统，其中每个进程可以在任意时间改变自己的本地状态并且完全独立于其他进程，同时所有进程共享一个全局时钟。我们提出了一种健全且完整的算法，用于这些系统中 LTL 属性的去中心化运行时验证。
Runtime verification is the process of verifying critical behavioral properties in big complex systems, where formal verification is not possible due to state space explosion. There have been several attempts to design efficient algorithms for runtime verification. Most of these algorithms have a formally defined correctness property as a reference and check whether the system consistently meets the demands of the property or it fails to satisfy the property at some point in runtime. LTL is a commonly used language for defining these kinds of properties and is also the language of focus in this paper. One of the main target systems for runtime verification are distributed systems, where the system consists of a number of processes connecting to each other using asynchronous message passing. There are two approaches for runtime verification in distributed systems. The first one consists of centralized algorithms, where all processes send their events to a specific decision-making process, which keeps track of all the events to evaluate the specified property. The second approach consists of distributed algorithms, where processes check the specified property collaboratively. Centralized algorithms are simple, but usually involve sending a large number of messages to the decision-making process. They also suffer from the problem of single point of failure, as well as high traffic loads towards one process. Distributed algorithms, on the other hand, are usually more complicated, but once implemented, offer more efficiency. In this paper, we focus on a class of asynchronous distributed systems, where each process can change its own local state at any arbitrary time and completely independent of others, while all processes share a global clock. We propose a sound and complete algorithm for decentralized runtime verification of LTL properties in these systems.