Developing correctly replicated databases using formal tools

Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Citations (Scopus)
143 Downloads (Pure)


Fault-tolerant distributed systems often contain complex error handling code. Such code is hard to test or model-check because there are often too many possible failure scenarios to consider. As we will demonstrate in this paper, formal methods have evolved to a state in which it is possible to generate this code along with correctness guarantees.
This paper describes our experience with building highlyavailable databases using replication protocols that were generated with the help of correct-by-construction formal methods. The goal of our project is to obtain databases with unsurpassed reliability while providing good performance.
We report on our experience using a total order broadcast protocol based on Paxos and specified using a new formal language called EventML. We compile EventML specifications into a form that can be formally verified while simultaneously obtaining code that can be executed. We have developed two replicated databases based on this code and show that they have performance that is competitive with popular databases in one of the two considered benchmarks.
Original languageEnglish
Title of host publication2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages12
ISBN (Electronic)978-1-4799-2233-8
Publication statusPublished - 23 Jun 2014
Event2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Atlanta, United States
Duration: 23 Jun 201426 Jun 2014

Publication series

NameAnnual IEEE/IFIP International Conference on Dependable Systems and Networks
ISSN (Print)1530-0889
ISSN (Electronic)2158-3927


Conference2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks
Country/TerritoryUnited States


  • Fault-tolerance
  • database replication
  • correct-byconstruction distributed protocols
  • formal tools


Dive into the research topics of 'Developing correctly replicated databases using formal tools'. Together they form a unique fingerprint.

Cite this