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

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

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

1 引 言

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

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

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

2 相關工作

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

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

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

3 物聯(lián)網服務提供的設計框架

3.1 一個特定的物聯(lián)網應用場景

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

3.2 實體提取

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

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

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

3.3 物聯(lián)網服務分類

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

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

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

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

3.4 物聯(lián)網服務框架

3.4.1 空氣質量服務組成框架

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

圖1 空氣質量服務組成框架結構圖Fig.1 Framework of the components in air quality services

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

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

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

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

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

圖2 物聯(lián)網服務按需提供框架結構圖Fig.2 Offered framework of the Internet of things services

4 面向資源的抽象建模

4.1 REST化的物聯(lián)網服務

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

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

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

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

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

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

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

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

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

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

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

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

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

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

圖3 資源狀態(tài)轉移結構圖Fig.3 State transition of resources

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

4.3.1 進程代數方法CSP

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

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

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

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

-URL表示面向資源服務的唯一標識和地址；

-Na表示面向資源服務的名稱，與URL是一一對應的；

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

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

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

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

-URL、Na和Ope都不為空；

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

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

針對空氣質量服務的應用場景，濕度監(jiān)測系統(tǒng)是原子服務.它可以建模為(URL，HumidityMonitor，RC，CSP，Ope)，其中：URL為濕度監(jiān)測服務的唯一標識；HumidityMonitor是服務的名稱；RC為原子服務的資源集合；Ope包括有獲取濕度傳感器的信息、監(jiān)測室內濕度以便觸發(fā)相應的操作、更改除濕機或加濕器的狀態(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)是原子服務.它可以建模為(URL，MethanalMonitor，RC，CSP，Ope)，其中：URL為甲醛監(jiān)測服務的唯一標識；MethanalMonitor是服務的名稱；RC為原子服務的資源集合；Ope包括有獲取甲醛濃度的信息、監(jiān)測甲醛濃度以便觸發(fā)相應操作、更改相應設備的狀態(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;

在空氣質量服務的應用場景中，還有溫度監(jiān)測系統(tǒng)、二氧化碳監(jiān)測系統(tǒng)、粉塵顆粒監(jiān)測系統(tǒng)，它們也都是原子服務.同理，溫度監(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.組合服務(Composite Service)為一個ROS，可以定義為CS=(URL，Na，RC，CSP，Ope)，其中：

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

-RC由各原子服務組合構成了組合服務的資源集合；

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

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

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)網服務驗證

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

5.1 線性時序邏輯LTL

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

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

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

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

5.2 物聯(lián)網服務驗證

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

5.2.1 服務與驗證性質相對應

接下來，將服務與屬性性質進行一一對應.

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

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

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

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

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

5.2.2 對原子服務和組合服務分別進行驗證

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

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

#assert TemperatureMonitor()deadlockfree;

(2)無發(fā)散性

#assert TemperatureMonitor()divergencefree;

(3)確定性

#assert TemperatureMonitor()deterministic;

(4)可達性

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

#assert TemperatureMonitor()reaches goal10;

#assert TemperatureMonitor()|= <>goal10;

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

#assert TemperatureMonitor()reaches goal11;

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

(5)活性

驗證當室內溫度大于等于25℃ 時， 最終可以自動開啟空調進行制冷降溫.用CSP#斷言表示為：

#define Temperature(TempData>=25);

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

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

#define Temp(18

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

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

2)組合服務驗證

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

#assert CompositeService()deadlockfree;

(2)無發(fā)散性

#assert CompositeService()divergencefree;

(3)確定性

#assert CompositeService()deterministic;

(4)可達性

驗證服務中溫度、濕度、二氧化碳濃度、甲醛濃度和粉塵顆粒濃度是否可以達到預期狀態(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)活性

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

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

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

圖4 組合服務實驗結果結構圖Fig.4 Experimental result of composite service

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

6 結束語

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

[2] 李 航.基于REST架構風格的智能傳感器網服務平臺的研究與實現[D].沈陽：沈陽師范大學，2015.

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

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

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

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

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