一种分布式动态重配置协议的的形式化验证
分布式、并行与集群计算
2022-05-17 v2
摘要
我们给出了 MongoRaftReconfig（一种分布式动态重配置协议）的机器检验的 TLA+ 安全性证明。MongoRaftReconfig 由 MongoDB（一种复制协议派生自 Raft 共识算法的分布式数据库）设计并在其上实现。我们给出了 MongoRaftReconfig 在 TLA+ 中形式化的归纳不变量，并使用 TLA+ 证明系统（TLAPS）进行了形式化证明。我们还给出了 MongoRaftReconfig 的两个关键安全属性 LeaderCompleteness 和 StateMachineSafety 的 TLAPS 形式化证明。据我们所知，这些是首个针对基于 Raft 的复制系统的动态重配置协议的机器检验归纳不变量与安全性证明。
引用
@article{arxiv.2109.11987,
title = {Formal Verification of a Distributed Dynamic Reconfiguration Protocol},
author = {William Schultz and Ian Dardik and Stavros Tripakis},
journal= {arXiv preprint arXiv:2109.11987},
year = {2022}
}
备注
First two authors contributed equally