利用機率模型檢查之物聯網應用程式服務品質分析

Abstract

近年來有許多的作品致力於降低設計物聯網應用程式的難度。 例如 Node-RED 與 Wukong 專案所採用的資料流程式設計就是將物聯網元件與資料流以抽象的方式表現。 使用者在設計物聯網應用程式時可以將元件視為黑盒子，如此便可快速的打造出應用程式的原型。 即使能夠很方便地設計出物聯網應用，但要形式化量化其服務品質仍是一個隱晦難解的問題。 我們的研究動機是利用機率模型檢查以使用形式化的將物聯網應用建構成正規的數學模型，並且利用機率模型檢查器來計算其服務品質。 在這份研究中，我們所考慮的是資料流程式設計所描述的物聯網應用。 我們設計了一套工具將給定的物聯網應用轉換成了數學模型，再利用機率模型檢查器來計算其量化性質，確保其服務品質符合原先規範。 由於資料流程式所規範的格式是個樹狀結構，我們可以將元件間的溝通關係建圖並加以分析。 再給定一些額外描述元件行為的參數，我們可以將資料流程式轉換成形式化數學模型。 利用最直接的方法將每個元件轉換成個別的模組，狀態空間會隨元件數量指數級的增長。 我們將重複的元件縮減為一個模組，利用一個模組來表達多個元件的行為，大幅減少了狀態空間。 實驗結果顯示，隨著重複元件數量的增加，狀態空間會以線性成長而狀態轉移數量會以平方成長。

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.