Paper Info
Title
Quality of service in IoT protocol as designs and its verification in PVS
Abstract
Reliable data transmission during communication in Internet of things (IoT)-based systems has gained much interest in last few years due to the current growth and huge investment in such systems. Message Queue Telemetry Transport (MQTT) is an open publish/subscribe-based messaging protocol that is widely used for device communication in IoT. For data transmission between devices, different levels of quality of service (QoS) are used in MQTT. In this paper, we provide a formal model for MQTT protocol under the Unifying Theories of Programming (UTP) semantic framework, where QoS levels in MQTT are modeled as designs in UTP. Refinement and equivalence relations between QoS levels can be established naturally via implication between predicates. Moreover, Prototype Verification System (PVS) is used to encode the UTP design models and some important properties as well as the refinement relation between QoS levels is proved with the PVS proof assistant.
Year
DOI
Venue
2022
10.1002/ett.3742
TRANSACTIONS ON EMERGING TELECOMMUNICATIONS TECHNOLOGIES
DocType
Volume
Issue
Journal
33
8
ISSN
Citations 
PageRank 
2161-3915
0
0.34
References 
Authors
0
6
Name
Order
Citations
PageRank
Muhammad Junaid Nawaz13711.30
Meng Sun29422.65
Basit Shahzad300.68
M. Ikram Ullah Lali4245.65
Tariq Umer511615.42
Shaohua Wan6516.11