A diversified and correct-by-construction broadcast service
2012
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:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
37
References
7
Citations
NaN
KQI