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

共 50 条

[1] Formal Specification and Verification of MQTT Protocol in PlusCal-2
Sabina Akhtar
Ehtesham Zahoor
Wireless Personal Communications, 2021, 119 : 1589 - 1606
[2] Formal Verification of Authorization Policies for Enterprise Social Networks Using PlusCal-2
Akhtar, Sabina
Zahoor, Ehtesham
Perrin, Olivier
COLLABORATIVE COMPUTING: NETWORKING, APPLICATIONS AND WORKSHARING, COLLABORATECOM 2017, 2018, 252 : 530 - 540
[3] Formal Specification, Verification and Evaluation of the MQTT Protocol in the Internet of Things
Houimli, Manel
Kahloul, Laid
Benaoun, Sihem
PROCEEDINGS OF THE 2017 INTERNATIONAL CONFERENCE ON MATHEMATICS AND INFORMATION TECHNOLOGY (ICMIT), 2017, : 214 - 221
[4] Formal specification and verification of a micropayment protocol
Gouda, MG
Liu, AX
ICCCN 2004: 13TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 2004, : 489 - 494
[5] FORMAL TECHNIQUES FOR PROTOCOL SPECIFICATION AND VERIFICATION
SUNSHINE, C
COMPUTER, 1979, 12 (09) : 20 - 27
[6] Formal Specification and Verification of Transmission Control Protocol
Jarrar, Abdessamad
Bellasri, Otman
Chougdali, Sallami
Balouki, Youssef
ICCWCS'17: PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTING AND WIRELESS COMMUNICATION SYSTEMS, 2017,
[7] Formal hardware specification languages for protocol compliance verification
Bunker, A
Gopalakrishnan, G
Mckee, SA
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2004, 9 (01) : 1 - 32
[8] Formal specification and verification of the SET/A protocol with an integrated approach
Lam, VSW
Padget, J
CEC 2004: IEEE INTERNATIONAL CONFERENCE ON E-COMMERCE TECHNOLOGY, PROCEEDINGS, 2004, : 229 - 235
[9] FORMAL SPECIFICATION AND COMPOSITIONAL VERIFICATION OF AN ATOMIC BROADCAST PROTOCOL
ZHOU, P
HOOMAN, J
REAL-TIME SYSTEMS, 1995, 9 (02) : 119 - 145
[10] Formal Specification and Verification of JXTA's Endpoint Routing Protocol
Konga, Yannick L. Kala
Djouani, Karim
IEEE AFRICON 2011, 2011,

← 1 2 3 4 5 →