Title :
A diversified and correct-by-construction broadcast service
Author :
Rahli, Vincent ; Schiper, Nicolas ; van Renesse, R. ; Bickford, Marck ; Constable, Robert L.
fDate :
Oct. 30 2012-Nov. 2 2012
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;
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
DOI :
10.1109/ICNP.2012.6459943
