面向資源的物聯(lián)網(wǎng)系統(tǒng)形式化建模與驗證

馬 莉，李維康，梁 晨，李愛萍

(太原理工大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，太原 030024)

1 引 言

基于物的互聯(lián)的物聯(lián)網(wǎng)技術(shù)被廣泛應(yīng)用于智能電網(wǎng)、智能交通、智能物流、環(huán)境監(jiān)測、老人護理等各種領(lǐng)域[1，2].近年來，軟件領(lǐng)域中面向服務(wù)技術(shù)的逐步成熟，為物聯(lián)網(wǎng)的應(yīng)用提供了技術(shù)實現(xiàn)的保障，許多研究者開始關(guān)注于面向服務(wù)的方法實現(xiàn)物聯(lián)網(wǎng)應(yīng)用.越來越多的物聯(lián)網(wǎng)服務(wù)及應(yīng)用，逐步成為人們?nèi)粘Ｉ钪胁豢苫蛉钡囊徊糠?同時，這種相關(guān)性也對這些物聯(lián)網(wǎng)應(yīng)用部署之前的測試和檢驗提出了較高的要求.為了確保物聯(lián)網(wǎng)系統(tǒng)的正確性和可靠性，在系統(tǒng)部署之前高效進行充分和必要的測試和檢驗就成為物聯(lián)網(wǎng)工程亟待解決的重要課題之一.

軟件測試對于檢驗系統(tǒng)的質(zhì)量問題存在固有的缺陷，特別是針對包含硬件設(shè)備和網(wǎng)絡(luò)傳輸?shù)奈锫?lián)網(wǎng)系統(tǒng)，傳統(tǒng)的測試方法不僅存在固有的無法進行完備測試的問題，還要面臨實際硬件設(shè)備和網(wǎng)絡(luò)的部署、調(diào)試等問題，造成測試周期和成本的急劇增長；而常規(guī)的仿真方法的檢驗，則面臨與實際系統(tǒng)差別較大的問題，無法對實際系統(tǒng)進行針對性檢驗；形式化方法是一種基于數(shù)學(xué)方式的系統(tǒng)描述和驗證方法，可以解決傳統(tǒng)測試的無法進行完備測試的問題，可以應(yīng)對傳統(tǒng)仿真方法與實際系統(tǒng)差別大的問題，但該方法也有其局限性，比如隨著狀態(tài)數(shù)增加而帶來的狀態(tài)爆炸等問題，目前尚無更好的徹底解決辦法[3].針對常規(guī)的物聯(lián)網(wǎng)應(yīng)用，形式化方法可以在成本和周期都較小的前提下，提供較好的檢驗方法和步驟，為高效進行物聯(lián)網(wǎng)系統(tǒng)的部署前檢驗提供有效的實施方法.

本文針對物聯(lián)網(wǎng)服務(wù)的部署前檢驗問題，提出一種形式化的建模和驗證方法，為物聯(lián)網(wǎng)系統(tǒng)的全面檢驗提供理論依據(jù)和實施參考.

2 相關(guān)工作

關(guān)于測試和驗證的問題，文獻[4，5]提到傳統(tǒng)的軟件測試在開發(fā)基于環(huán)境因素和特殊行為的系統(tǒng)的時候是有缺陷的，只能檢驗特定場景的局部系統(tǒng)行為，而采用形式化方法就克服了這些缺陷.文獻[6]提出了一種基于混成系統(tǒng)理論的物聯(lián)網(wǎng)服務(wù)建模與驗證框架，雖然為了避免狀態(tài)空間爆炸問題，使用了基于微分動態(tài)邏輯和定量微分動態(tài)邏輯的方法構(gòu)造物聯(lián)網(wǎng)服務(wù)的模型，但是把混成系統(tǒng)理論應(yīng)用到物聯(lián)網(wǎng)服務(wù)的研究還不夠成熟，對物聯(lián)網(wǎng)服務(wù)的建模與驗證還需要更進一步的探索.在質(zhì)量和可靠性方面，文獻[7]強調(diào)對服務(wù)質(zhì)量屬性的建模，但沒有考慮由于環(huán)境的動態(tài)變化性，如何對服務(wù)的動態(tài)行為進行建模.

近年來，國內(nèi)外的許多學(xué)者研究面向服務(wù)的方法與物聯(lián)網(wǎng)相結(jié)合.劉明星等人[8]基于服務(wù)組合的思想，提出了一種CPS建模與驗證方法，他們不僅提出了CPS資源的服務(wù)分類及組成框架，并根據(jù)時間自動機理論提出了對CPS的物理環(huán)境和服務(wù)的建模方法以及原子服務(wù)的組合方法，但由于CPS的復(fù)雜性，未對CPS不確定性的服務(wù)進行建模分析.

基于上述研究，考慮到物聯(lián)網(wǎng)的資源受限特性，本文結(jié)合REST面向資源的思想，研究一種面向資源的物聯(lián)網(wǎng)服務(wù)的建模和驗證方法.本文首先提出一種面向服務(wù)化的物聯(lián)網(wǎng)服務(wù)按需提供框架，其次提出面向資源的物聯(lián)網(wǎng)服務(wù)抽象建模方法，然后使用進程代數(shù)方法CSP對物聯(lián)網(wǎng)服務(wù)行為進行面向資源的抽象建模與分析，最后借助PAT工具對相關(guān)性質(zhì)進行了驗證.

3 物聯(lián)網(wǎng)服務(wù)提供的設(shè)計框架

3.1 一個特定的物聯(lián)網(wǎng)應(yīng)用場景

目前，由于霧霾現(xiàn)象的多次出現(xiàn)，人們開始關(guān)注環(huán)境污染對其自身的危害.環(huán)境污染給人們帶來的最直接的后果是使人類的生存環(huán)境質(zhì)量嚴(yán)重下降.以空氣質(zhì)量服務(wù)系統(tǒng)的物聯(lián)網(wǎng)應(yīng)用場景為例，該場景的應(yīng)用需求為：通過溫濕度傳感器采集室內(nèi)實時空氣溫度和濕度，并且自動調(diào)節(jié)空調(diào)、加濕器、除濕機來達(dá)到預(yù)定舒適溫濕度；通過二氧化碳傳感器、甲醛傳感器、粉塵顆粒傳感器分別采集室內(nèi)二氧化碳、甲醛、粉塵顆粒的濃度，并且根據(jù)濃度的設(shè)定自動調(diào)節(jié)電動窗戶、智能新風(fēng)系統(tǒng)、空氣凈化器工作.

3.2 實體提取

在不同的物聯(lián)網(wǎng)系統(tǒng)應(yīng)用場景中，物聯(lián)網(wǎng)服務(wù)系統(tǒng)與環(huán)境之間的相互作用是不同的.根據(jù)應(yīng)用需求，一般環(huán)境由環(huán)境實體和設(shè)備實體組成，這些環(huán)境實體分為兩大類：

1)被感知的環(huán)境實體.服務(wù)以感知的方式獲取這類實體的狀態(tài)值，但它不能直接改變這些實體的狀態(tài)，外界無法預(yù)測實體的狀態(tài)，它是以自己的方式變化著.例如，場景中的室內(nèi)空氣；

2)被控制的設(shè)備實體.服務(wù)不僅可以獲取這類實體的狀態(tài)值(即各項屬性值)，還可以向這些實體發(fā)送事先定義好的指令，以便改變實體的狀態(tài)，達(dá)到控制實體的狀態(tài)變化的目的.各種嵌入式設(shè)備均屬于該類實體，例如場景中的空調(diào)、加濕器等.

3.3 物聯(lián)網(wǎng)服務(wù)分類

基于服務(wù)的物聯(lián)網(wǎng)系統(tǒng)中，每個實體提供的功能都可以看作為一個服務(wù).按照不同的分類標(biāo)準(zhǔn)，物聯(lián)網(wǎng)服務(wù)類型可以有好多種，根據(jù)該空氣質(zhì)量服務(wù)應(yīng)用場景，按照其功能可將物聯(lián)網(wǎng)服務(wù)分為信息型服務(wù)、操作型服務(wù)和邏輯型服務(wù).它們都是具有原子性的服務(wù)，組合服務(wù)是由物聯(lián)網(wǎng)系統(tǒng)的綜合性服務(wù)構(gòu)成.

1)信息型服務(wù).這類服務(wù)主要進行信息的采集、存儲和查詢，通過感知外界環(huán)境實體的變化，將得到的信息傳遞給其他服務(wù).但每種信息型服務(wù)只能對其特定的環(huán)境實體屬性進行處理.

2)操作型服務(wù).這類服務(wù)與可控環(huán)境實體進行交互，先得到某種環(huán)境實體的操作信息，然后將這些信息轉(zhuǎn)換成操作命令，最后將其發(fā)送給對應(yīng)的環(huán)境實體，通過操作從而達(dá)到控制環(huán)境實體.

3)邏輯型服務(wù).這類服務(wù)是根據(jù)用戶的需求，將得到的信息按照提前設(shè)定好的業(yè)務(wù)邏輯進行分析、計算、處理，使生成的命令達(dá)到控制設(shè)備資源的目的.

3.4 物聯(lián)網(wǎng)服務(wù)框架

3.4.1 空氣質(zhì)量服務(wù)組成框架

根據(jù)以上實體提取和物聯(lián)網(wǎng)服務(wù)的分類，從圖1可以看出，空氣質(zhì)量服務(wù)由五部分組成：環(huán)境實體、信息型服務(wù)、邏輯型服務(wù)、操作型服務(wù)、設(shè)備實體.其中，環(huán)境實體是被感知的實體，設(shè)備實體是被控制的實體.在服務(wù)提供的過程中，信息型服務(wù)采集被監(jiān)測的環(huán)境實體的狀態(tài)信息，由通道傳送給邏輯型服務(wù)；邏輯型服務(wù)依據(jù)原先設(shè)定的業(yè)務(wù)邏輯，分析、計算處理數(shù)據(jù)，將結(jié)果發(fā)送給操作型服務(wù)；根據(jù)預(yù)定義的規(guī)則，操作型服務(wù)將結(jié)果數(shù)據(jù)翻譯成相應(yīng)的指令，將空調(diào)、窗戶等設(shè)備實體的狀態(tài)進行改變.在物聯(lián)網(wǎng)空氣質(zhì)量服務(wù)中，環(huán)境實體可以通過一系列的原子服務(wù)作用于設(shè)備實體，改變設(shè)備的狀態(tài)；設(shè)備實體也會反作用于環(huán)境實體，以達(dá)到改善空氣的目的.

圖1 空氣質(zhì)量服務(wù)組成框架結(jié)構(gòu)圖Fig.1 Framework of the components in air quality services

3.4.2 物聯(lián)網(wǎng)服務(wù)按需提供框架

按照本文場景描述，可以抽象出一種物聯(lián)網(wǎng)服務(wù)按需提供框架，該框架由兩大部分構(gòu)成，即實體類和物聯(lián)網(wǎng)服務(wù)系統(tǒng).

1)實體類包括環(huán)境實體和設(shè)備實體.其中，環(huán)境實體有空氣、油煙等，設(shè)備實體有空調(diào)、加濕器、凈化器等.此外，實體類之間也具有一定的聯(lián)系，例如，加濕器的開關(guān)狀態(tài)將會導(dǎo)致室內(nèi)濕度的變化.

2)物聯(lián)網(wǎng)服務(wù)系統(tǒng)包括原子服務(wù)和組合服務(wù).其中，原子服務(wù)由信息型原子服務(wù)、邏輯型原子服務(wù)、操作型原子服務(wù)三大類組成，通過各類服務(wù)自組織，組合出滿足用戶需求的物聯(lián)網(wǎng)服務(wù)，然后應(yīng)用到各種領(lǐng)域.

隨著物聯(lián)網(wǎng)服務(wù)的廣泛應(yīng)用，人們提出了各種需求.圖2是由簡單原子服務(wù)組合成更加復(fù)雜的組合服務(wù)的物聯(lián)網(wǎng)服務(wù)按需提供框架圖.當(dāng)用戶提出新的需求時，首先查找是否有恰好滿足需求的可重用服務(wù)，如果沒有，就查看由一些原子服務(wù)，通過重新組合得到的服務(wù)是否能夠滿足需求.例如，如果用戶的需求是PM2.5值監(jiān)測，根據(jù)需求發(fā)現(xiàn)原子服務(wù)中具有粉塵顆粒濃度監(jiān)測服務(wù)，因此直接選擇該服務(wù)；如果用戶的需求是溫濕度監(jiān)測，根據(jù)需求發(fā)現(xiàn)原子服務(wù)中具有溫度監(jiān)測和濕度監(jiān)測服務(wù)，因此選擇二者進行組合，將得到的組合模型提供給用戶.

圖2 物聯(lián)網(wǎng)服務(wù)按需提供框架結(jié)構(gòu)圖Fig.2 Offered framework of the Internet of things services

4 面向資源的抽象建模

4.1 REST化的物聯(lián)網(wǎng)服務(wù)

REST最初是由Roy Fielding博士在他的博士論文[9]中提出的.REST(Representational State Transfer，表述性狀態(tài)轉(zhuǎn)移)是一種跨平臺、跨語言的分布式系統(tǒng)設(shè)計的架構(gòu)風(fēng)格，REST式的Web服務(wù)是對REST在Web領(lǐng)域的實現(xiàn).可見，Web是一種遵循REST的面向資源的架構(gòu).

在REST架構(gòu)風(fēng)格中，核心思想是面向資源(Resource-Oriented)的概念.所謂資源，任何能夠被命名的信息都可以被抽象為資源.一個資源既可以是物理對象(比如房間、傳感器等)，也可以是抽象的概念(比如軟件、網(wǎng)絡(luò)環(huán)境等).將面向資源的思想與物聯(lián)網(wǎng)服務(wù)相結(jié)合，把物聯(lián)網(wǎng)應(yīng)用場景中的各個要素都看作資源，例如環(huán)境實體、設(shè)備、感知數(shù)據(jù)、服務(wù)、狀態(tài)信息等都可以抽象為資源.

4.2 面向資源的物聯(lián)網(wǎng)服務(wù)模型

在REST架構(gòu)風(fēng)格中，基于ROA(Resource-Oriented Architecture，面向資源的架構(gòu))的屬性，我們針對物聯(lián)網(wǎng)服務(wù)中的用戶需求對資源建模提出一些技術(shù)難點：如何對物聯(lián)網(wǎng)資源確定唯一的標(biāo)識符，并建立資源間的鏈接；如何對物聯(lián)網(wǎng)資源統(tǒng)一接口、確定操作方法；如何對物聯(lián)網(wǎng)資源定義表述格式，以便通過資源的表示構(gòu)成彼此的鏈接；如何對物聯(lián)網(wǎng)資源狀態(tài)進行高效的管理，實現(xiàn)面向資源架構(gòu)的無狀態(tài)性.針對以上的問題，結(jié)合面向資源架構(gòu)的思想提出了面向資源的物聯(lián)網(wǎng)服務(wù)模型.

在ROA中，URI(Universal Resource Identifier，統(tǒng)一資源標(biāo)識符)既是資源的名稱，也是資源的地址.因此，我們把物聯(lián)網(wǎng)服務(wù)資源形式化抽象定義為一個四元組(URI，Method，Link，MediaType).

資源URI定義為一個五元組(IP，ResourceType，ResourceId，Activity，Parameter).其中，IP表示URI的根目錄即服務(wù)端口形式；ResourceType表示資源設(shè)備類型；ResourceId表示資源設(shè)備的標(biāo)識符；Activity表示擴展后對資源的操作方法；Parameter表示操作時所需要調(diào)用的參數(shù).其中，Activity和Parameter可根據(jù)具體情況進行設(shè)定.例如http：//…/Sensors/{TempSensor.Id}/{Activity.Id}/{Parameter}

Method表示資源的接口操作方法.資源的接口操作方法信息都存在于HTTP方法中，HTTP基本的操作接口方法是GET、PUT、POST、DELETE.可根據(jù)用戶需求對操作接口的方法進行擴展，以滿足用戶更加復(fù)雜的操作.

Link表示通過資源的表述彼此連接起來，體現(xiàn)了資源的鏈接屬性.

MediaType表示資源的媒體類型.資源表述(Resource Representation)定義了媒體類型下的傳輸過程中數(shù)據(jù)采用的傳輸格式，文本、二進制流、XML和JSON等格式都可以作為資源的表述.比如，應(yīng)用中更為常見的設(shè)置是“application/json”和“application/xml”，分別代表JSON和XML類型.

通過簡單的服務(wù)場景來說明面向資源的物聯(lián)網(wǎng)服務(wù)模型具體的實現(xiàn).例如，通過溫度傳感器采集室內(nèi)的空氣溫度.當(dāng)溫度高于25℃時，打開空調(diào)的制冷系統(tǒng)；當(dāng)溫度低于15℃時，打開空調(diào)的制熱系統(tǒng).

為了實現(xiàn)以上的功能，如表1所示.首先，要查找所有的傳感器列表；其次，通過查找溫度傳感器來獲取室內(nèi)溫度的信息；再次，對室內(nèi)的溫度進行監(jiān)測，根據(jù)不同的溫度值，改變空調(diào)的運行狀態(tài).

表1 物聯(lián)網(wǎng)資源實例模型實驗數(shù)據(jù)表Table 1 Model of Internet of Things resources

在REST風(fēng)格架構(gòu)中，一個資源不僅包含自身的信息，還應(yīng)具有與其它相關(guān)資源的鏈接.下頁圖3為一個簡單的示例圖，體現(xiàn)了資源之間的Link.箭頭表示客戶端請求操作資源引起客戶端應(yīng)用狀態(tài)的轉(zhuǎn)移；箭頭旁邊的方法表示引起資源狀態(tài)轉(zhuǎn)移的操作方法.

針對上述服務(wù)，從開始獲取資源1，獲取資源2，獲取資源3，修改資源4.由于該服務(wù)是一個閉環(huán)監(jiān)控的狀態(tài)，因此修改了資源4的狀態(tài)后，還會轉(zhuǎn)移到資源3的狀態(tài)，進而達(dá)到繼續(xù)監(jiān)控的目的.

圖3 資源狀態(tài)轉(zhuǎn)移結(jié)構(gòu)圖Fig.3 State transition of resources

4.3 物聯(lián)網(wǎng)服務(wù)的進程代數(shù)方法建模與分析

4.3.1 進程代數(shù)方法CSP

通信順序進程[10](Communication Sequential Processes，CSP)是描述分布式并發(fā)軟件系統(tǒng)規(guī)格和設(shè)計的一種典型的進程代數(shù)方法.基于物聯(lián)網(wǎng)系統(tǒng)是一種分布式并發(fā)系統(tǒng)，本文就采用CSP來對REST架構(gòu)的物聯(lián)網(wǎng)服務(wù)進行形式化建模與分析.

針對CSP的概念，為了表述方便，我們進行符號的約定.設(shè)大寫字母P、Q、R表示進程，小寫字母x、y表示事件，大寫字母C表示事件集.CSP的基本成分是事件和進程，它有兩種基本的算子運算符：順序算子“→”和選擇算子“|”，例如進程P可以表示為x→Qπ，進程的選擇可以表示為(x→R|y→Q).此外，還定義了進程的復(fù)合操作，例如選擇進程(P[]Q)、或進程(P「?Q)、并發(fā)進程(P||Q)、混合進程(P|||Q)、順序進程(P;Q).

4.3.2 物聯(lián)網(wǎng)服務(wù)形式化建模

在進程代數(shù)的研究基礎(chǔ)上，我們將面向資源的物聯(lián)網(wǎng)服務(wù)(Resource-Oriented Service，ROS)定義為一個五元組ROS=(URL，Na，RC，CSP，Ope)，其中：

-URL表示面向資源服務(wù)的唯一標(biāo)識和地址；

-Na表示面向資源服務(wù)的名稱，與URL是一一對應(yīng)的；

-RC表示組成服務(wù)的資源集合，RC中包括原子服務(wù)和組合服務(wù).

-CSP表示進程代數(shù)表示方法，用來對服務(wù)的動態(tài)行為進行建模；

-Ope表示對服務(wù)進行的操作集合，分別是HTTP的操作方法GET、PUT、DELETE、POST.

定義1.原子服務(wù)(Atomic Service)為一個ROS，可以定義為AT=(URL，Na，RC，CSP，Ope)，其中：

-URL、Na和Ope都不為空；

-RC由信息型服務(wù)、邏輯型服務(wù)或操作型服務(wù)中的服務(wù)組成；

-CSP不為空，表示對物聯(lián)網(wǎng)原子服務(wù)的動態(tài)行為用CSP方法表示.

針對空氣質(zhì)量服務(wù)的應(yīng)用場景，濕度監(jiān)測系統(tǒng)是原子服務(wù).它可以建模為(URL，HumidityMonitor，RC，CSP，Ope)，其中：URL為濕度監(jiān)測服務(wù)的唯一標(biāo)識；HumidityMonitor是服務(wù)的名稱；RC為原子服務(wù)的資源集合；Ope包括有獲取濕度傳感器的信息、監(jiān)測室內(nèi)濕度以便觸發(fā)相應(yīng)的操作、更改除濕機或加濕器的狀態(tài)信息；CSP用來刻畫濕度監(jiān)測的動態(tài)行為，可表示為：

HumidityMonitor()=

[HumiData<30]open_Humidifier{HumidifierSwitch=1;

DehumidifierSwitch=0;}->ControlHumidity{HumiData=50;}-> HumidityMonitor()

[][HumiData>=30&&HumiData<=80]close_Humidifier_Dehumidifier{HumidifierSwitch=0;DehumidifierSwitch=0;} -> Skip

[][HumiData>80]open_Dehumidifier{DehumidifierSwitch=1;HumidifierSwitch=0;} ->ControlHumidity{HumiData=50;} -> HumidityMonitor();

甲醛監(jiān)測系統(tǒng)是原子服務(wù).它可以建模為(URL，MethanalMonitor，RC，CSP，Ope)，其中：URL為甲醛監(jiān)測服務(wù)的唯一標(biāo)識；MethanalMonitor是服務(wù)的名稱；RC為原子服務(wù)的資源集合；Ope包括有獲取甲醛濃度的信息、監(jiān)測甲醛濃度以便觸發(fā)相應(yīng)操作、更改相應(yīng)設(shè)備的狀態(tài)信息；CSP用來刻畫甲醛監(jiān)測的動態(tài)行為，可表示為：

MethanalMonitor()=

[MethanalConcentration>=80]open_Window_IntelligentFre

shAirSystem2{WindowSwitch=1;IntelligentFreshAirSystemSwitch=1;}->ControlMethanal{MethanalConcentration=0;}->MethanalMonitor()

[][MethanalConcentration<80]close_Window_IntelligentFreshAirSystem2{WindowSwitch=0;IntelligentFreshAirSystemSwitch=0;} -> Skip;

在空氣質(zhì)量服務(wù)的應(yīng)用場景中，還有溫度監(jiān)測系統(tǒng)、二氧化碳監(jiān)測系統(tǒng)、粉塵顆粒監(jiān)測系統(tǒng)，它們也都是原子服務(wù).同理，溫度監(jiān)測系統(tǒng)可以建模為(URL，TemperatureMonitor，RC，CSP，Ope)；二氧化碳監(jiān)測系統(tǒng)可以建模為(URL，CarbonDioxideMonitor，RC，CSP，Ope)；粉塵顆粒監(jiān)測系統(tǒng)可以建模為(URL，DustParticlesMonitor，RC，CSP，Ope).

定義2.組合服務(wù)(Composite Service)為一個ROS，可以定義為CS=(URL，Na，RC，CSP，Ope)，其中：

-URL、Na和Ope都不為空，分別是由組合后得到新的地址、名稱及操作集合；

-RC由各原子服務(wù)組合構(gòu)成了組合服務(wù)的資源集合；

-CSP不為空，通過按照進程的復(fù)合操作運算，對物聯(lián)網(wǎng)服務(wù)中組合服務(wù)的動態(tài)行為進行建模.

針對空氣質(zhì)量服務(wù)的應(yīng)用場景，環(huán)境監(jiān)測是一個組合服務(wù).它可以建模為(URL，CompositeService，RC，CSP，Ope)，其中：URL是環(huán)境監(jiān)測服務(wù)的唯一標(biāo)識；CompositeService是服務(wù)的名稱；RC為組合服務(wù)的資源集合，包括有溫濕度監(jiān)測、甲醛監(jiān)測、二氧化碳監(jiān)測及粉塵顆粒監(jiān)測.Ope包括有各種傳感器獲取信息、監(jiān)測信息觸發(fā)相應(yīng)操作、更改各種設(shè)備的狀態(tài)信息.CSP用來刻畫環(huán)境監(jiān)測中各服務(wù)的動態(tài)行為，則服務(wù)可表示為：

CompositeService()=if(time>10){EnvironmentMonitor()}

else{StopMonitor()};

EnvironmentMonitor()=TemperatureMonitor();HumidityMonitor();CarbonDioxideMonitor();MethanalMonitor();DustParticlesMonitor();TimeSet();

TimeSet()=timeset{time=0;} -> CompositeService();

StopMonitor()=change{time++;TempData=TempData+1;HumiData=HumiData-3;CO2Concentration=CO2Concentration+60;MethanalConcentration=MethanalConcentration+9;IndoorDustParticlesConcentration=IndoorDustParticlesConcentration+10;}->CompositeService();

5 基于PAT的物聯(lián)網(wǎng)服務(wù)驗證

本文采用模型檢測器PAT作為物聯(lián)網(wǎng)服務(wù)時效正確性驗證的工具.PAT模型檢測器是一個對并發(fā)實時系統(tǒng)建模、推理和驗證的工具.在PAT中，使用線性時序邏輯LTL對相關(guān)屬性進行驗證.

5.1 線性時序邏輯LTL

線性時序邏輯[11](Linear Temporary Logic，簡稱LTL)是在命題邏輯的基礎(chǔ)上加上時序算子組成.用時序算子來描述計算樹上的路徑的一些性質(zhì)，LTL包含的基本時序算子運算符有next算子?、existential算子◇、global算子?」、until算子∪.

而在PAT工具中，用戶要遵循一種性質(zhì)驗證語法：

F=e|prop|[]F|<>F|XF|F1∪F2|F1RF2

其中，F(xiàn)是一個LTL公式；e是事件；prop是預(yù)定義的命題；[]等同于“always”，在PAT中也被記作G；<>等同于“eventually”，在PAT中也被記作F；X等同于“next”；U等同于“until”.

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

物聯(lián)網(wǎng)服務(wù)的驗證包含對原子服務(wù)的驗證和對組合服務(wù)的驗證.針對空氣質(zhì)量服務(wù)系統(tǒng)，利用PAT工具對其進行驗證.

5.2.1 服務(wù)與驗證性質(zhì)相對應(yīng)

接下來，將服務(wù)與屬性性質(zhì)進行一一對應(yīng).

1)要驗證服務(wù)是否可以一直處于運行狀態(tài)(除非正常停止運行)，并且不期望的事件永遠(yuǎn)不會發(fā)生，就要驗證服務(wù)的安全性.服務(wù)的無死鎖性是一種典型的安全性.

2)要驗證服務(wù)中是否沒有包含有用的服務(wù)，就要驗證服務(wù)的無發(fā)散性.如果無發(fā)散性驗證是有效的，那么說明服務(wù)中包含有用的服務(wù).

3)要驗證服務(wù)中是否有不確定的狀態(tài)，就要驗證服務(wù)的確定性.如果確定性驗證是有效的，那么說明服務(wù)中任何一個狀態(tài)的轉(zhuǎn)移都不會導(dǎo)致兩個不同的狀態(tài).

4)要驗證服務(wù)最終期望的目標(biāo)狀態(tài)能否實現(xiàn)，就要驗證服務(wù)的可達(dá)性.希望在物聯(lián)網(wǎng)服務(wù)的控制下，被控制的設(shè)備實體最終能處于運行狀態(tài)，被感知的環(huán)境實體最終也能處于目標(biāo)狀態(tài).例如，在空氣質(zhì)量服務(wù)中，希望空調(diào)可以處于運行狀態(tài)；希望室內(nèi)的CO2濃度可以降到目標(biāo)值.

5)要驗證傳感器采集的信息是否可以觸發(fā)相應(yīng)的操作，就要驗證服務(wù)的活性，希望發(fā)生的事件最終都能發(fā)生.例如當(dāng)濕度小于30%時，則自動開啟加濕器進行加濕工作.

5.2.2 對原子服務(wù)和組合服務(wù)分別進行驗證

1)原子服務(wù)驗證(舉例溫度監(jiān)測服務(wù)的驗證)

(1)安全性(即無死鎖性)

#assert TemperatureMonitor()deadlockfree;

(2)無發(fā)散性

#assert TemperatureMonitor()divergencefree;

(3)確定性

#assert TemperatureMonitor()deterministic;

(4)可達(dá)性

驗證服務(wù)中空調(diào)是否可以處于運行狀態(tài).用CSP#斷言表示為：#define goal10(AirconditioningSwitch==1);

#assert TemperatureMonitor()reaches goal10;

#assert TemperatureMonitor()|= <>goal10;

驗證服務(wù)中溫度是否可以達(dá)到預(yù)期狀態(tài)值.用CSP#斷言表示為：#define goal11(TempData>=18&&TempData<=25);

#assert TemperatureMonitor()reaches goal11;

#assert TemperatureMonitor()|= []<>goal11;

(5)活性

驗證當(dāng)室內(nèi)溫度大于等于25℃ 時， 最終可以自動開啟空調(diào)進行制冷降溫.用CSP#斷言表示為：

#define Temperature(TempData>=25);

#assert TemperatureMonitor()|=[](Temperature-><>open_Airconditioning_cool);

驗證當(dāng)室內(nèi)溫度大于18℃且小于25℃時，下一個狀態(tài)是關(guān)閉空調(diào)設(shè)備.用CSP#斷言表示為：

#define Temp(18

#assert TemperatureMonitor() |= Temp->X close_Airconditioning;

同理，通過PAT平臺對各原子服務(wù)的模型進行自動驗證，可以得出該空氣質(zhì)量原子服務(wù)模型具備以上性質(zhì).

2)組合服務(wù)驗證

(1)安全性(無死鎖性)

#assert CompositeService()deadlockfree;

(2)無發(fā)散性

#assert CompositeService()divergencefree;

(3)確定性

#assert CompositeService()deterministic;

(4)可達(dá)性

驗證服務(wù)中溫度、濕度、二氧化碳濃度、甲醛濃度和粉塵顆粒濃度是否可以達(dá)到預(yù)期狀態(tài)值.用CSP#斷言表示為：

#define goal6((TempData>=18&&TempData<=25) && (HumiData>=30&&HumiData<=80) && CO2Concentration<1200 && MethanalConcentration<80 && IndoorDustParticlesConcentration<150);

#assert CompositeService()reaches goal6;

#assert CompositeService()|=[]<>goal6;

(5)活性

在組合服務(wù)中驗證當(dāng)甲醛濃度偏高時，最終都會打開窗戶和智能新風(fēng)系統(tǒng).用CSP#斷言表示為：

#assert CompositeService()|=[]Methanal-><>open_Window_IntelligentFreshAirSystem2);

例如，將組合服務(wù)安全性的CSP#斷言表示輸入到PAT驗證器中，得到的結(jié)果是該性質(zhì)是被滿足的，如圖4所示.

圖4 組合服務(wù)實驗結(jié)果結(jié)構(gòu)圖Fig.4 Experimental result of composite service

采用同樣的方法，通過PAT平臺對前文中提到的各原子服務(wù)和組合服務(wù)中的相關(guān)性質(zhì)分別進行可滿足性驗證，結(jié)果顯示，其他性質(zhì)也是可滿足的.

6 結(jié)束語

本文針對特定場景的應(yīng)用需求，對物聯(lián)網(wǎng)服務(wù)按照功能進行了分類，結(jié)合面向服務(wù)和面向資源的思想，提出了物聯(lián)網(wǎng)服務(wù)按需提供的框架和面向資源的物聯(lián)網(wǎng)服務(wù)模型，并給出溫度監(jiān)測系統(tǒng)實例場景說明了該服務(wù)化模型的具體應(yīng)用.然后，通過采用進程代數(shù)CSP的方法，分別對原子服務(wù)和組合服務(wù)進行了抽象建模.最后，采用PAT模型檢測工具，對空氣質(zhì)量服務(wù)案例的性質(zhì)進行了驗證.通過驗證該物聯(lián)網(wǎng)服務(wù)模型滿足無死鎖性、無發(fā)散性、確定性、可達(dá)性、活性這五種性質(zhì)的過程，為應(yīng)用實例的具體部署和實施提供參考.本文主要研究的是服務(wù)的順序組合方式，下一步還需要研究與實際場景對應(yīng)的服務(wù)的其他組合方式.此外，實驗中形式化驗證過程中產(chǎn)生的狀態(tài)數(shù)量會隨時間的推移而增加，因此需要研究好的方法和技術(shù)來避免狀態(tài)爆炸問題.

[1] Wu Zhen-yu.Research on web of things service environment architecture and key technologies[D].Beijing：Beijing University of Posts and Telecommunications，2013.

[2] Li Hang.The study and realization of service platform for intelligent sensor network based on REST architecture style[D].Shenyang：Shenyang Normal University，2015.

[3] Sun Jun，Liu Yang，Dong Jin-song，et al.Modeling and verifying hierarchical real-time systems using stateful timed CSP[J].ACM Transactions on Software Engineering and Methodology(TOSEM)，2013，22(1)：1-3.

[4] Liu Yan，Zhang Xian，Liu Yang，et al.Towards formal modeling and verification of pervasive computing systems[J].Transactions on Computational Collective Intelligence XVI，2014，8070：62-91.

[5] Liu Yan.Applying model checking to pervasive computing systems[D].Singapore：National University of Singapore，2014.

[6] Ye Lin，Tang Pu，Guo Li-peng，et al.Modeling and verification of internet of things service based on the composite system[J].Journal of Chinese Computer Systems，2013，34(12)：2663-2668.

[7] Li Ge，Wei Qiang，Li Li-xing，et al.Modeling of the internet of things services：a modeling method based on the environment[J].China Science：Information Science，2013，43(10)：1198-1218.

[8] Liu Ming-xing，Ma Wu-bin，Deng Su，et al.Modeling and verification of services oriented cyber physical systems[J].Journal of Computer Applications，2014，34(6)：1770-1773.

[9] Fielding R T，Architectural styles and the design of network-based software architecture[D].Irvine：University of California，2000.

[10] Gu Tian-long.Formal methods in software development[M].Beijing：Higher Education Press，2005.

[11] Cheng Yi-yun.Adaptive software requirements analysis based on the linear temporal logic[J].Digital Technology and Application，2011，(10)：134-136.

附中文參考文獻：

[1] 吳振宇.基于Web的物聯(lián)網(wǎng)應(yīng)用體系架構(gòu)和關(guān)鍵技術(shù)研究[D].北京：北京郵電大學(xué)，2013.

[2] 李 航.基于REST架構(gòu)風(fēng)格的智能傳感器網(wǎng)服務(wù)平臺的研究與實現(xiàn)[D].沈陽：沈陽師范大學(xué)，2015.

[6] 葉 林，湯 瀑，郭立鵬，等.基于混成系統(tǒng)的物聯(lián)網(wǎng)服務(wù)建模與驗證[J].小型微型計算機系統(tǒng)，2013，34(12)：2663-2668.

[7] 李 戈，魏 強，李力行，等.物聯(lián)網(wǎng)服務(wù)建模：一種基于環(huán)境建模的方法[J].中國科學(xué)：信息科學(xué)，2013，43(10)：1198-1218.

[8] 劉明星，馬武彬，鄧 蘇，等.面向服務(wù)的信息物理融合系統(tǒng)建模與驗證[J].計算機應(yīng)用，2014，34(6)：1770-1773.

[10] 古天龍.軟件開發(fā)的形式化方法[M].北京：高等教育出版社，2005.

[11] 程逸云.基于線性時序邏輯自適應(yīng)軟件的需求分析[J].數(shù)字技術(shù)與應(yīng)用，2011，(10)：134-136.