Developing a Consensus Algorithm using Stepwise Refinement
- Lookup NU author(s)
- Dr Jeremy Bryans
|
|
|
|
| Author(s) | | Bryans JW |
| Editor(s) | | Qin, S., Qiu, Z. |
| Publication type | | Conference Proceedings (inc. Abstract) |
| Conference Name | | 13th International Conference on Formal Engeneering Methods |
| Conference Location | | Durham, UK |
| Year of Conference | | 2011 |
| Date | | 25-28 October 2011 |
| Volume | | 6991 |
| Pages | | 553-568 |
| Series Title | | Lecture Notes in Computer Science |
| ISBN | | 9783642245589 |
| |  |
|
|
|
| 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. |
|
|
|
| Publisher | | Springer |
| URL | | http://dx.doi.org/10.1007/978-3-642-24559-6_37 |
| DOI | | 10.1007/978-3-642-24559-6_37 |
| Actions | |  |
| Library holdings | | Search Newcastle University Library for this item |
