TTCN-3 Bibliography
TTCN-3 Bibliography |
|
 |
 |
 |
|
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: 69/2618
|
| 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. |