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

Vincent Rahli; David Guaspari; Mark Bickford; Robert L. Constable

doi:10.14279/tuj.eceasst.72.1013

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

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

Computer Science

Research output: Contribution to journal › Article › peer-review

11 Citations (Scopus)

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.

Original language	English
Number of pages	15
Journal	Electronic Communications of the EASST
Volume	72
DOIs	https://doi.org/10.14279/tuj.eceasst.72.1013
Publication status	Published - 2015
Event	15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015) - Edinburgh, United Kingdom Duration: 1 Sept 2015 → 4 Sept 2015

Keywords

functional programming
formal methods
formal verification
theorem proving
distributed systems
fault tolerance
event logic
event-based programming

Access to Document

10.14279/tuj.eceasst.72.1013

https://doi.org/10.14279/tuj.eceasst.72.1013

Cite this

@article{050cfa24074f4b7aa45a8a2421a9c8da,

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

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

keywords = "functional programming, formal methods, formal verification, theorem proving, distributed systems, fault tolerance, event logic, event-based programming",

author = "Vincent Rahli and David Guaspari and Mark Bickford and Constable, {Robert L.}",

year = "2015",

doi = "10.14279/tuj.eceasst.72.1013",

language = "English",

volume = "72",

journal = "Electronic Communications of the EASST",

issn = "1863-2122",

publisher = "European Association of Software Science and Technology",

note = "15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015) ; Conference date: 01-09-2015 Through 04-09-2015",

}

TY - JOUR

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

AU - Rahli, Vincent

AU - Guaspari, David

AU - Bickford, Mark

AU - Constable, Robert L.

PY - 2015

Y1 - 2015

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

KW - functional programming

KW - formal methods

KW - formal verification

KW - theorem proving

KW - distributed systems

KW - fault tolerance

KW - event logic

KW - event-based programming

U2 - 10.14279/tuj.eceasst.72.1013

DO - 10.14279/tuj.eceasst.72.1013

M3 - Article

SN - 1863-2122

VL - 72

JO - Electronic Communications of the EASST

JF - Electronic Communications of the EASST

T2 - 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015)

Y2 - 1 September 2015 through 4 September 2015

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this