Developing correctly replicated databases using formal tools

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

doi:10.1109/DSN.2014.45

Developing correctly replicated databases using formal tools

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

23 Citations (Scopus)

143 Downloads (Pure)

Abstract

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 language	English
Title of host publication	2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings)
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	395-406
Number of pages	12
ISBN (Electronic)	978-1-4799-2233-8
DOIs	https://doi.org/10.1109/DSN.2014.45
Publication status	Published - 23 Jun 2014
Event	2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Atlanta, United States Duration: 23 Jun 2014 → 26 Jun 2014

Publication series

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

Conference

Conference	2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks
Country/Territory	United States
City	Atlanta
Period	23/06/14 → 26/06/14

Keywords

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

Access to Document

10.1109/DSN.2014.45Licence: None: All rights reserved

Schiper_et_al_Developing_Correctly_Replicated_Databases_Using_Formal_Tools_44th_Annual_IEEE/IFIP_International_Conference_on_Dependable_Systems_and_Networks_2014
© 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. N. Schiper, V. Rahli, R. V. Renesse, M. Bickford and R. L. Constable, "Developing Correctly Replicated Databases Using Formal Tools," 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, Atlanta, GA, 2014, pp. 395-406. doi: 10.1109/DSN.2014.45
Accepted author manuscript, 307 KBLicence: None: All rights reserved

https://ieeexplore.ieee.org/document/6903597?arnumber=6903597&tag=1Licence: None: All rights reserved

Cite this

Schiper, N., Rahli, V., Renesse, R. V., Bickford, M., & Constable, R. L. (2014). Developing correctly replicated databases using formal tools. In 2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings) (pp. 395-406). (Annual IEEE/IFIP International Conference on Dependable Systems and Networks). Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/DSN.2014.45

Schiper, Nicolas ; Rahli, Vincent ; Renesse, Robbert van et al. / Developing correctly replicated databases using formal tools. 2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings) . Institute of Electrical and Electronics Engineers (IEEE), 2014. pp. 395-406 (Annual IEEE/IFIP International Conference on Dependable Systems and Networks).

@inproceedings{97df8c5cabee4852b424c24eb658e742,

title = "Developing correctly replicated databases using formal tools",

abstract = "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.",

keywords = "Fault-tolerance, database replication, correct-byconstruction distributed protocols, formal tools",

author = "Nicolas Schiper and Vincent Rahli and Renesse, {Robbert van} and Mark Bickford and Constable, {Robert L.}",

year = "2014",

month = jun,

day = "23",

doi = "10.1109/DSN.2014.45",

language = "English",

series = "Annual IEEE/IFIP International Conference on Dependable Systems and Networks",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "395--406",

booktitle = "2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings)",

note = "2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks ; Conference date: 23-06-2014 Through 26-06-2014",

}

Schiper, N, Rahli, V, Renesse, RV, Bickford, M & Constable, RL 2014, Developing correctly replicated databases using formal tools. in 2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings) . Annual IEEE/IFIP International Conference on Dependable Systems and Networks, Institute of Electrical and Electronics Engineers (IEEE), pp. 395-406, 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, Atlanta, Georgia, United States, 23/06/14. https://doi.org/10.1109/DSN.2014.45

Developing correctly replicated databases using formal tools. / Schiper, Nicolas; Rahli, Vincent; Renesse, Robbert van et al.

2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings) . Institute of Electrical and Electronics Engineers (IEEE), 2014. p. 395-406 (Annual IEEE/IFIP International Conference on Dependable Systems and Networks).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Developing correctly replicated databases using formal tools

AU - Schiper, Nicolas

AU - Rahli, Vincent

AU - Renesse, Robbert van

AU - Bickford, Mark

AU - Constable, Robert L.

PY - 2014/6/23

Y1 - 2014/6/23

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

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

KW - Fault-tolerance

KW - database replication

KW - correct-byconstruction distributed protocols

KW - formal tools

U2 - 10.1109/DSN.2014.45

DO - 10.1109/DSN.2014.45

M3 - Conference contribution

T3 - Annual IEEE/IFIP International Conference on Dependable Systems and Networks

SP - 395

EP - 406

BT - 2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings)

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks

Y2 - 23 June 2014 through 26 June 2014

ER -

Schiper N, Rahli V, Renesse RV, Bickford M, Constable RL. Developing correctly replicated databases using formal tools. In 2014 44th Annual IEEE/IFIP international conference on dependable systems and networks (proceedings) . Institute of Electrical and Electronics Engineers (IEEE). 2014. p. 395-406. (Annual IEEE/IFIP International Conference on Dependable Systems and Networks). doi: 10.1109/DSN.2014.45

Developing correctly replicated databases using formal tools

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this