Apache Kafka is a distributed, fault-tolerant and highly available open-source technology that utilizes a publish-subscribe communication model to stream large volumes of data. It is widely being used in various domains such as finance, entertainment, online education, and e-commerce for real-time data processing and analytics. This paper demonstrates an application of Alloy 6—the latest version of Alloy with built-in temporal logic operators—to formal modeling and analysis of a complex distributed system like Kafka. The architecture and key operations of Kakfa are modeled, and its various properties, including fault-tolerance, data availability, service availability, consistency, and recoverability, are analyzed using the Alloy Analyzer. The result of the analysis provides insights into how Kafka maintains the properties that it claims to have, and the circumstances under which these properties may be violated.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{SinhaK24,
author = {Saloni Sinha and
Eunsuk Kang},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Formal Modeling and Analysis of Apache Kafka in Alloy 6},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {25--42},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_2},
doi = {10.1007/978-3-031-63790-2\_2},
timestamp = {Thu, 27 Jun 2024 16:32:24 +0200},
biburl = {https://dblp.org/rec/conf/zum/SinhaK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}