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 条
  • [41] METAGRAMMARS AS A MEANS OF FORMAL PROTOCOL SPECIFICATION
    ATAKISHCHEV, OI
    KOZIN, YD
    AVTOMATIKA I VYCHISLITELNAYA TEKHNIKA, 1989, (05): : 11 - 16
  • [42] Formal Specification of Memory Coherence Protocol
    Khan, Jahanzaib
    Atif, Muhammad
    Bajwa, Muhammad Khurram Zahoor
    Mahmood, Muhammad Sohaib
    Usman, Sobia
    INTERNATIONAL JOURNAL OF ADVANCED COMPUTER SCIENCE AND APPLICATIONS, 2018, 9 (08) : 641 - 650
  • [43] AN INFORMAL OVERVIEW OF FORMAL PROTOCOL SPECIFICATION
    RUDIN, H
    IEEE COMMUNICATIONS MAGAZINE, 1985, 23 (03) : 46 - 52
  • [44] An executable specification of a formal argumentation protocol
    Artikis, Alexander
    Sergot, Marek
    Pitt, Jeremy
    ARTIFICIAL INTELLIGENCE, 2007, 171 (10-15) : 776 - 804
  • [45] Formal Verification of the Sumcheck Protocol
    Bosshard, Azucena Garvia
    Bootle, Jonathan
    Sprenger, Christoph
    2024 IEEE 37TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, CSF 2024, 2024, : 605 - 619
  • [46] Formal Verification of the FDO Protocol
    Bussa, Simone
    Sisto, Riccardo
    Valenza, Fulvio
    2023 IEEE CONFERENCE ON STANDARDS FOR COMMUNICATIONS AND NETWORKING, CSCN, 2023, : 290 - 295
  • [47] Formal verification for a PMQTT protocol
    Elemam, Eman
    Bahaa-Eldin, Ayman M.
    Shaker, Nabil H.
    Sobh, Mohamed
    EGYPTIAN INFORMATICS JOURNAL, 2020, 21 (03) : 169 - 182
  • [48] Formal Verification of the xDAuth Protocol
    Alam, Quratulain
    Tabbasum, Saher
    Malik, Saif U. R.
    Alam, Masoom
    Ali, Tamleek
    Akhunzada, Adnan
    Khan, Samee U.
    Vasilakos, Athanasios V.
    Buyya, Rajkumar
    IEEE TRANSACTIONS ON INFORMATION FORENSICS AND SECURITY, 2016, 11 (09) : 1956 - 1969
  • [49] A Survey of Smart Contract Formal Specification and Verification
    Tolmach, Palina
    Li, Yi
    Lin, Shang-Wei
    Liu, Yang
    Li, Zengxiang
    ACM COMPUTING SURVEYS, 2021, 54 (07)
  • [50] A formal specification for web services composition and verification
    Shi, YL
    Zhang, L
    Liu, B
    Liu, FF
    Lin, LL
    Shi, BL
    Fifth International Conference on Computer and Information Technology - Proceedings, 2005, : 252 - 256
12345