KnowledgeBase » PUBLICATION » ID = 746

Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
2015

• In Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Edinburgh, UK, September 1, 2015.
• Unofficial PDF

Abstract
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 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.