物聯網服務的π-演算建模與驗證

李文翔

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

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

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

1 基于π-演算的物聯網服務建模

文獻[1]提出的基于環境的物聯網服務建模框架，將建模過程分成環境實體建模和物聯網服務建模兩個部分。依據π-演算的特點，結合基于環境的物聯網服務建模框架[1]，可以使用π-演算語法從動態行為角度描述環境實體和物聯網服務。

1.1 環境實體建模

環境實體是指物聯網系統運行環境下的一組實體，例如光照、溫度、空調等，其可分為被感知型環境實體和受控型環境實體。

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

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

(1)

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

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

(2)

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

定義3 一個受控型環境實體可以描述為

(3)

定義3給出的受控型環境實體，輸入動作clopi完成后，環境實體被設置為對應的狀態。

1.2 物聯網服務建模

1.2.1 原子服務建模

物聯網服務的功能通過其與環境實體之間的交互體現，服務通過交互感知到環境的狀態，及時地實施對環境的控制，實現改變環境狀態的目的[2]。依據服務的類型，原子服務可細分為感知型服務、控制型服務和業務邏輯型服務。

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

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

(4)

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

定義5 一個感知型服務SA可以定義為

(5)

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

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

定義6 一個控制型服務CA可以定義為

(6)

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

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

定義7 一個業務邏輯型服務LA可描述為

(7)

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

1.2.2 組合服務建模

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

定義8 一個組合服務ZHA可以定義為

ZHA=SA|LA|CA。

(8)

1.3 建模方法特點

物聯網系統是一個并發的交互式系統，是物聯網服務與環境實體之間交互的具體表現。基于π-演算和μ-演算相結合的建模方法，對物聯網服務、環境實體和物聯網服務能力三方面內容進行建模與分析，具有以下幾個特點：

1)整個建模方法不依賴任何特定的物聯網系統，使用嚴格的數學定義進行系統建模，具有高度的抽象性。

2)整個建模方法側重于物聯網服務與環境實體之間的交互行為。

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

4)使用μ-演算公式表示物聯網服務能力，本質上將物聯網服務具有的性質描述成動態行為的執行路徑，只關注服務功能需求問題。

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

2 物聯網服務驗證

本文將物聯網服務和環境實體視為進程實體，二者的并行交互形成了一個完整的物聯網系統。通過使用π-演算的反應規則[11]可以確定物聯網系統的事件發生序列，即物聯網服務和環境實體之間的動態行為交互過程。為此對物聯網服務的正確性驗證就可以看成物聯網服務和環境實體之間的動態交互序列的正確性驗證，可分解為以下三類性質，并統一采用μ-演算公式來表述。

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

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

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

3 實例

本文以智能會議室應用場景為例，用π-演算對環境實體和物聯網服務建模，將服務的正確性表述為μ-演算公式，最后使用MWB工具進一步驗證物聯網服務的正確性。

一個智能會議室場景為：會議室中裝有一盞日光燈和一臺投影儀。當投影儀開啟時，日光燈自動關閉。當投影儀關閉時，環境光線由亮變暗時，日光燈在2 s將會自動啟動；當環境光線由暗變亮時，日光燈在2 s內自動關閉。其建模如下：

1)被感知型環境實體

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

(9)

那么環境光實體可以定義為

Enls=Enl+Enl
。

(10)

2)受控型環境實體

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

(11)

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

(12)

3) 感知型服務

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

(13)

4) 業務邏輯型服務

業務邏輯服務P1，在使用輸入動作getps獲取投影儀的當前狀態后，依據當前狀態是否為開啟狀態，通過輸出動作lampcode發出關閉指令off。

P1=getps(ps).([ps=

(14)

業務邏輯服務P2，可通過輸入動作isbr與感光服務SA通信，然后通過輸出動作lampcode發出關閉指令off；又或者通過輸入動作isda與感光服務SA通信，而后使用輸入動作getps獲取投影儀狀態，依據投影儀是否關閉，通過輸出動作lampcode發出開啟指令。

(15)

5) 控制型服務

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

(16)

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

(17)

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

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

true。

(18)

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

(19)

(3) 日光燈2 s內啟動

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

(20)

(21)

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

(22)

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

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

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

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

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

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

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

4 結束語

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

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