Graph- versus Vector-Based Analysis of a Consensus Protocol

Giorgio Delzanno; Arend Rensink; Riccardo Traverso

doi:10.4204/EPTCS.159.5

Graph- versus Vector-Based Analysis of a Consensus Protocol

Giorgio Delzanno, Arend Rensink, Riccardo Traverso

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

140 Downloads (Pure)

Abstract

The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.

Original language	Undefined
Title of host publication	Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)
Editors	Dragan Bošnački, Stefan Edelkamp, Alberto Lluch Lafuente, Anton Wijs
Publisher	EPTCS
Pages	44-57
Number of pages	14
DOIs	https://doi.org/10.4204/EPTCS.159.5
Publication status	Published - Apr 2014
Event	3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014 - Grenoble, France Duration: 5 Apr 2014 → 5 Apr 2014

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	EPTCS
Volume	159
ISSN (Print)	2075-2180
ISSN (Electronic)	2075-2180

Workshop

Workshop	3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014
Period	5/04/14 → 5/04/14
Other	5 April 2014

Keywords

EWI-24980
GROOVE
Graph Transformation
IR-91953
Consensus Protocols
Model Checking
METIS-305983
SPIN

Access to Document

10.4204/EPTCS.159.5

GRAPHITE2014.5

http://eprints.eemcs.utwente.nl/24980/01/paper.cgi?GRAPHITE2014.5.pdf

Cite this

Delzanno, G., Rensink, A., & Traverso, R. (2014). Graph- versus Vector-Based Analysis of a Consensus Protocol. In D. Bošnački, S. Edelkamp, A. Lluch Lafuente, & A. Wijs (Eds.), Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014) (pp. 44-57). (Electronic Proceedings in Theoretical Computer Science; Vol. 159). EPTCS. https://doi.org/10.4204/EPTCS.159.5

Delzanno, Giorgio ; Rensink, Arend ; Traverso, Riccardo. / Graph- versus Vector-Based Analysis of a Consensus Protocol. Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). editor / Dragan Bošnački ; Stefan Edelkamp ; Alberto Lluch Lafuente ; Anton Wijs. EPTCS, 2014. pp. 44-57 (Electronic Proceedings in Theoretical Computer Science).

@inproceedings{55767b7ab50b472fb015682be411c0dd,

title = "Graph- versus Vector-Based Analysis of a Consensus Protocol",

abstract = "The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.",

keywords = "EWI-24980, GROOVE, Graph Transformation, IR-91953, Consensus Protocols, Model Checking, METIS-305983, SPIN",

author = "Giorgio Delzanno and Arend Rensink and Riccardo Traverso",

note = "10.4204/EPTCS.159.5 ; 3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014 ; Conference date: 05-04-2014 Through 05-04-2014",

year = "2014",

month = apr,

doi = "10.4204/EPTCS.159.5",

language = "Undefined",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "EPTCS",

pages = "44--57",

editor = "Dragan Bo{\v s}na{\v c}ki and Stefan Edelkamp and {Lluch Lafuente}, Alberto and Anton Wijs",

booktitle = "Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)",

}

Delzanno, G, Rensink, A & Traverso, R 2014, Graph- versus Vector-Based Analysis of a Consensus Protocol. in D Bošnački, S Edelkamp, A Lluch Lafuente & A Wijs (eds), Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). Electronic Proceedings in Theoretical Computer Science, vol. 159, EPTCS, pp. 44-57, 3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014, 5/04/14. https://doi.org/10.4204/EPTCS.159.5

Graph- versus Vector-Based Analysis of a Consensus Protocol. / Delzanno, Giorgio; Rensink, Arend; Traverso, Riccardo.
Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). ed. / Dragan Bošnački; Stefan Edelkamp; Alberto Lluch Lafuente; Anton Wijs. EPTCS, 2014. p. 44-57 (Electronic Proceedings in Theoretical Computer Science; Vol. 159).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Graph- versus Vector-Based Analysis of a Consensus Protocol

AU - Delzanno, Giorgio

AU - Rensink, Arend

AU - Traverso, Riccardo

N1 - 10.4204/EPTCS.159.5

PY - 2014/4

Y1 - 2014/4

N2 - The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.

AB - The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.

KW - EWI-24980

KW - GROOVE

KW - Graph Transformation

KW - IR-91953

KW - Consensus Protocols

KW - Model Checking

KW - METIS-305983

KW - SPIN

U2 - 10.4204/EPTCS.159.5

DO - 10.4204/EPTCS.159.5

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 44

EP - 57

BT - Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)

A2 - Bošnački, Dragan

A2 - Edelkamp, Stefan

A2 - Lluch Lafuente, Alberto

A2 - Wijs, Anton

PB - EPTCS

T2 - 3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014

Y2 - 5 April 2014 through 5 April 2014

ER -