| Abstract [eng] |
The purpose of this thesis is to overview the statistical model checking (SMC) theory, the Uppaal tool and use them to analyze the identified properties of the chosen IoT system. Moreover, we discuss what is required to perform SMC to an Internet of Things (IoT) system model. The room temperature control system was chosen for analysis. In the practical work part the IoT system model, which was verified using classical model checking, was changed so that the requirements for SMC verification would be satisfied. The obtained verification results have showed that the system effectively and predictably behaves reaching its required goals. Effectiveness might be affected by the device fault probability weight, temperature sensor count, repair time length. Overall, the analysis and verification showed that the analyzed system is stable, deadlock-free, functionally correct, reaches the target temperature, fault tolerant. |
