在Spin中模型检验Paxos
计算机科学中的逻辑
2014-08-27 v1 分布式、并行与集群计算
离散数学
摘要
我们提出了一个分布式共识算法的形式化模型，使用可执行规范语言Promela，并扩展了一种新型守卫，称为计数守卫，用于实现依赖于多数投票的转换。我们的形式化利用了从应用于特定案例研究的归约定理中得出的抽象。我们应用模型检验器Spin自动验证模型的有限实例，并提取协议选举阶段使用的法定人数大小的前置条件。
引用
@article{arxiv.1408.5962,
title = {Model Checking Paxos in Spin},
author = {Giorgio Delzanno and Michele Tatarek and Riccardo Traverso},
journal= {arXiv preprint arXiv:1408.5962},
year = {2014}
}
备注
In Proceedings GandALF 2014, arXiv:1408.5560