Model Checking of Fault-Tolerant Algorithms for the Dependability of Distributed Systems

一致性算法是实现容错分布式系统的核心算法，提出了一种机械验证方法来验证一致性算法。实验结果表明，当假设一个抽象的分布式系统模型时，我们的方法可以扩展到大约十个计算节点。

A mechanical verification approach is proposed to verify consensus algorithms, which are core algorithms that can be used in implementing fault-tolerant distributed systems. Experiment results show that when an abstract distributed system model is assumed, our approach can scale up to around ten computing nodes.