Developing a Consensus Algorithm using Stepwise Refinement

Bryans, , JW

doi:10.1007/978-3-642-24559-6_37

Developing a Consensus Algorithm using Stepwise Refinement

Lookup NU author(s): Dr Jeremy Bryans

Downloads

Accepted version [.pdf]

Abstract

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.