Model Checking Paxos in Spin

Giorgio Delzanno
(DIBRIS, University of Genova)
Michele Tatarek
(DIBRIS, University of Genova)
Riccardo Traverso
(FBK, Trento)

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.

In Adriano Peron and Carla Piazza: Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014), Verona, Italy, 10th - 12th September 2014, Electronic Proceedings in Theoretical Computer Science 161, pp. 131–146.
Published: 24th August 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: