---
abstract: "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.\r\nFinally we introduce an abstract model of a possible network on which\r\nthe algorithm could be executed."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - jeremy.bryans@ncl.ac.uk
creators_name:
  - family: Bryans
    given: Jeremy W.
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-12
date_type: completed
datestamp: 2011-02-16 14:27:09
department: ~
dir: disk0/00/00/02/85
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 285
event_dates: ~
event_location: ~
event_title: ~
event_type: other
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/285/1/root.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: unpub
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ' Consensus Algorithms, Stepwise Refinement, Verification'
lastmod: 2011-02-18 15:29:14
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: 1-19
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: other
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: Newcastle University
refereed: FALSE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 34
series: ~
skill_areas: []
source: ~
status_changed: 2011-02-16 14:27:09
subjects:
  - Refinement
  - examples
  - theory
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Developing a Consensus Algorithm using Stepwise Refinement
type: other
userid: 43
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>