K. Mladenov, "Formal verication of the implementation of the MQTT protocol in IoT devices," University of Amsterdam, Amsterdam, July 15, 2017.
Added by: TET group (21 Jul 2017 10:54:09 Europe/Berlin) Last edited by: TET group (21 Jul 2017 10:59:19 Europe/Berlin)
|Resource type: Report/Documentation
BibTeX citation key: Mladenov2017
View all bibliographic details
Keywords: conformance, IoT, MQTT, Titan, TLA+, TTCN-3
Publisher: University of Amsterdam (Amsterdam)
Views index: %
Popularity index: 3.75%
Message Queue Telemetry Transport (MQTT) is a protocol suitable for application in Internet
of Things (IoT) devices. It is designed around requirements for low bandwidth and small code footprint.
The count of the embedded devices that make use of it is constantly increasing. Therefore,
a mistake in its implementation would be critical from both operational and security perspective.
The following research is aimed at nding a formal technique to verify whether the MQTT
implementations are adhering to the standard. After discussing several possible methods, the Test
and Test Control Notation version 3 (TTCN-3) language is selected. It is used to dene dierent
tests, based on the normative requirements in the standard. Executing those tests showed discrepancies
between the denition of the protocol and the three dierent open source implementations
that were selected for verication. As a side eect, the option to ngerprint those implementations
based on the selected tests is also discussed.