We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 35 Issue 6
November  2020
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+[J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323. DOI: 10.1007/s11390-020-0538-7
Citation: Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+[J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323. DOI: 10.1007/s11390-020-0538-7
shu

Specification and Verification of the Zab Protocol with TLA+

  • 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

Funds: 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, and the Fundamental Research Funds for the Central Universities of China.
More Information
  • Author Bio:

    Jia-Qi Yin is currently a Ph.D. candidate in software engineering in Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai. His research interests contain formal methods, mobile edge computing, cloud computing and process algebra.

  • Corresponding author:

    Hui-Biao Zhu E-mail: hbzhu@sei.ecnu.edu.cn

    Yuan Fei E-mail: yuanfei@shnu.edu.cn

  • Received Date: April 10, 2020
  • Revised Date: October 08, 2020
  • Published Date: November 19, 2020
    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.
    • FullText(HTML)
    • References (23)
  • [1]
    Burrows M. The chubby lock service for loosely-coupled distributed systems. In Proc. the 7th Int. Symposium on Operating Systems Design and Implementation, November 2006, pp.335-350.
    [2]
    Junqueira F P, Reed B C. Brief announcement Zab:A practical totally ordered broadcast protocol. In Proc. the 23rd Int. Symposium on Distributed Computing, September 2009, pp.362-363.
    [3]
    Lamport L. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. AddisonWesley, 2002.
    [4]
    Junqueira F P, Reed B C, Serafini M. Zab:Highperformance broadcast for primary-backup systems. In Proc. the 41st Int. Conference on Dependable Systems and Networks, June 2011, pp.245-256.
    [5]
    Hunt P, Konar M, Junqueira F P, Reed B. ZooKeeper:Wait-free coordination for Internet-scale systems. In Proc. the 2010 USENIX Annual Technical Conference, June 2010.
    [6]
    Ongaro D, Ousterhout J K. In search of an understandable consensus algorithm. In Proc. the 2014 USENIX Annual Technical Conference, June 2014, pp.305-319.
    [7]
    Lamport L, Malkhi D, Zhou L. Vertical paxos and primarybackup replication. In Proc. the 28th Annual ACM Symposium on Principles of Distributed Computing, August 2009, pp.312-313.
    [8]
    Kuppe M A, Lamport L, Ricketts D. The TLA+ toolbox. In Proc. the 5th Workshop on Formal Integrated Development Environment, October 2019, pp.50-62.
    [9]
    Lamport L, Matthews J, Tuttle M R, Yu Y. Specifying and verifying systems with TLA+. In Proc. the 10th ACM SIGOPS European Workshop, July 2002, pp.45-48.
    [10]
    Paiva P Y A, Saotome O, Brandauer C. Specification and verification of a multi-agent coordination protocol with TLA+. In Proc. the 8th Brazilian Symposium on Computing Systems Engineering, November 2018, pp.207-212.
    [11]
    Chaudhuri K, Doligez D, Lamport L, Merz S. Verifying safety properties with the TLA+ proof system. In Proc. the 5th Int. Joint Conference on Automated Reasoning, July 2010, pp.142-148.
    [12]
    Cousineau D, Doligez D, Lamport L, Merz S, Ricketts D, Vanzetto H. TLA + proofs. In Proc. the 18th Int. Symposium on Formal Methods, August 2012, pp.147-154.
    [13]
    EL-Sanosi I, Ezhilchelvan P D. Improving the latency and throughput of ZooKeeper atomic broadcast. In Proc. the 7th Imperial College Computing Student Workshop, September 2017, Article No. 3.
    [14]
    EL-Sanosi I, Ezhilchelvan P D. Improving ZooKeeper atomic broadcast performance by coin tossing. In Proc. the 14th European Performance Engineering Workshop, September 2017, pp.249-265.
    [15]
    Batson B, Lamport L. High-level specifications:Lessons from industry. In Proc. the 1st Int. Symposium on Formal Methods for Components and Objects, November 2002, pp.242-261.
    [16]
    Newcombe C. Why Amazon chose TLA+. In Proc. the 4th Int. Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, June 2014, pp.25-39.
    [17]
    Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon web services uses formal methods. Commun. ACM, 2015, 58(4):66-73.
    [18]
    Joshi R, Lamport L, Matthews J, Tasiran S, Tuttle M R, Yu Y. Checking cache-coherence protocols with TLA+. Formal Methods Syst. Des., 2003, 22(2):125-131.
    [19]
    Lu T, Merz S, Weidenbach C. Towards verification of the pastry protocol using TLA+. In Proc. the 13th IFIP WG 6.1 International Conference and the 31st IFIP WG 6.1 Int. Conference, June 2011, pp.244-258.
    [20]
    Mokkedem A, Ferguson M J, de Johnston R. A TLA solution to the specification and verification of the RLP1 retransmission protocol. In Proc. the 4th Int. Symposium of Formal Methods Europe, September 1997, pp.398-417.
    [21]
    Regnier P, Lima G, Andrade A M S. A TLA+ formal specification and verification of a new real-time communication protocol. Electron. Notes Theor. Comput. Sci., 2009, 240:221-238.
    [22]
    Chand S, Liu Y A, Stoller S D. Formal verification of MultiPaxos for distributed consensus. In Proc. the 21st Int. Symposium on Formal Methods, November 2016, pp.119-136.
    [23]
    Gao Y, Li H, Li Y, Liu B, Wang X, Ruan H. Using TLA+ to specify leader election of Raft algorithm with consideration of leadership transfer in multiple controllers. In Proc. the 19th IEEE Int. Conference on Software Quality, Reliability and Security Companion, July 2019, pp.219-226.
    • Relative Articles

  • Related Articles

    [1]Zhao-Hui Li, Xin-Yu Feng. Verifying Contextual Refinement with Ownership Transfer[J]. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366. DOI: 10.1007/s11390-021-1671-7
    [2]Qian-Qian Lin, Shu-Ling Wang, Bo-Hua Zhan, Bin Gu. Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow[J]. Journal of Computer Science and Technology, 2020, 35(6): 1324-1342. DOI: 10.1007/s11390-020-0537-8
    [3]Dian-Xiang Xu, Omar El-Ariss, Wei-Feng Xu, Lin-Zhang Wang. Aspect-Oriented Modeling and Verification with Finite State Machines[J]. Journal of Computer Science and Technology, 2009, 24(5): 949-961.
    [4]Yu Huiqun, Sun Yongqiang. Hybridity in Embedded Computing Systems[J]. Journal of Computer Science and Technology, 1996, 11(1): 90-96.
    [5]Xu Dianxiang, Zheng Guoliang. Logical Object as a Basis of Knowledge Based Systems[J]. Journal of Computer Science and Technology, 1995, 10(5): 425-438.
    [6]Zhang Yaoxue, Shi Meilin, Norio Shiratori. A Knowledge-Based Specification Technique for Protocol Development[J]. Journal of Computer Science and Technology, 1993, 8(2): 92-96.
    [7]Liu Tong, C.S.Tang. Semantic Specification and Verification of Data Flow Diagrams[J]. Journal of Computer Science and Technology, 1991, 6(1): 21-31.
    [8]Zhao Xudong, Feng Yulin. Automatic and Hierarchical Verification for Concurrent Systems[J]. Journal of Computer Science and Technology, 1990, 5(3): 241-249.
    [9]Lu Qi, Zhang Fubo, Qian Jiahua. Program Slicing:Its Improved Algorithm and Application in Verification[J]. Journal of Computer Science and Technology, 1988, 3(1): 29-39.
    [10]Gong Zhenhe. On Conceptual Model Specification and Verification[J]. Journal of Computer Science and Technology, 1987, 2(1): 35-50.
    • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(8)

    1. M. A. Poltavtseva, A. A. Podorov, E. B. Aleksandrova. Verification of Access Control in Big Data Systems Using Temporal Logics. Automatic Control and Computer Sciences, 2024, 58(8): 1311. DOI:10.3103/S0146411624700974
    2. Maxim V. Neyzov, Egor V. Kuzmin. Using TLA+/TLC for modeling and verification of cryptographic protocols. Modeling and Analysis of Information Systems, 2024, 31(4): 446. DOI:10.18255/1818-1015-2024-4-446-473
    3. Vadym Shkarupylo, Ihor Blinov, Alexander Chemeris, et al. Iterative Approach to TLC Model Checker Application. 2021 IEEE 2nd KhPI Week on Advanced Technology (KhPIWeek), DOI:10.1109/KhPIWeek53812.2021.9570055
    4. Zhi Niu, Luming Dong, Yong Zhu, et al. Verifying Zookeeper based on Model-Based runtime Trace-Checking using TLA+. Proceedings of the 7th International Conference on Cyber Security and Information Engineering, DOI:10.1145/3558819.3558822
    5. Lingzhi Ouyang, Yu Huang, Binyu Huang, et al. Dependable Software Engineering. Theories, Tools, and Applications. Lecture Notes in Computer Science, DOI:10.1007/978-981-99-8664-4_11
    6. Lei Wang, Yufei Su, Haie Dou, et al. Offloading Model of 5G Intelligent Terminal Based on UC-MEC and Node Consensus Mechanism. 2023 International Conference on Wireless Communications and Signal Processing (WCSP), DOI:10.1109/WCSP58612.2023.10404689
    7. Wenting Dong, Jiaqi Yin, Sini Chen, et al. Parallel and Distributed Computing, Applications and Technologies. Lecture Notes in Electrical Engineering, DOI:10.1007/978-981-99-8211-0_2
    8. Qiuyang Wei, Xufeng Zhao, Xue-Yang Zhu, et al. Formal Analysis of IBC Protocol. 2023 IEEE 31st International Conference on Network Protocols (ICNP), DOI:10.1109/ICNP59255.2023.10355573

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (122) PDF downloads (0) Cited by(8)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return