Back to Search Start Over

Formal Specification and Verification of MQTT Protocol in PlusCal-2

Authors :
Ehtesham Zahoor
Sabina Akhtar
Source :
Wireless Personal Communications.
Publication Year :
2021
Publisher :
Springer Science and Business Media LLC, 2021.

Abstract

The recent rise in adaptation of Internet of Things (IoT) concepts has potential to transform industries such as healthcare, manufacturing and power-grids. The communication protocols are at the heart of IoT and one such lightweight protocol being in widespread use is the Message Queue Telemetry Transport (MQTT) protocol. In this paper, we address the need to verify the correctness of the MQTT protocol. We have proposed a PlusCal-2 and TLA+ based formal model to both model check the safety and liveness properties and provide execution traces in case of any violation. We have detailed our models and provided performance analysis results to explain the practicality of our technique.

Details

ISSN :
1572834X and 09296212
Database :
OpenAIRE
Journal :
Wireless Personal Communications
Accession number :
edsair.doi...........2aaa8114bbcd21bf7c056c83b36e2804
Full Text :
https://doi.org/10.1007/s11277-021-08296-4