TY - JOUR
T1 - EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems
AU - Rahli, Vincent
AU - Guaspari, David
AU - Bickford, Mark
AU - Constable, Robert L.
PY - 2017/11/15
Y1 - 2017/11/15
N2 - Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal language that is intuitively clear to the programmers. We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system. This article focuses on the logical foundations as well as the basic ideas of formal EventML programming, illustrated by implementing a fault-tolerant consensus protocol and showing how we prove its safety properties with the Nuprl proof assistant.
AB - Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal language that is intuitively clear to the programmers. We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system. This article focuses on the logical foundations as well as the basic ideas of formal EventML programming, illustrated by implementing a fault-tolerant consensus protocol and showing how we prove its safety properties with the Nuprl proof assistant.
U2 - 10.1016/j.scico.2017.05.009
DO - 10.1016/j.scico.2017.05.009
M3 - Article
SN - 0167-6423
VL - 148
SP - 26
EP - 48
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -