Formal Specification and Verification of MQTT Protocol in PlusCal-2

被引：7

作者：

Akhtar, Sabina ^{[1
]}

Zahoor, Ehtesham ^{[1
]}

机构：

[1] Natl Univ Comp & Emerging Sci, Secure Networks & Distributed Syst Lab SENDS, 3 AK Brohi Rd,H-11-4, Islamabad, Pakistan

来源：

WIRELESS PERSONAL COMMUNICATIONS | 2021年 / 119卷 / 02期

关键词：

IoT; MQTT protocol; Formal verification; TLA plus; PlusCal-2; tlc;

D O I：

10.1007/s11277-021-08296-4

中图分类号：

TN [电子技术、通信技术];

学科分类号：

0809 ;

摘要：

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.

引用

页码：1589 / 1606

页数：18

共 24 条

[11] Towards Formal Methods of IoT Application Layer Protocols [J].

Hofer-Schmitz, Katharina ;

Stojanovic, Branka .

2019 12TH CMI CONFERENCE ON CYBERSECURITY AND PRIVACY (CMI), 2019, :20-25

[12]

Karagiannis V., 2015, Transaction on IoT and Cloud Computing, V3, P11, DOI [DOI 10.5281/ZEN0D0.51613, DOI 10.5281/ZENODO.51613]

[13]

Kovatsch M., 2013, Proceedings of the 2013 ACM conference on, P1495, DOI [DOI 10.1145/2494091.2497583, DOI 10.1145/2494091]

[14]

Lamport L., 2002, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

[15] How Amazon Web Services Uses Formal Methods [J].

Newcombe, Chris ;

Rath, Tim ;

Zhang, Fan ;

Munteanu, Bogdan ;

Brooker, Marc ;

Deardeuff, Michael .

COMMUNICATIONS OF THE ACM, 2015, 58 (04) :66-73

[16]

Newcombe Chris., 2013, Use of formal methods at amazon web services

[17]

Perrin O., 2017, COLLABRATECOM 2017, P1

[18]

Rodriguez L. G. Araujo, 2020, P ACM ISSTA, P582

[19]

Saint-Andre Peter., XMPP DEFINITIVE GUID

[20]

Tanabe Y., 2020, KnowledgeBased Software Engineering: 2020, P47

← 1 2 3 →