一句话：利用对称点对点算法的 cutoff，在 TLA+、IVy 与计数器自动机上参数化验证 Chandra-Toueg 故障检测器的安全性与活性。
部分同步分布式算法常按进程数参数化，其正确性依赖消息延迟与进程速度的时间界，自动验证困难。本文对基于部分同步的 Chandra-Toueg 故障检测器进行安全性与活性验证的案例研究。作者形式化一类对称点对点算法，证明其存在 cutoff，且在同步、异步与部分同步下均成立，从而可用小实例模型检测。随后在 TLA+、IVy 和计数器自动机中建模，用计数器或一阶关系编码消息缓冲。评估显示：TLA+ 与计数器自动机证明固定时间界安全性，IVy 证明任意时间界安全性；活性归约为安全性，并用 IVy 归纳不变式验证。
Partial synchrony is a model of computation in many distributed algorithms and modern blockchains. These algorithms are typically parameterized in the number of participants, and their correctness requires the existence of bounds on message delays and on the relative speed of processes after reaching Global Stabilization Time. These characteristics make partially synchronous algorithms parameterized in the number of processes, and parametric in time bounds, which render automated verification of partially synchronous algorithms challenging. In this paper, we present a case study on formal verification of both safety and liveness of the Chandra and Toueg failure detector that is based on partial synchrony. To this end, we first introduce and formalize the class of symmetric point-to-point algorithms that contains the failure detector. Second, we show that these symmetric point-to-point algorithms have a cutoff, and the cutoff results hold in three models of computation: synchrony, asynchrony, and partial synchrony. As a result, one can verify them by model checking small instances, but the verification problem stays parametric in time. Next, we specify the failure detector and the partial synchrony assumptions in three frameworks: TLA+, IVy, and counter automata. Importantly, we tune our modeling to use the strength of each method: (1) We are using counters to encode message buffers with counter automata, (2) we are using first-order relations to encode message buffers in IVy, and (3) we are using both approaches in TLA+. By running the tools for TLA+ and counter automata, we demonstrate safety for fixed time bounds. By running IVy, we prove safety for arbitrary time bounds. Moreover, we show how to verify liveness of the failure detector by reducing the verification problem to safety verification. Thus, both properties are verified by developing inductive invariants with IVy.
@article{paperbot2233,
title = {A case study on parametric verification of failure detectors},
author = {Thanh-Hai Tran and Igor Konnov and Josef Widder},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:17)2023}
}