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 条
  • [21] Formal specification and verification of a coordination protocol for an automated air traffic control system
    Zhao, Yang
    Rozier, Kristin Yvonne
    SCIENCE OF COMPUTER PROGRAMMING, 2014, 96 : 337 - 353
  • [22] Synthesis and Formal Verification of On-Chip Protocol Transducers through Decomposed Specification
    Fujita, Masahiro
    Tanida, Hideo
    Gao, Fei
    Nishihara, Tasuku
    Matsumoto, Takeshi
    PROCEEDINGS OF THE ELEVENTH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN (ISQED 2010), 2010, : 515 - 523
  • [23] Formal specification and security verification of the IDKE protocol using FDR model checking
    Soltwisch, R
    Tegeler, F
    Hogrefe, D
    2005 13TH IEEE INTERNATIONAL CONFERENCE ON NETWORKS JOINTLY HELD WITH THE 2005 7TH IEEE MALAYSIA INTERNATIONAL CONFERENCE ON COMMUNICATIONS, PROCEEDINGS 1 AND 2, 2005, : 329 - 334
  • [24] Formal specification of a protocol processor
    Westerlund, T
    Plosila, J
    EMBEDDED COMPUTER SYSTEMS: ARCHITECTURES, MODELING, AND SIMULATION, 2005, 3553 : 122 - 131
  • [25] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    MICROPROCESSING AND MICROPROGRAMMING, 1988, 24 (1-5): : 371 - 378
  • [26] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    INTEGRATION-THE VLSI JOURNAL, 1989, 7 (03) : 247 - 266
  • [27] ON THE FORMAL SPECIFICATION AND VERIFICATION OF DIGITAL CIRCUITS
    DEGRAAF, PJ
    MICROPROCESSING AND MICROPROGRAMMING, 1990, 30 (1-5): : 537 - 544
  • [28] Formal Specification and Verification of Security Guidelines
    Zhioua, Zeineb
    Roudier, Yves
    Ameur, Rabea Boulifa
    2017 IEEE 22ND PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC 2017), 2017, : 267 - 273
  • [29] Formal Verification of ABAP by Z Specification
    Rodruksa, Soravit
    Pradubsuwun, Denduang
    PROCEEDINGS OF 2017 14TH INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (JCSSE), 2017,
  • [30] Formal specification and verification of hardware designs
    Ramesh, S
    Rao, SSSP
    Sivakumar, G
    Bhaduri, P
    PHOTOMASK AND X-RAY MASK TECHNOLOGY V, 1998, 3412 : 261 - 268
12345