Back to Search
Start Over
Formal Specification and Verification of MQTT Protocol in PlusCal-2
- 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.
- Subjects :
- MQTT
Correctness
Computer science
business.industry
Liveness
020206 networking & telecommunications
02 engineering and technology
Computer Science Applications
PlusCal
Formal specification
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Lightweight protocol
Electrical and Electronic Engineering
business
Communications protocol
Message queue
Computer network
Subjects
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