物聯(lián)網服務組合與驗證的研究.pdf

1、物聯(lián)網融合了物理世界和信息世界，延伸和擴展了互聯(lián)網，成為了大家研究的熱門領域。隨著物聯(lián)網的快速發(fā)展，物聯(lián)網也變得越來越復雜，使得現(xiàn)有對物聯(lián)網的研究已經有了局限性。一方面，由于物聯(lián)網中的設備直接運行于物理環(huán)境中，需要同物理環(huán)境進行直接交互。物理設備的運行和物理環(huán)境的改變通常是連續(xù)變化的，而對物理設備的控制常常是離散指令。目前對物聯(lián)網的研究在這一特性上考慮不夠，主要采用模型檢查方式的驗證，在處理連續(xù)變化時可能遇到狀態(tài)爆炸的情況。另一方面，物

2、聯(lián)網中用到的物理設備越來越多，使物聯(lián)網的規(guī)模變得越來越龐大，內部交互越來越復雜。目前對物聯(lián)網的研究，主要是對物聯(lián)網進行整體的分析，既不便于擴展和維護，其設計與驗證過程也較為復雜。
　　混成系統(tǒng)(Hybrid Systems)是一類同時包含連續(xù)動態(tài)行為和離散動態(tài)行為的系統(tǒng)?；斐上到y(tǒng)的建模方法同時具有離散和連續(xù)的刻畫能力，能夠較好的描述物聯(lián)網系統(tǒng)的離散指令和物理設備的連續(xù)行為，很好的符合了物聯(lián)網的特點。近年來，Andre Platze

3、r等提出了以微分動態(tài)邏輯為基礎的混成系統(tǒng)建模與驗證方法，取得了很好的研究成果，同時開發(fā)了混成系統(tǒng)自動驗證工具KeYmaera。針對分布式混成系統(tǒng)，微分動態(tài)邏輯后續(xù)又擴展為定量微分動態(tài)邏輯，在公式中引入了定量算子，支持分布式混成系統(tǒng)的建模，驗證工具也升級為KeYmaeraD，大大提高了原有模型的擴展與應用能力。
　　本文結合物聯(lián)網的特點，提出了一套對物聯(lián)網系統(tǒng)進行服務建模的方法，貫穿物聯(lián)網系統(tǒng)的模擬、組件化建模和驗證的整個過程，很好

4、的貼合了物聯(lián)網系統(tǒng)越來越龐大，內部交互越來越復雜的特點。
　　本文先將一個復雜的物聯(lián)網系統(tǒng)根據(jù)功能封裝成若干個小的成員服務，然后用PtolemyⅡ分別對成員服務進行可視化的設計和模擬，利用混成自動機作為橋梁，將設計圖轉化為混成程序，用混成系統(tǒng)對成員服務進行組件化建模，最后通過對成員服務進行組合的方式將成員服務合成一個整體服務。這種分而治之的方法，具有良好的模塊性，保證了物聯(lián)網系統(tǒng)的可擴展性。
　　而對物聯(lián)網服務的驗證，也可受