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 条
  • [31] FORMAL TECHNIQUES FOR SYSTEMS SPECIFICATION AND VERIFICATION
    CARMO, J
    SERNADAS, A
    INFORMATION SYSTEMS, 1991, 16 (03) : 245 - 272
  • [32] FORMAL SPECIFICATION AND VERIFICATION OF DISTRIBUTED SYSTEMS
    CHEN, BS
    YEH, RT
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1983, 9 (06) : 710 - 722
  • [33] Formal specification in VHDL for hardware verification
    Reetz, R
    Schneider, K
    Kropf, T
    DESIGN, AUTOMATION AND TEST IN EUROPE, PROCEEDINGS, 1998, : 257 - 263
  • [34] PROTOCOL SPECIFICATION, TESTING AND VERIFICATION
    不详
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1984, 8 (01): : 57 - 65
  • [35] PROTOCOL SPECIFICATION, TESTING AND VERIFICATION
    不详
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1984, 8 (02): : 146 - 155
  • [36] PROTOCOL SPECIFICATION, TESTING AND VERIFICATION
    不详
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1985, 10 (3-4): : 231 - 237
  • [37] A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol
    Regnier, Paul
    Lima, George
    Andrade, Aline
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 221 - 238
  • [38] Formal Specification and Verification of a Protocol for Consistent Diagnosis in Real-Time Embedded Systems
    Barbosa, Raul
    Karlsson, Johan
    2008 INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS, 2008, : 192 - 199
  • [39] Formal specification of a Web services protocol
    Johnson, James E.
    Langworthy, David E.
    Lamport, Leslie
    Vogt, Friedrich H.
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2007, 70 (01): : 34 - 52
  • [40] Formal Specification of a Team Formation Protocol
    Niyogi, Rajdeep
    ADVANCED INFORMATION NETWORKING AND APPLICATIONS, AINA-2022, VOL 3, 2022, 451 : 301 - 313
12345