李文翔

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

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

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

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

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

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

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

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

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

(1)

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

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

(2)

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

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

(3)

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

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

1.2.1 原子服務(wù)建模

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

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

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

(4)

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

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

(5)

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

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

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

(6)

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

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

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

(7)

式中動作π可以是輸入動作、輸出動作或者空動作。

1.2.2 組合服務(wù)建模

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

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

ZHA=SA|LA|CA。

(8)

1.3 建模方法特點

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

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

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

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

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

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

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

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

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

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

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

3 實例

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

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

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

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

(9)

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

Enls=Enl+Enl
。

(10)

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

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

(11)

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

(12)

3) 感知型服務(wù)

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

(13)

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

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

P1=getps(ps).([ps=

(14)

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

(15)

5) 控制型服務(wù)

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

(16)

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

(17)

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

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

true。

(18)

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

(19)

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

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

(20)

(21)

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

(22)

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

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

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

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

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

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

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

4 結(jié)束語

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

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