--- abstract: "\r\nConsensus problems arise in any area of computing where distributed\r\nprocesses must come to a joint decision. Although solutions to\r\nconsensus problems have similar aims, they vary according to the\r\nprocessor faults and network \r\nproperties that must be taken into account, and modifying these\r\nassumptions will lead to different algorithms. \r\nReasoning about consensus\r\nprotocols is subtle, and correctness proofs are often informal.\r\nThis paper gives a fully formal development and proof of a known\r\nconsensus algorithm using the stepwise refinement method Event-B.\r\nThis allows us to manage the complexity of the proof process by\r\nfactoring the proof of correctness into a number of refinement steps,\r\nand to carry out the proof task concurrently with the development.\r\nDuring the development the processor faults and network properties on which\r\nthe development steps rely are identified. The research outlined here\r\nis motivated by the observation that making different choices at these\r\npoints may lead to alternative algorithms and proofs, leading to a\r\nrefinement tree of algorithms with partially shared proofs." 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: 2011-10 date_type: ~ datestamp: 2012-01-23 13:10:15 department: ~ dir: disk0/00/00/03/63 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 363 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: application/pdf;http://deploy-eprints.ecs.soton.ac.uk/363/1/icfem.pdf|application/pdf;http://deploy-eprints.ecs.soton.ac.uk/363/2/icfem.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: ~ item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2012-01-23 13:10:15 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: 6991 official_url: http://dl.acm.org/citation.cfm?id=2075089.2075136 output_media: ~ pagerange: 553-568 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: - DEPLOY publication: Proceedings of the 13th international conference on Formal methods and software engineering publisher: Springer-Verlag refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 8 series: ~ skill_areas: [] source: ~ status_changed: 2012-01-23 13:10:15 subjects: - Refinement - examples succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Developing a Consensus Algorithm Using Stepwise Refinement type: article userid: 43 volume: LNCS