Quality of Service Analysis for Internet of Things Applications with Probabilistic Model Checking

• Main Authors: Chen-Hao Chang, 張振豪
• Other Authors: Chi-Sheng Shih
• Format: Others
• Language: en_US
• Published: 2017
• Online Access: http://ndltd.ncl.edu.tw/handle/wmxuqr

碩士 === 國立臺灣大學 === 資訊工程學研究所 === 105 === In recent years, many efforts have been devoted to making it more convenient to design an Internet of Things (IoT) application. For example, Flow-Based Programming (FBP) adopted by Node-RED and Wukong abstracts the component in and data flow with boxes and arrows. While designing an IoT applications, users can treat each component as a black-box and quickly make a prototype. As there are many factors related to the qualities of the applications. it is obscure to analyze the quantitative properties in an IoT application. Our motivation is to evaluate the quantitative properties in an IoT application formally using probabilistic model checking that models an application in a mathematical model and checks its properties using formal logic such as probabilistic computation tree logic. In this work, we consider IoT applications described with FBP, and we design a tool to automatically convert the given application to a mathematical model and use a probabilistic model checker to verify whether it meets its requirements. The formats of FBP flows are regulated, so it is feasible to analyze the flow and construct the communication graph. Given the application-related and environmental parameters, we can convert the flow-based application into a mathematical model. The naive conversion generates one module for each component, making the state space grow exponentially. With our duplicate reduction technique, the duplicated components are merged, which reduces the state spaces. The experiments show that the optimization makes the state space grows linearly and the number of transitions grows quadratically as the number of duplicated components grows.