Formal Modeling and Verification of Kafka Producer-Consumer Communication in Mediator

Apache Kafka is a widely used distributed publish-subscribe messaging system, offering high throughput and low latency. It is significant to guarantee the reliability and correctness of message transmissions in Kafka via formal modeling and verification. One of Kafka’s core functions is the producer-consumer communication. In this paper, the message delivery between producers and consumers in Kafka is formally modeled and verified via Mediator, a hierarchical component-based modeling language for distributed and concurrent systems. Moreover, we translate the Mediator model into the model checker PRISM to verify its properties, such as Deadlock Freedom, Acknowledgement Mechanism, Parallelism, Sequentiality and Fault Tolerance. Results demonstrate the reliability of the producer-consumer communication in Kafka.