DocumentCode
3310491
Title
A diversified and correct-by-construction broadcast service
Author
Rahli, Vincent ; Schiper, Nicolas ; van Renesse, R. ; Bickford, Marck ; Constable, Robert L.
fYear
2012
fDate
Oct. 30 2012-Nov. 2 2012
Firstpage
1
Lastpage
6
Abstract
We present a fault-tolerant ordered broadcast service that is correct-by-construction. Our broadcast service allows for diversity in space, whereby the participants in the broadcast protocol run different code, as well as in time, whereby the protocol itself is changed periodically. We use the Nuprl proof assistant to specify the service, prove correctness, and synthesize the code. The paper includes initial performance results.
Keywords
broadcasting; fault tolerance; formal specification; formal verification; protocols; telecommunication computing; Nuprl proof assistant; broadcast protocol; code synthesis; correct-by-construction broadcast service; correctness proof; fault-tolerant ordered broadcast service; Computer crashes; Fault tolerance; Fault tolerant systems; Proposals; Protocols; Reactive power; Switches;
fLanguage
English
Publisher
ieee
Conference_Titel
Network Protocols (ICNP), 2012 20th IEEE International Conference on
Conference_Location
Austin, TX
Print_ISBN
978-1-4673-2445-8
Electronic_ISBN
978-1-4673-2446-5
Type
conf
DOI
10.1109/ICNP.2012.6459943
Filename
6459943
Link To Document