Paper Info
Title
Specification And Verification Of The Zab Protocol With Tla
Abstract
ZooKeeper Atomic Broadcast (Zab) is an atomic broadcast protocol specially designed for ZooKeeper, which supports additional crash recovery. This protocol actually has been widely adopted by famous Internet companies, but there are few studies on the correctness and credibility of the Zab protocol, and thus we utilize formal methods to study the correctness. In this paper, Zab, Paxos and Raft are all analyzed and compared to help better understand the Zab protocol. Then we model the Zab protocol with TLA+ and verify three properties abstracted from the specification by the model checker TLC, including two liveness properties and one safety property. The final experimental results can prove that the design of the protocol conforms to the original requirements. This paper makes up for the analysis of formal methods in the Zab protocol.
Year
DOI
Venue
2020
10.1007/s11390-020-0538-7
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY
Keywords
DocType
Volume
Zab protocol, TLA plus, specification, verification
Journal
35
Issue
ISSN
Citations 
6
1000-9000
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Jiaqi Yin126.80
Huibiao Zhu258386.68
Yuan Fei311.71