Quantitative Analysis of Variation-Aware Internet of Things Designs Using Statistical Model Checking

Since Internet of Things (IoT) applications are deployed within open physical environments, their executions suffer from a wide spectrum of uncertain factors (e.g., network delay, sensor inputs). Although ThingML is a promising IoT modeling and specification language which enables the fast development of resource-constrained IoT applications, it lacks the capability to model such uncertainties and quantify their effects. Consequently, within uncertain environments the quality and performance of IoT applications generated from ThingML designs cannot be guaranteed. To explore the overall runtime performance variations caused by environmental uncertainties, this paper proposes a quantitative uncertainty evaluation framework for ThingML-based IoT designs. By adopting network of priced timed automata as the model of computation and statistical model checking as the evaluation engine, our approach can model uncertainties caused by external environments as well as support various kinds of performance queries on the extended ThingML designs. Experimental results of two comprehensive case studies demonstrate the efficacy of our approach.