TTCN-3 Bibliography

WIKINDX Resources

K. Mladenov, "Formal veri cation 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
Categories: General
Keywords: conformance, IoT, MQTT, Titan, TLA+, TTCN-3
Creators: Mladenov
Publisher: University of Amsterdam (Amsterdam)
Views: 12/510
Views index: %
Popularity index: 3.25%
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 de ne di erent
tests, based on the normative requirements in the standard. Executing those tests showed discrepancies
between the de nition of the protocol and the three di erent open source implementations
that were selected for veri cation. As a side e ect, the option to ngerprint those implementations
based on the selected tests is also discussed.
wikindx 5.2.1 ©2017 | Total resources: 339 | Username: -- | Bibliography: WIKINDX Master Bibliography | Style: Institute of Electrical and Electronics Engineers (IEEE) | Database queries: 48 | DB execution: 0.02461 secs | Script execution: 0.04338 secs