Specification and Verification of the Zab Protocol with TLA+  

作　　者：Jia-Qi Yin Hui-Biao Zhu Yuan Fei 

机构地区：[1]Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China [2]College of Information,Mechanical and Electrical Engineering,Shanghai Normal University,Shanghai 200234,China

出　　处：《Journal of Computer Science & Technology》2020年第6期1312-1323,共12页计算机科学技术学报（英文版）

基　　金：This work was partly supported by the National Key Research and Development Program of China under Grant No.2018YFB2101300;the National Natural Science Foundation of China under Grant No.61872145;Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things under Grant No.ZF1213;the Fundamental Research Funds for the Central Universities of China.

摘　　要：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.

关 键 词：Zab protocol TLA+ SPECIFICATION VERIFICATION 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]