Graph- versus Vector-Based Analysis of a Consensus Protocol

Giorgio Delzanno, Arend Rensink, Riccardo Traverso

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    83 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 languageUndefined
    Title of host publicationProceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)
    EditorsDragan Bošnački, Stefan Edelkamp, Alberto Lluch Lafuente, Anton Wijs
    PublisherEPTCS
    Pages44-57
    Number of pages14
    DOIs
    Publication statusPublished - Apr 2014
    Event3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014 - Grenoble, France
    Duration: 5 Apr 20145 Apr 2014

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science
    PublisherEPTCS
    Volume159
    ISSN (Print)2075-2180
    ISSN (Electronic)2075-2180

    Workshop

    Workshop3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014
    Period5/04/145/04/14
    Other5 April 2014

    Keywords

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

    Cite this