Crash-Resilient Decentralized Synchronous Runtime Verification
Crash-Resilient Decentralized Synchronous Runtime Verification
复制标题
DOI：
10.1109/tdsc.2023.3265566
复制
发表时间：
2024-05
影响因子：
7.3
通讯作者：
Ritam Ganguly;Shokufeh Kazemloo;Borzoo Bonakdarpour
中科院分区：
文献类型：
--
作者：
Ritam Ganguly;Shokufeh Kazemloo;Borzoo Bonakdarpour
验证是一种技术，其中监视进程从运行的系统中提取信息，以评估系统执行是否违反或满足给定的正确性规范。在本文中，我们考虑同步分布式系统的运行时验证，其中一组仅查看系统部分视图的分散监视器可能会出现崩溃故障。在这种情况下，不可避免的是，监视器可能对底层系统有不同的看法，因此，对正确性属性有不同的意见。我们提出了一个基于自动机的同步监控算法，处理$t$t崩溃监视器故障。在我们提出的方法中，本地监视器不传达它们对底层系统的显式阅读。相反，他们发出一个象征性的判决，有效地编码他们的部分意见。这大大降低了通信开销。为此，我们还引入了一种（离线）基于SMT的监视器合成算法，可以最大限度地减少监视消息的大小。我们评估我们的算法在广泛的公式，并观察到平均2.5倍的监视器自动机的状态数增加。
Runtime verification is a technique, where a monitor process extracts information from a running system in order to evaluate whether system executions violate or satisfy a given correctness specification. In this article, we consider runtime verification of synchronous distributed systems, where a set of decentralized monitors that only have a partial view of the system are subject to crash failures. In this context, it is unavoidable that monitors may have different views of the underlying system, and, therefore, have different opinions about the correctness property. We propose an automata-based synchronous monitoring algorithm that copes with $t$t crash monitor failures. In our proposed approach, local monitors do not communicate their explicit reading of the underlying system. Rather, they emit a symbolic verdict that efficiently encodes their partial views. This significantly reduces the communication overhead. To this end, we also introduce an (offline) SMT-based monitor synthesis algorithm, which results in minimizing the size of monitoring messages. We evaluate our algorithm on a wide range of formulas and observe an average of 2.5 times increase in the number of states of the monitor automaton.