Model Checking Paxos in Spin
Logic in Computer Science
2014-08-27 v1 Distributed, Parallel, and Cluster Computing
Discrete Mathematics
Abstract
We present a formal model of a distributed consensus algorithm in the executable specification language Promela extended with a new type of guards, called counting guards, needed to implement transitions that depend on majority voting. Our formalization exploits abstractions that follow from reduction theorems applied to the specific case-study. We apply the model checker Spin to automatically validate finite instances of the model and to extract preconditions on the size of quorums used in the election phases of the protocol.
Keywords
Cite
@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}
}
Comments
In Proceedings GandALF 2014, arXiv:1408.5560