Industrial deployment of system engineering methods providing high dependability and productivity


Developing a Consensus Algorithm using Stepwise Refinement

Bryans, Jeremy W. (2010) Developing a Consensus Algorithm using Stepwise Refinement. Newcastle University. (Unpublished)

PDF (Technical Report)


We give a formal development and proof of a known consensus algorithm using stepwise refinement. We begin with an abstract specification of the intended result of the algorithm. The algorithm is developed and proved correct over a number of refinement steps. The proof of correctness is performed concurrently with the development. The development and proof make use of key fault and failure assumptions. The stepwise refinement approach allows us to introduce and prove each property at the most appropriate stage in the development, before detail irrelevant to that property has been added to the model. Finally we introduce an abstract model of a possible network on which the algorithm could be executed.

Item Type:Other
Uncontrolled Keywords: Consensus Algorithms, Stepwise Refinement, Verification
Subjects:Methodology > Refinement
Event-B > Event-B Examples
Event-B > Event-B Theory
ID Code:285
Deposited By:Dr Jeremy Bryans
Deposited On:16 Feb 2011 14:27
Last Modified:18 Feb 2011 15:29

Repository Staff Only: item control page

Deploy-Project - All right reserved