@inproceedings{9487093bec084389be2dec90a997f457,
title = "The Development of a TLA+ Verified Correctness Raft Consensus Protocol",
abstract = "Distributed consensus protocols require significant effort to design, develop, and verify correctly. Traditional software quality assurance methods rely on developers creating extensive test cases to cover all code branches, which depend heavily on human experience and prolonged testing. While formal methods offer a reliable means of designing correct protocols, they ensure correctness only at the design level. Ensuring implementation correctness remains challenging once it deviates from its original design. This paper introduces our development of a verified correctness Raft protocol using an innovative specification-driven approach. We first specified Raft using TLA+ and verified its correctness with a model checker. Subsequently, we implemented the protocol based on this verified specification. Finally, we employed model checker tools to automatically generate test cases covering the entire design space for implementation verification, ensuring the implementation is an exact specification refinement. This approach ensures the correctness of both the implementation and the design.",
keywords = "Distributed System, Raft, TLA",
author = "Hua Guo and Yunhong Ji and Xuan Zhou",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2024.; 8th Asia-Pacific Web and Web-Age Information Management Joint International Conference on Web and Big Data, APWeb-WAIM 2024 ; Conference date: 30-08-2024 Through 01-09-2024",
year = "2024",
doi = "10.1007/978-981-97-7244-5\_40",
language = "英语",
isbn = "9789819772438",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "459--469",
editor = "Wenjie Zhang and Zhengyi Yang and Xiaoyang Wang and Anthony Tung and Zhonglong Zheng and Hongjie Guo",
booktitle = "Web and Big Data - 8th International Joint Conference, APWeb-WAIM 2024, Proceedings",
address = "德国",
}