Quality of service in IoT protocol as designs and its verification in PVS
TRANSACTIONS ON EMERGING TELECOMMUNICATIONS TECHNOLOGIES(2022)
摘要
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.
更多查看译文
关键词
iot protocol,pvs,quality,verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要