物聯(lián)網(wǎng)服務(wù)的π-演算建模與驗(yàn)證

李文翔

(福建商學(xué)院 信息工程學(xué)院，福建 福州 350012)

物聯(lián)網(wǎng)服務(wù)建模是物聯(lián)網(wǎng)研究領(lǐng)域的一個(gè)分支，相比較于傳統(tǒng)的服務(wù)，物聯(lián)網(wǎng)服務(wù)具有實(shí)時(shí)性、資源約束性、位置相關(guān)性等性質(zhì)。在物聯(lián)網(wǎng)服務(wù)建模研究中，國(guó)內(nèi)外學(xué)者做了大量的相關(guān)研究：李戈等[1]和李力行等[2]采用時(shí)間自動(dòng)機(jī)理論建模物聯(lián)網(wǎng)服務(wù)以及物理環(huán)境，并將用戶期望的服務(wù)特性描述為時(shí)序邏輯公式，從而驗(yàn)證物聯(lián)網(wǎng)服務(wù)運(yùn)行于特定環(huán)境下能夠滿足期望的性質(zhì)；針對(duì)基于自動(dòng)機(jī)、Petri網(wǎng)等模型的狀態(tài)空間爆炸問(wèn)題，葉林等[3]提出使用微分動(dòng)態(tài)邏輯和定量微分動(dòng)態(tài)邏輯對(duì)物聯(lián)網(wǎng)服務(wù)建模與驗(yàn)證；韓喬等[4]針對(duì)語(yǔ)義物聯(lián)網(wǎng)服務(wù)的正確性驗(yàn)證問(wèn)題，提出基于時(shí)態(tài)描述邏輯ALC-μ的語(yǔ)義物聯(lián)網(wǎng)服務(wù)驗(yàn)證方法；馬莉等[5]提出一種面向資源的物聯(lián)網(wǎng)系統(tǒng)形式化建模與驗(yàn)證方法，使用通信順序進(jìn)程CSP對(duì)物聯(lián)網(wǎng)系統(tǒng)的動(dòng)態(tài)行為進(jìn)行建模，利用線性時(shí)序邏輯LTL刻畫(huà)待驗(yàn)證的性質(zhì)；Yen等[6-7]擴(kuò)展了現(xiàn)有OWL-S表達(dá)功能，將其用于對(duì)物聯(lián)網(wǎng)服務(wù)的描述，并以此為基礎(chǔ)討論了物聯(lián)網(wǎng)服務(wù)的組合問(wèn)題；De等[8]基于本體語(yǔ)言分別對(duì)實(shí)體、資源和物聯(lián)網(wǎng)服務(wù)進(jìn)行語(yǔ)義建模；Sivrikaya等[9]針對(duì)智慧城市的具體應(yīng)用，提出了一個(gè)服務(wù)識(shí)別和組合的分布式框架ISCO(intelligent framework for service discovery and composition)，在基于語(yǔ)義網(wǎng)的物聯(lián)網(wǎng)服務(wù)和物理設(shè)備統(tǒng)一模型的基礎(chǔ)上，使用OWL-S描述服務(wù)；為高效地獲取物聯(lián)網(wǎng)的各項(xiàng)資源(物理設(shè)備、物聯(lián)網(wǎng)服務(wù)等)，Gomes等[10]提出了一個(gè)基于語(yǔ)義的資源識(shí)別服務(wù)QoDisco，該服務(wù)主要用于識(shí)別基于本體論進(jìn)行語(yǔ)義描述的物聯(lián)網(wǎng)各項(xiàng)資源。這些學(xué)者分別從不同的角度闡述物聯(lián)網(wǎng)服務(wù)形式化建模與驗(yàn)證的機(jī)制，為本文提供了參考。

為此，本文以描述物聯(lián)網(wǎng)服務(wù)間的動(dòng)態(tài)交互問(wèn)題為出發(fā)點(diǎn)，提出基于環(huán)境的物聯(lián)網(wǎng)服務(wù)π-演算[11]建模方法以及使用μ-演算[12]描述物聯(lián)網(wǎng)服務(wù)所具備的性質(zhì)。針對(duì)特定實(shí)例場(chǎng)景，使用π-演算定義物聯(lián)網(wǎng)服務(wù)和環(huán)境實(shí)體，利用μ-演算對(duì)物聯(lián)網(wǎng)服務(wù)能力進(jìn)行描述，最后使用模型檢測(cè)工具M(jìn)WB(mobile workbench)進(jìn)行驗(yàn)證。

1 基于π-演算的物聯(lián)網(wǎng)服務(wù)建模

文獻(xiàn)[1]提出的基于環(huán)境的物聯(lián)網(wǎng)服務(wù)建?？蚣?，將建模過(guò)程分成環(huán)境實(shí)體建模和物聯(lián)網(wǎng)服務(wù)建模兩個(gè)部分。依據(jù)π-演算的特點(diǎn)，結(jié)合基于環(huán)境的物聯(lián)網(wǎng)服務(wù)建?？蚣躘1]，可以使用π-演算語(yǔ)法從動(dòng)態(tài)行為角度描述環(huán)境實(shí)體和物聯(lián)網(wǎng)服務(wù)。

1.1 環(huán)境實(shí)體建模

環(huán)境實(shí)體是指物聯(lián)網(wǎng)系統(tǒng)運(yùn)行環(huán)境下的一組實(shí)體，例如光照、溫度、空調(diào)等，其可分為被感知型環(huán)境實(shí)體和受控型環(huán)境實(shí)體。

1) 被感知型環(huán)境實(shí)體。此類環(huán)境實(shí)體具有被感知的屬性以及屬性的獲取操作，例如光照、溫度等。建模時(shí)采用π-演算的輸出動(dòng)作作為被感知屬性的獲取操作。被感知屬性通過(guò)輸出動(dòng)作傳遞，以便其他環(huán)境實(shí)體或物聯(lián)網(wǎng)服務(wù)交互獲取。

定義1 一個(gè)抽象的被感知型環(huán)境實(shí)體可描述為

(1)

定義1給出了環(huán)境實(shí)體一種抽象的形式。但在實(shí)際應(yīng)用場(chǎng)景中，被感知屬性存在多種屬性值。例如光照屬性可取的屬性值集合為{bright,dark,normal}。為此在定義1的基礎(chǔ)上給出一個(gè)具體的被感知型環(huán)境實(shí)體的形式化定義。

定義2 一個(gè)具體的被感知型環(huán)境實(shí)體對(duì)象可描述為

(2)

2) 受控型環(huán)境實(shí)體。相比較于被感知型環(huán)境實(shí)體，此類環(huán)境實(shí)體除了受控操作外，還有狀態(tài)的獲取操作。這里使用輸入動(dòng)作表示受控操作，輸出動(dòng)作作為狀態(tài)獲取操作，以實(shí)現(xiàn)其他服務(wù)或環(huán)境實(shí)體獲取當(dāng)前操作狀態(tài)。

定義3 一個(gè)受控型環(huán)境實(shí)體可以描述為

(3)

定義3給出的受控型環(huán)境實(shí)體，輸入動(dòng)作clopi完成后，環(huán)境實(shí)體被設(shè)置為對(duì)應(yīng)的狀態(tài)。

1.2 物聯(lián)網(wǎng)服務(wù)建模

1.2.1 原子服務(wù)建模

物聯(lián)網(wǎng)服務(wù)的功能通過(guò)其與環(huán)境實(shí)體之間的交互體現(xiàn)，服務(wù)通過(guò)交互感知到環(huán)境的狀態(tài)，及時(shí)地實(shí)施對(duì)環(huán)境的控制，實(shí)現(xiàn)改變環(huán)境狀態(tài)的目的[2]。依據(jù)服務(wù)的類型，原子服務(wù)可細(xì)分為感知型服務(wù)、控制型服務(wù)和業(yè)務(wù)邏輯型服務(wù)。

1) 感知型服務(wù)。此類服務(wù)的主要功能在于定時(shí)獲取某一類環(huán)境實(shí)體的狀態(tài)或感知屬性，然后依據(jù)狀態(tài)或感知屬性的值做相應(yīng)的處理。其感知操作可以表示為一個(gè)輸入動(dòng)作。使用輸出動(dòng)作表示下一步將要處理的操作，以便與其他服務(wù)交互。

定義4 一個(gè)時(shí)鐘變量Clocki(i是時(shí)鐘數(shù)且為大于等于0的正整數(shù))可以表示為

(4)

定義4給出的時(shí)鐘變量起定時(shí)作用。tick為1個(gè)時(shí)鐘，輸出動(dòng)作start表示啟動(dòng)操作。當(dāng)要表示5個(gè)時(shí)鐘內(nèi)啟動(dòng)某個(gè)操作P，采用π演算的并行操作可將進(jìn)程進(jìn)一步書(shū)寫(xiě)為Clock5|start.P,那么感知型服務(wù)的形式化定義如下。

定義5 一個(gè)感知型服務(wù)SA可以定義為

(5)

式中：m為大于等于1的正整數(shù)；輸入動(dòng)作Attri表示獲取被感知型環(huán)境實(shí)體的第i個(gè)屬性xi；Vali表示第i個(gè)屬性可取的屬性值；輸出動(dòng)作op表示感知服務(wù)以便與其他服務(wù)交互的操作。

2) 控制型服務(wù)。通過(guò)輸入動(dòng)作獲取其他服務(wù)發(fā)來(lái)的控制指令，再依據(jù)指令類型由輸出動(dòng)作向受控型環(huán)境實(shí)體發(fā)送控制操作，控制型服務(wù)的形式化定義如下。

定義6 一個(gè)控制型服務(wù)CA可以定義為

(6)

式中：輸入動(dòng)作getcodei表示獲取其他服務(wù)發(fā)來(lái)的控制指令ci；ti則表示控制指令的某種類型；輸出動(dòng)作clopi表示向受控型環(huán)境實(shí)體發(fā)送控制操作。

3) 業(yè)務(wù)邏輯型服務(wù)。此類服務(wù)通過(guò)輸入動(dòng)作獲取感知型服務(wù)傳來(lái)的信息或受控型環(huán)境實(shí)體的狀態(tài)，然后根據(jù)傳來(lái)的信息或狀態(tài)做相應(yīng)的邏輯處理，比如再次查詢受控型環(huán)境實(shí)體的狀態(tài)等，最后使用輸出動(dòng)作傳遞控制指令。業(yè)務(wù)邏輯型服務(wù)的形式化定義如下。

定義7 一個(gè)業(yè)務(wù)邏輯型服務(wù)LA可描述為

(7)

式中動(dòng)作π可以是輸入動(dòng)作、輸出動(dòng)作或者空動(dòng)作。

1.2.2 組合服務(wù)建模

以原子服務(wù)為基礎(chǔ)，使用π-演算的并行操作可以得到多個(gè)組合服務(wù)。組合服務(wù)的形式化定義如下。

定義8 一個(gè)組合服務(wù)ZHA可以定義為

ZHA=SA|LA|CA。

(8)

1.3 建模方法特點(diǎn)

物聯(lián)網(wǎng)系統(tǒng)是一個(gè)并發(fā)的交互式系統(tǒng)，是物聯(lián)網(wǎng)服務(wù)與環(huán)境實(shí)體之間交互的具體表現(xiàn)?；讦?演算和μ-演算相結(jié)合的建模方法，對(duì)物聯(lián)網(wǎng)服務(wù)、環(huán)境實(shí)體和物聯(lián)網(wǎng)服務(wù)能力三方面內(nèi)容進(jìn)行建模與分析，具有以下幾個(gè)特點(diǎn)：

1)整個(gè)建模方法不依賴任何特定的物聯(lián)網(wǎng)系統(tǒng)，使用嚴(yán)格的數(shù)學(xué)定義進(jìn)行系統(tǒng)建模，具有高度的抽象性。

2)整個(gè)建模方法側(cè)重于物聯(lián)網(wǎng)服務(wù)與環(huán)境實(shí)體之間的交互行為。

3)使用π-演算對(duì)物聯(lián)網(wǎng)服務(wù)和環(huán)境實(shí)體進(jìn)行行為建模，可以更為抽象地表示物聯(lián)網(wǎng)服務(wù)與環(huán)境實(shí)體之間的行為交互，建模過(guò)程主要以功能行為的描述為主。

4)使用μ-演算公式表示物聯(lián)網(wǎng)服務(wù)能力，本質(zhì)上將物聯(lián)網(wǎng)服務(wù)具有的性質(zhì)描述成動(dòng)態(tài)行為的執(zhí)行路徑，只關(guān)注服務(wù)功能需求問(wèn)題。

5)行為間交互傳遞的是消息，結(jié)合π-演算描述能力以及名字的概念[11]，將連續(xù)型數(shù)值屬性進(jìn)行離散化表示。

2 物聯(lián)網(wǎng)服務(wù)驗(yàn)證

本文將物聯(lián)網(wǎng)服務(wù)和環(huán)境實(shí)體視為進(jìn)程實(shí)體，二者的并行交互形成了一個(gè)完整的物聯(lián)網(wǎng)系統(tǒng)。通過(guò)使用π-演算的反應(yīng)規(guī)則[11]可以確定物聯(lián)網(wǎng)系統(tǒng)的事件發(fā)生序列，即物聯(lián)網(wǎng)服務(wù)和環(huán)境實(shí)體之間的動(dòng)態(tài)行為交互過(guò)程。為此對(duì)物聯(lián)網(wǎng)服務(wù)的正確性驗(yàn)證就可以看成物聯(lián)網(wǎng)服務(wù)和環(huán)境實(shí)體之間的動(dòng)態(tài)交互序列的正確性驗(yàn)證，可分解為以下三類性質(zhì)，并統(tǒng)一采用μ-演算公式來(lái)表述。

1)安全性，表示服務(wù)交互過(guò)程中不期望發(fā)生的事件或行為不會(huì)被執(zhí)行。

2) 活性，表示服務(wù)交互過(guò)程中期望發(fā)生的事件或行為最終能執(zhí)行。

3) 時(shí)間約束，表示服務(wù)交互過(guò)程中某些事件或行為的執(zhí)行時(shí)間要求。

3 實(shí)例

本文以智能會(huì)議室應(yīng)用場(chǎng)景為例，用π-演算對(duì)環(huán)境實(shí)體和物聯(lián)網(wǎng)服務(wù)建模，將服務(wù)的正確性表述為μ-演算公式，最后使用MWB工具進(jìn)一步驗(yàn)證物聯(lián)網(wǎng)服務(wù)的正確性。

一個(gè)智能會(huì)議室場(chǎng)景為：會(huì)議室中裝有一盞日光燈和一臺(tái)投影儀。當(dāng)投影儀開(kāi)啟時(shí)，日光燈自動(dòng)關(guān)閉。當(dāng)投影儀關(guān)閉時(shí)，環(huán)境光線由亮變暗時(shí)，日光燈在2 s將會(huì)自動(dòng)啟動(dòng)；當(dāng)環(huán)境光線由暗變亮?xí)r，日光燈在2 s內(nèi)自動(dòng)關(guān)閉。其建模如下：

1)被感知型環(huán)境實(shí)體

在本實(shí)例中，環(huán)境光被識(shí)別為被感知型環(huán)境實(shí)體。環(huán)境光通過(guò)輸出動(dòng)作getint向感知服務(wù)輸出光線的明亮程度int。其中int∈{da,br}，da表示暗光，br表示強(qiáng)光。為此環(huán)境光類可以定義為

(9)

那么環(huán)境光實(shí)體可以定義為

Enls=Enl+Enl
。

(10)

2)受控型環(huán)境實(shí)體

投影儀實(shí)體具有3個(gè)動(dòng)作：向外提供投影儀當(dāng)前狀態(tài)ps的輸出動(dòng)作getps、打開(kāi)投影儀輸入動(dòng)作pon以及關(guān)閉投影儀輸入動(dòng)作poff。投影儀則定義為

(11)

日光燈實(shí)體除了和投影儀實(shí)體具有類似的3個(gè)動(dòng)作，還使用時(shí)鐘算子表示開(kāi)或關(guān)的時(shí)延性。日光燈則定義為

(12)

3) 感知型服務(wù)

感光服務(wù)SA先通過(guò)輸入動(dòng)作getint獲取環(huán)境光線的明亮程度int，然后根據(jù)明亮程度，分別通過(guò)輸出動(dòng)作isda和isbr與業(yè)務(wù)邏輯服務(wù)通信。

(13)

4) 業(yè)務(wù)邏輯型服務(wù)

業(yè)務(wù)邏輯服務(wù)P1，在使用輸入動(dòng)作getps獲取投影儀的當(dāng)前狀態(tài)后，依據(jù)當(dāng)前狀態(tài)是否為開(kāi)啟狀態(tài)，通過(guò)輸出動(dòng)作lampcode發(fā)出關(guān)閉指令off。

P1=getps(ps).([ps=

(14)

業(yè)務(wù)邏輯服務(wù)P2，可通過(guò)輸入動(dòng)作isbr與感光服務(wù)SA通信，然后通過(guò)輸出動(dòng)作lampcode發(fā)出關(guān)閉指令off；又或者通過(guò)輸入動(dòng)作isda與感光服務(wù)SA通信，而后使用輸入動(dòng)作getps獲取投影儀狀態(tài)，依據(jù)投影儀是否關(guān)閉，通過(guò)輸出動(dòng)作lampcode發(fā)出開(kāi)啟指令。

(15)

5) 控制型服務(wù)

控制型服務(wù)Lcon，用來(lái)控制日光燈的開(kāi)啟或關(guān)閉。首先通過(guò)輸入動(dòng)作lampcode獲取指令code，依據(jù)指令的類型，向日光燈實(shí)體發(fā)出開(kāi)啟lon或關(guān)閉loff的動(dòng)作。

(16)

為驗(yàn)證服務(wù)的正確性，需要將上述模塊進(jìn)行組合計(jì)算，因此一個(gè)智能會(huì)議室場(chǎng)景可以描述為

(17)

那么該智能會(huì)議室場(chǎng)景可滿足的三類性質(zhì)，描述如下：

(1)當(dāng)投影儀打開(kāi)時(shí)，日光燈關(guān)閉，如式(18)所示。

true。

(18)

(2) 當(dāng)投影儀關(guān)閉時(shí)，環(huán)境光線昏暗情況下，日光燈打開(kāi)，如式(19)所示。

(19)

(3) 日光燈2 s內(nèi)啟動(dòng)

該性質(zhì)可分為投影儀開(kāi)啟后日光燈2 s內(nèi)關(guān)閉(如式(20)所示)和投影儀關(guān)閉后日光燈2 s內(nèi)開(kāi)啟(如式(21)所示)。

(20)

(21)

(4) 當(dāng)投影儀打開(kāi)后，環(huán)境光線昏暗情況下，日光燈不會(huì)打開(kāi),如式(22)所示。

(22)

其中式(18)和式(19)表示的是活性，時(shí)間約束性質(zhì)由式(20)和式(21)表示，而式(22)則表示安全性。

將本文所描述的環(huán)境實(shí)體和物聯(lián)網(wǎng)服務(wù)以及式(18)—式(22)使用MWB工具進(jìn)行描述，并使用prove命令可以得到所設(shè)計(jì)的物聯(lián)網(wǎng)服務(wù)建模滿足式(18)—式(22)所代表的性質(zhì)，其在MWB工具上的運(yùn)行效果如圖1—圖5所示。這驗(yàn)證了所設(shè)計(jì)的物聯(lián)網(wǎng)服務(wù)建模的正確性。

圖1 式(18)的驗(yàn)證結(jié)果Fig.1 The verification result of the formula (18)

圖2 式(19)的驗(yàn)證結(jié)果Fig.2 The verification result of the formula (19)

圖3 式(20)的驗(yàn)證結(jié)果Fig.3 The verification result of the formula (20)

圖4 式(21)的驗(yàn)證結(jié)果Fig.4 The verification result of the formula (21)

圖5 式(22)的驗(yàn)證結(jié)果Fig.5 The verification result of the formula (22)

4 結(jié)束語(yǔ)

本文針對(duì)基于環(huán)境建模的物聯(lián)網(wǎng)服務(wù)框架，從動(dòng)態(tài)行為交互建模的角度出發(fā)，提出了一種基于π-演算和μ-演算相結(jié)合的物聯(lián)網(wǎng)服務(wù)建模方法，并給出智能會(huì)議室應(yīng)用場(chǎng)景實(shí)例說(shuō)明此方法的具體應(yīng)用。首先通過(guò)使用π-演算分別對(duì)環(huán)境實(shí)體和物聯(lián)網(wǎng)服務(wù)進(jìn)行行為建模，然后使用μ-演算將物聯(lián)網(wǎng)服務(wù)具有的性質(zhì)描述成動(dòng)態(tài)行為的執(zhí)行路徑，最后采用MWB模型檢測(cè)工具，對(duì)智能會(huì)議室實(shí)例的性質(zhì)進(jìn)行了驗(yàn)證，通過(guò)驗(yàn)證該模型滿足安全性、活性和時(shí)間約束三個(gè)性質(zhì)，進(jìn)一步說(shuō)明了此方法的正確性和可行性，為物聯(lián)網(wǎng)服務(wù)建模研究提供了參考。

本文研究的是物聯(lián)網(wǎng)服務(wù)動(dòng)態(tài)行為建模，其服務(wù)組合方式以并行組合為主，下一步將對(duì)環(huán)境實(shí)體狀態(tài)的自主變化、連續(xù)型數(shù)值的表示以及服務(wù)的其他組合方式等問(wèn)題進(jìn)行建模描述，同時(shí)也需要解決在實(shí)驗(yàn)驗(yàn)證過(guò)程中出現(xiàn)的狀態(tài)空間爆炸問(wèn)題。