TTCN-3 Bibliography

WIKINDX Resources

Mladenov, K. (2017). Formal veri cation of the implementation of the mqtt protocol in iot devices Amsterdam: University of Amsterdam. 
Added by: TET group (21/07/2017, 10:54)   Last edited by: TET group (21/07/2017, 10:59)
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)
Collection:
Views: 83/1866
Abstract
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 6.7.0 | Total resources: 347 | Username: -- | Bibliography: WIKINDX Master Bibliography | Style: American Psychological Association (APA)