Title :
A Formal Model and Analysis of the MQ Telemetry Transport Protocol
Author_Institution :
Sch. of Comput., Univ. of Portsmouth, Portsmouth, UK
Abstract :
We present a formal model of the MQ Telemetry Transport version 3.1 protocol based on a timed message-passing process algebra. We explain the modeling choices that we made, including pointing out ambiguities in the original protocol specification, and we carry out a static analysis of the formal protocol model, which is based on an approximation of a name-substitution semantics for algebra. The analysis reveals that the protocol behaves correctly as specified against the first two quality of service modes of operation providing at most once and at least once delivery semantics to the subscribers. However, we find that the third and highest quality of service semantics is prone to error and at best ambiguous in certain aspects of its specification. Finally, we suggest an enhancement of this level of QoS for the protocol.
Keywords :
approximation theory; formal specification; formal verification; message passing; process algebra; program diagnostics; programming language semantics; quality of service; radiotelemetry; telecommunication computing; transport protocols; MQ telemetry transport version 3.1 protocol; QoS level enhancement; embedded systems; formal protocol model; modeling choices; name-substitution semantics approximation; quality-of-service modes; static analysis; timed message-passing process algebra; Abstracts; Algebra; Approximation methods; Protocols; Quality of service; Semantics; Servers; Embedded Systems; Formal Verification; IoT; MQTT; Protocols;
Conference_Titel :
Availability, Reliability and Security (ARES), 2014 Ninth International Conference on
Conference_Location :
Fribourg
DOI :
10.1109/ARES.2014.15
