Formal Verification of Consensus in the Taurus Distributed Database

FORMAL METHODS, FM 2021(2021)

Cited 4|Views6
No score
Abstract
Distributed database services are an increasingly important part of cloud computing. They are required to satisfy several key properties, including consensus and fault tolerance. Given the highly concurrent nature of these systems, subtle errors can arise that are difficult to discover through traditional testing methods. Formal verification can help in discovering bugs and ensuring correctness of these systems. In this paper, we apply formal methods to specify and verify an industrial distributed database, Taurus, which uses a combination of several fundamental protocols, including Multi-Version Concurrency Control and Raft-based Cluster Management. TLA(+) is used to model an abstraction of the system and specify its properties. The properties are verified using the TLC model checker, as well as by theorem proving using the TLA proof system (TLAPS). We show that model checking is able to reproduce a bug in Taurus that was found during testing. But our most significant result is twofold: we successfully verified an abstract model of Taurus, and convinced our industrial partners of the usefulness of formal methods to industrial systems.
More
Translated text
Key words
Formal verification, Distributed consensus, TLA(+)
AI Read Science
Must-Reading Tree
Example
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined