Formal-Modeling-and-Verification-of-MQTT-Using-UPPAAL

Methodology and Experimental Artifacts We propose a methodological framework for analyzing the performance and security properties of the MQTT protocol using the UPPAAL-SMC statistical model checker. First, the core components of the protocol — Publisher, Subscriber, and Broker — were modeled as timed automata to capture their interactions and timing behavior. Second, we extended the model with an additional automaton representing a universal attacker capable of simulating various malicious actions without being restricted to a specific predefined attack scenario. Third, we formalized a set of 32 verification formulas, including generic liveness, safety, and deadlock properties. These formulas were verified under two conditions: with and without the presence of the attacker, enabling a comparative analysis of system behavior and verification complexity. Finally, we evaluated the impact of different UPPAAL-SMC configurations on verification performance by varying diagnostic trace generation (-t option) and state-space exploration strategies (-o option). The experimental results show that all liveness properties remain satisfied in both scenarios, ensuring that MQTT maintains system progress and message delivery even under adversarial conditions. However, safety properties are not always satisfied, indicating that certain intermediate states may violate expected operational constraints. The deadlock property could not be conclusively verified within the computational limits, mainly due to the high complexity of the state space generated by the interaction between protocol automata, timing mechanisms, and the attacker model. Reproducibility and File Description To reproduce the experiments, the UPPAAL-SMC tool must be installed. The provided XML models can be loaded into the UPPAAL graphical interface to visualize the automata and execute the verification queries. They can also be analyzed via the command line using the verifyta executable. This repository contains the following files: Model Files (.xml) EWSN.xml – Official modified MQTT model used to test specific protocol properties. with attacker.xml – MQTT model including the universal attacker and the set of generic verification formulas. without attacker.xml – Same model and formulas but without the attacker, used for comparison. These files allow full reproduction of the verification scenarios described in the paper. Data Files (.xlsx) The Excel files contain the raw numerical results produced during statistical model checking. For each formula and configuration, they report: CPU user time Virtual and resident memory usage Number of stored states Number of explored states These datasets were used to generate the performance curves presented in the article. LaTeX Figure Files (.tex) The .tex files correspond to the LaTeX source used to generate the performance curves included in the paper. Each file produces a figure illustrating the verification cost (CPU time, memory usage, and explored states) under different configurations and attacker conditions. Curve Generation The curves presented in the article were generated from the collected experimental data and visualized through LaTeX plotting scripts. They illustrate the impact of attacker presence and UPPAAL-SMC configuration parameters on verification performance across all 32 formulas.