@inproceedings{ca7a648d4f064d2c854571c61d5007eb,
title = "Formalization and Verification of the Zab Protocol Using CSP",
abstract = "ZooKeeper Atomic Broadcast (Zab) is a high-performance atomic broadcast protocol, which is a key component of Apache ZooKeeper. By ensuring strong consistency and fault tolerance, the Zab protocol plays a crucial role in building robust and resilient distributed systems. However, the correctness and reliability of the Zab protocol have received limited attention in research. Thus, we employ Communicating Sequential Processes (CSP) to analyze and evaluate of the Zab protocol{\textquoteright}s properties and behavior. We utilize Process Analysis Toolkit (PAT) to verify six important properties, including Deadlock Freedom, Divergence Freedom, Data Reachability, Consistency, Sequentiality and Atomicity. The verification results demonstrate that the Zab protocol provides assurance of correctness and reliability.",
keywords = "CSP, Modeling, PAT, Verification, Zab protocol",
author = "Wenting Dong and Jiaqi Yin and Sini Chen and Huibiao Zhu",
note = "Publisher Copyright: {\textcopyright} 2024, The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.; 24th International Conference on Parallel and Distributed Computing, Applications and Technologies, PDCAT 2023 ; Conference date: 16-08-2023 Through 18-08-2023",
year = "2024",
doi = "10.1007/978-981-99-8211-0\_2",
language = "英语",
isbn = "9789819982103",
series = "Lecture Notes in Electrical Engineering",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "12--24",
editor = "Park, \{Ji Su\} and Hiroyuki Takizawa and Hong Shen and Park, \{James J.\}",
booktitle = "Parallel and Distributed Computing, Applications and Technologies - Proceedings of PDCAT 2023",
address = "德国",
}