Developing a Consensus Algorithm using Stepwise Refinement

  1. Lookup NU author(s)
  2. Dr Jeremy Bryans
Author(s)Bryans JW
Editor(s)Qin, S., Qiu, Z.
Publication type Conference Proceedings (inc. Abstract)
Conference Name13th International Conference on Formal Engeneering Methods
Conference LocationDurham, UK
Year of Conference2011
Legacy Date25-28 October 2011
Series TitleLecture Notes in Computer Science
Full text is available for this publication:
Consensus problems arise in any area of computing where distributedprocesses must come to a joint decision. Although solutions toconsensus problems have similar aims, they vary according to theprocessor faults and network properties that must be taken into account, and modifying theseassumptions will lead to different algorithms. Reasoning about consensusprotocols is subtle, and correctness proofs are often informal.This paper gives a fully formal development and proof of a knownconsensus algorithm using the stepwise refinement method Event-B.This allows us to manage the complexity of the proof process byfactoring 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 whichthe development steps rely are identified. The research outlined hereis motivated by the observation that making different choices at thesepoints may lead to alternative algorithms and proofs, leading to arefinement tree of algorithms with partially shared proofs.
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item