Skip to content
Back to outputs

A formal model and analysis of the MQ telemetry transport protocol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Standard

A formal model and analysis of the MQ telemetry transport protocol. / Aziz, Benjamin.

2014 Ninth International Conference on Availabilty, Reliability and Security (ARES). IEEE, 2014. p. 59-68.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Harvard

Aziz, B 2014, A formal model and analysis of the MQ telemetry transport protocol. in 2014 Ninth International Conference on Availabilty, Reliability and Security (ARES). IEEE, pp. 59-68, The 9th International Conference on Availability, Reliability and Security (ARES 2014), Fribourg, Switzerland, 8/09/14. https://doi.org/10.1109/ARES.2014.15

APA

Aziz, B. (2014). A formal model and analysis of the MQ telemetry transport protocol. In 2014 Ninth International Conference on Availabilty, Reliability and Security (ARES) (pp. 59-68). IEEE. https://doi.org/10.1109/ARES.2014.15

Vancouver

Aziz B. A formal model and analysis of the MQ telemetry transport protocol. In 2014 Ninth International Conference on Availabilty, Reliability and Security (ARES). IEEE. 2014. p. 59-68 https://doi.org/10.1109/ARES.2014.15

Author

Aziz, Benjamin. / A formal model and analysis of the MQ telemetry transport protocol. 2014 Ninth International Conference on Availabilty, Reliability and Security (ARES). IEEE, 2014. pp. 59-68

Bibtex

@inproceedings{48af25b18bae4b03a65f3949f2e4c715,
title = "A formal model and analysis of the MQ telemetry transport protocol",
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.",
author = "Benjamin Aziz",
year = "2014",
month = sep,
doi = "10.1109/ARES.2014.15",
language = "English",
isbn = "978-1479942237",
pages = "59--68",
booktitle = "2014 Ninth International Conference on Availabilty, Reliability and Security (ARES)",
publisher = "IEEE",
note = "The 9th International Conference on Availability, Reliability and Security (ARES 2014) ; Conference date: 08-09-2014 Through 12-09-2014",

}

RIS

TY - GEN

T1 - A formal model and analysis of the MQ telemetry transport protocol

AU - Aziz, Benjamin

PY - 2014/9

Y1 - 2014/9

N2 - 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.

AB - 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.

U2 - 10.1109/ARES.2014.15

DO - 10.1109/ARES.2014.15

M3 - Conference contribution

SN - 978-1479942237

SP - 59

EP - 68

BT - 2014 Ninth International Conference on Availabilty, Reliability and Security (ARES)

PB - IEEE

T2 - The 9th International Conference on Availability, Reliability and Security (ARES 2014)

Y2 - 8 September 2014 through 12 September 2014

ER -

ID: 3621284