Developing a consensus algorithm using stepwise refinement

    Research output: Chapter in Book/Report/Conference proceedingConference proceeding

    3 Citations (Scopus)

    Abstract

    Consensus problems arise in any area of computing where distributed processes must come to a joint decision. Although solutions to consensus problems have similar aims, they vary according to the processor faults and network properties that must be taken into account, and modifying these assumptions will lead to different algorithms. Reasoning about consensus protocols is subtle, and correctness proofs are often informal. This paper gives a fully formal development and proof of a known consensus algorithm using the stepwise refinement method Event-B. This allows us to manage the complexity of the proof process by factoring the proof of correctness into a number of refinement steps, and to carry out the proof task concurrently with the development. During the development the processor faults and network properties on which the development steps rely are identified. The research outlined here is motivated by the observation that making different choices at these points may lead to alternative algorithms and proofs, leading to a refinement tree of algorithms with partially shared proofs.
    Original languageEnglish
    Title of host publicationFormal Methods and Software Engineering
    EditorsShengchao Qin, Zongyan Qiu
    Place of PublicationBerlin
    PublisherSpringer Verlag
    Pages553-568
    Number of pages16
    Volume6991 LNCS
    ISBN (Electronic)978-3-642-24559-6
    ISBN (Print)978-3-642-24558-9
    DOIs
    Publication statusPublished - 2011

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6991

    Keywords

    • Consensus algorithms
    • Stepwise refinement
    • Verification
    • Event-B

    Fingerprint Dive into the research topics of 'Developing a consensus algorithm using stepwise refinement'. Together they form a unique fingerprint.

  • Cite this

    Bryans, J. W. (2011). Developing a consensus algorithm using stepwise refinement. In S. Qin, & Z. Qiu (Eds.), Formal Methods and Software Engineering (Vol. 6991 LNCS, pp. 553-568). (Lecture Notes in Computer Science; Vol. 6991). Berlin: Springer Verlag. https://doi.org/10.1007/978-3-642-24559-6_37