A Formal Modeling Approach for QOS in MQTT Protocol

Abstract

With the rising demand for IoT devices, communication protocols like MQTT, CoAP, and many more, have become an integral part of the system to ensure safe and reliable data transfer. Using lightweight communication protocols such as the Message Queuing Telemetry Transport (MQTT) protocol makes it much easier to establish communication between distributed devices as it easily recovers from connectivity loss, component failures, and loss of packets. The pivotal contribution of this paper is the method of approach to formally model, analyze, and verify the Quality of Service (QoS) levels of the MQTT protocol. A complete analysis of the Quality of Service levels is performed to confirm that it behaves correctly as specified when used in communication between different components. Formal modeling has been done using PROMELA language and the model verification is done using a system verification tool called SPIN Model Checker.