物聯(lián)網(wǎng)服務(wù)組合與驗(yàn)證的研究.pdf

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

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

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

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