?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Developing+a+Consensus+Algorithm+using+Stepwise+Refinement&rft.creator=Bryans%2C+Jeremy+W.&rft.subject=Refinement&rft.subject=Event-B+Examples&rft.subject=Event-B+Theory&rft.description=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%2C+before+detail+irrelevant+to+that+property+has+been+added+to+the+model.%0D%0AFinally+we+introduce+an+abstract+model+of+a+possible+network+on+which%0D%0Athe+algorithm+could+be+executed.&rft.publisher=Newcastle+University&rft.date=2010-12&rft.type=Other&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F285%2F1%2Froot.pdf&rft.identifier=++Bryans%2C+Jeremy+W.++(2010)+Developing+a+Consensus+Algorithm+using+Stepwise+Refinement.++Newcastle+University.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F285%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>