Skip to content

A formal model and analysis of the MQ telemetry transport protocol

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publication2014 Ninth International Conference on Availabilty, Reliability and Security (ARES)
PublisherIEEE
Pages59-68
ISBN (Print)978-1479942237
DOIs
Publication statusPublished - Sep 2014
EventThe 9th International Conference on Availability, Reliability and Security (ARES 2014) - Fribourg, Switzerland
Duration: 8 Sep 201412 Sep 2014

Conference

ConferenceThe 9th International Conference on Availability, Reliability and Security (ARES 2014)
CountrySwitzerland
CityFribourg
Period8/09/1412/09/14

Documents

  • bare_conf

    Accepted author manuscript (Post-print), 333 KB, PDF document

Related information

Relations Get citation (various referencing formats)

ID: 3621284