Skip to content
Back to outputs

A formal model and analysis of an IoT protocol

Research output: Contribution to journalArticlepeer-review

Standard

A formal model and analysis of an IoT protocol. / Aziz, Benjamin Yowell Yousif.

In: Ad Hoc Networks, Vol. 36, No. 1, 01.01.2016, p. 49-57.

Research output: Contribution to journalArticlepeer-review

Harvard

APA

Vancouver

Author

Aziz, Benjamin Yowell Yousif. / A formal model and analysis of an IoT protocol. In: Ad Hoc Networks. 2016 ; Vol. 36, No. 1. pp. 49-57.

Bibtex

@article{c5e2355ff8f1484881e728c92fff0b07,
title = "A formal model and analysis of an IoT 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 modelling 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 = "Formal verification, IoT, MQTT",
author = "Aziz, {Benjamin Yowell Yousif}",
year = "2016",
month = jan,
day = "1",
doi = "10.1016/j.adhoc.2015.05.013",
language = "English",
volume = "36",
pages = "49--57",
journal = "Ad Hoc Networks",
issn = "1570-8705",
publisher = "Elsevier",
number = "1",

}

RIS

TY - JOUR

T1 - A formal model and analysis of an IoT protocol

AU - Aziz, Benjamin Yowell Yousif

PY - 2016/1/1

Y1 - 2016/1/1

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

KW - Formal verification

KW - IoT

KW - MQTT

U2 - 10.1016/j.adhoc.2015.05.013

DO - 10.1016/j.adhoc.2015.05.013

M3 - Article

VL - 36

SP - 49

EP - 57

JO - Ad Hoc Networks

JF - Ad Hoc Networks

SN - 1570-8705

IS - 1

ER -

ID: 2411405