<p>With the rising demandArchana, E. for IoT devices, communication protocols like MQTT, CoAP, and many more, haveRajeev, Akshay become an integral part of the system to ensureKuruvila, Aby safe and reliable data transfer. Using lightweight communication protocols such as the Message QueuingNarayankutty, Revathi Telemetry Transport (MQTT) protocol makes it much easier to establish communication between distributed devicesKannimoola, Jinesh M. 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.</p>
E. Archana, Rajeev, A., Kuruvila, A., Narayankutty, R., and M. K. Jinesh, “A Formal Modeling Approach for QOS in MQTT Protocol”, Data Communication and Networks. Springer Singapore, Singapore, pp. 39-57, 2020.