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

    70 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

    Publication series

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

    Keywords

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

    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