Advertisement
Published in:
2022 | OriginalPaper | Chapter
4. First Case Study: The MQTT Protocol
Author : Benjamin Aziz
Published in: Formal Analysis by Abstract Interpretation
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
This chapter present a formal model of the MQ Telemetry Transport protocol based on a timed message-passing process algebra, the formal language used throughout this book. We explain the modelling choices that we made, including pointing out ambiguities in the original protocol specification, and we carry out an abstract interpretation-based static analysis of the formal protocol model, which is based on an approximation of a name-substitution semantics for algebra, as defined in earlier chapters of the book. 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. This chapter represents the first case study in this book.