陳 光 蔣同海 王 蒙 唐新余 季文飛

1(中國科學院新疆理化技術(shù)研究所 新疆 烏魯木齊 830011)2(中國科學院大學 北京 100049)3(江蘇中科西北星信息科技有限公司 江蘇 無錫 214135)4(新疆民族語音語言信息處理實驗室 新疆 烏魯木齊 830011)5(中國科學院物聯(lián)網(wǎng)研究發(fā)展中心 江蘇 無錫 214135)

0 引 言

物聯(lián)網(wǎng)(Internet of Things,IoT)，指的是將各種信息傳感設備通過多種組網(wǎng)技術(shù)與互聯(lián)網(wǎng)相結(jié)合形成的動態(tài)松耦合系統(tǒng)[1]。物聯(lián)網(wǎng)是繼計算機、互聯(lián)網(wǎng)與移動通信網(wǎng)絡之后的世界信息產(chǎn)業(yè)的第三次浪潮。國內(nèi)外業(yè)界人士都將發(fā)展物聯(lián)網(wǎng)視為新的技術(shù)創(chuàng)新點和經(jīng)濟增長點[2-5]。從總體上看，我國的物聯(lián)網(wǎng)技術(shù)產(chǎn)業(yè)鏈仍處于概念和探索階段，物聯(lián)網(wǎng)的整個技術(shù)體系架構(gòu)和產(chǎn)業(yè)模式尚未成熟[6]。

與傳統(tǒng)互聯(lián)網(wǎng)不同，物聯(lián)網(wǎng)被認為具有一些特殊的性質(zhì)[1]。物聯(lián)網(wǎng)的特殊性質(zhì)使得物聯(lián)網(wǎng)系統(tǒng)相比于一般的互聯(lián)網(wǎng)系統(tǒng)具有更多的系統(tǒng)狀態(tài)，并且因為這些系統(tǒng)狀態(tài)之間的轉(zhuǎn)換與物理世界的交互性，往往具有很強的實時性要求[7]，所以需要在物聯(lián)網(wǎng)系統(tǒng)設計階段進行充分的考慮。

時間自動機可以直觀地刻畫實時系統(tǒng)與時間有關(guān)的行為[8]，是物聯(lián)網(wǎng)實時系統(tǒng)進行設計和建模的重要方法?；跁r間自動機的理論研究，也產(chǎn)生了許多時間自動機建模和模型檢測工具[9]。

本文探討了基于時間自動機進行物聯(lián)網(wǎng)系統(tǒng)建模的理論、方法、工具和建模實踐。以物聯(lián)網(wǎng)溫度傳感器感知物理溫度環(huán)境為例，說明了基于時間自動機理論使用UPPAAL建模工具進行物聯(lián)網(wǎng)系統(tǒng)建模和模型檢測的方法，并進行了溫度感知的建模實踐。

1 相關(guān)工作

在時間自動機的理論研究方面，文獻[10-12]都對時間自動機的形式化理論進行了研究。文獻[12]最早認為時間自動機是一個4元組的概念。韓德帥等[11]在關(guān)于時間自動機的理論研究中認為時間自動機是6元組的概念，但是沒有在約束集合的定義中考慮時間自動機的屬性變量和屬性約束。李力行等[10]在基于時間自動機的建模與驗證研究中，考慮到了時間自動機中的屬性約束對時間自動機格局造成的影響，提出了7元組的時間自動機形式化定義，但是對于時鐘約束和屬性約束的區(qū)別和聯(lián)系，闡述得不夠明確。上述研究中，都沒有指出如何依據(jù)時間自動機理論進行時間自動機建模的方法，也沒有說明時間自動機理論與建模實踐之間的關(guān)系。

本文基于Bengtsson等[12]的時間自動機理論研究(UPPAAL以此為基礎(chǔ)實現(xiàn))，結(jié)合使用UPPAAL進行時間自動機的建模實踐，總結(jié)得出了時間自動機的6元組形式化定義。給出了時鐘變量、時鐘約束、屬性變量、屬性約束，以及時鐘屬性映射(時鐘屬性解釋)與時鐘屬性映射滿足時鐘屬性約束等相關(guān)概念的精確形式化定義。本文結(jié)合一個建模實例說明了時間自動機理論研究對于建模的指導意義?；谶@些理論研究，說明了使用時間自動機建立物聯(lián)網(wǎng)系統(tǒng)模型的方法。

在使用時間自動機進行建模和模型檢測方面，文獻[13-14]對機器人系統(tǒng)和關(guān)鍵通信節(jié)點進行了時間自動機的建模和分析；文獻[15]將時間自動機建模和模型檢測的方法應用到高鐵跨界臨時限速的問題上，但是都沒有給出明確的建模過程和檢測方法；文獻[16]對RFID等常見的物聯(lián)網(wǎng)物端傳感設備進行了時間自動機建模和分析，但是沒有將其與物聯(lián)網(wǎng)云端服務聯(lián)動起來，對完整的物聯(lián)網(wǎng)業(yè)務系統(tǒng)進行建模。上述所有的建模研究更側(cè)重于在理想情況中對物聯(lián)網(wǎng)系統(tǒng)進行建模，沒有對可能出現(xiàn)的故障情況做出考慮，在系統(tǒng)組成的建模上也沒有體現(xiàn)出如何針對系統(tǒng)容錯性進行建模。

本文在第5節(jié)的建模實踐中，根據(jù)物聯(lián)網(wǎng)溫度傳感器感知物理環(huán)境溫度的需求，建立了物聯(lián)網(wǎng)實時溫度感知系統(tǒng)模型。對物聯(lián)網(wǎng)系統(tǒng)可能出現(xiàn)設備故障的情況以及系統(tǒng)容錯性做出了充分的考慮。通過設計，所有接入到這個物聯(lián)網(wǎng)系統(tǒng)中的溫度傳感器都可以進入故障狀態(tài)，并設定，只要有一個溫度傳感器沒有發(fā)生故障，則溫度傳感器管理服務就不會進入故障狀態(tài)，以此體現(xiàn)所設計物聯(lián)網(wǎng)系統(tǒng)的容錯性。即使在系統(tǒng)中接入了發(fā)生故障的傳感器，甚至不接入傳感器，溫度傳感器管理服務也可以快速指示出現(xiàn)故障的狀態(tài)，以此體現(xiàn)物聯(lián)網(wǎng)實時系統(tǒng)的實時感知特性。

2 時間自動機建模理論

時間自動機的建模和驗證方法都是建立在時間自動機的理論上實現(xiàn)的。本節(jié)首先介紹與時間自動機形式化定義相關(guān)的概念，探討關(guān)于時鐘和屬性約束之間的關(guān)系。然后給出時間自動機的形式化定義，澄清時間自動機狀態(tài)和格局的關(guān)系，并給出格局轉(zhuǎn)換、緊迫和原子狀態(tài)的形式化定義。最后給出時間自動機網(wǎng)絡的形式化定義。

2.1 屬性變量和屬性約束

在一個時間自動機中可能存在多個屬性變量，這些屬性變量構(gòu)成了屬性變量的集合V。例如：V={temperature,humidity,luminosity}表示了一個由溫度、濕度和光照度構(gòu)成的屬性變量集合。

屬性約束可以是包含多個屬性變量的元組，例如ρ=〈temperature≥10,humidity<50〉，但不一定包含所有的屬性變量，例如〈luminosity≥0〉只對屬性變量luminosity做出限制。

2.2 時鐘變量和時鐘約束

時鐘約束可以是包含多個時鐘變量的元組，例如：η=〈x≥2,1≤y<10,z>0〉，但不一定包含所有的時鐘變量，例如〈y≥0〉只對時鐘變量y做出限制。

2.3 時鐘屬性約束集合

2.4 不變性約束與守衛(wèi)約束

時間自動機引入了位置的概念，時間自動機的所有位置組成時間自動機的位置集合N。對于N中的某個位置l，可以對應兩種不同形式的約束。

定義7限制時間自動機狀態(tài)可以進入某個位置l的約束稱為守衛(wèi)性約束(guard)，一般用g來表示。

值得注意的是，I僅包含了到不變性約束的映射，對于守衛(wèi)約束不做定義和限制。

2.5 時間自動機約束之間的關(guān)系

在進行時間自動機物聯(lián)網(wǎng)體系結(jié)構(gòu)建模的時候，必須明確時鐘約束與屬性約束、守衛(wèi)約束與不變性約束之間的關(guān)系，在設計時間自動機的約束條件時做到概念清晰。

時鐘約束與屬性約束可以看成是從構(gòu)成約束的變量集合類型角度進行分類的結(jié)果。而守衛(wèi)約束和不變性約束則是從約束與位置的關(guān)系角度進行分類的結(jié)果。在時間自動機建模的時候，這些約束可以互相包含。守衛(wèi)約束或者不變性約束中既可以包含時鐘約束，也可以包含屬性約束。而一個時鐘約束或者屬性約束既可能是一個不變性約束，也有可能是一個守衛(wèi)約束。

例如圖1所示的時間自動機中的約束所示的時間自動機模型中，S0位置的不變性約束是時鐘約束c≤10，S1位置的不變性約束是屬性約束temperature<30，屬性約束temperature>26和時鐘約束c>10共同構(gòu)成進入S1狀態(tài)的守衛(wèi)約束。

圖1 時間自動機中的約束

2.6 時鐘屬性映射與滿足約束

定義10時鐘屬性映射u滿足時鐘屬性約束φ。對于時鐘屬性約束φ∈B(X)，如果時鐘屬性映射(時鐘屬性解釋)u中的每一個分量〈Xi=c〉均滿足時鐘屬性約束φ中對應分量上的約束條件，即〈Xi=c〉∈〈Xi～c〉，則稱時鐘屬性映射(時鐘屬性解釋)u滿足時鐘屬性約束φ，記為：u∈φ。

對應地，時鐘屬性解釋u滿足守衛(wèi)時鐘約束g，可以記為：u∈g；時鐘屬性解釋u滿足不變性約束I(l)，可以記為：u∈I(l)。

可以將一個時鐘屬性約束〈X1～c1,X2～c2,…,Xn～cn〉理解為一個n維空間中點集的概念，而時鐘屬性映射(時鐘屬性解釋)〈X1=c1,X2=c2,…，Xn=cn〉可以理解為一個具體的點的概念。這樣可以很容易理解時鐘屬性映射滿足時鐘屬性約束的概念，比如〈x≤2〉代表一個以2為端點的射線，因為x∈R，射線是無窮多個點的集合， 而〈x=1〉代表了一個具體的點，由于點屬于點集，所以自然有〈x=1〉∈〈x≤2〉。

2.7 時間自動機的形式化定義

2.8 時間自動機的狀態(tài)和格局

需要特別指出的是，各研究對時間自動機的狀態(tài)定義，不相同，文獻[10]認為時間自動機的狀態(tài)就是指時間自動機的位置，而文獻[12]認為時間自動機的狀態(tài)是包含了時鐘屬性解釋的二元組。為了避免混淆，考慮到在學術(shù)研究中探討“時間自動機狀態(tài)轉(zhuǎn)換”的時候一般是指時間自動機的位置發(fā)生變化，因此我們將狀態(tài)與位置的概念等同起來，引入一個新的概念——格局，用它來表示包含時間取值和屬性取值的一個時間自動機狀態(tài)。

定義12時間自動機的格局(Status)。一個時間自動機的格局定義為一個二元組〈l,u〉，其中l(wèi)∈N代表一個位置，u代表此時間自動機時鐘屬性變量集合X下的一個時鐘屬性解釋?？梢岳斫鈺r間自動機的格局為包含某個時鐘屬性解釋的位置，也就是包含了時間和屬性取值的狀態(tài)。

定義13時間自動機格局變換(Operational Semantics)。對于時間自動機中的一般位置(狀態(tài))l∈N，包括初始狀態(tài)l0都存在以下2種變換方式：

從時間自動機格局變換的定義中可以很容易推導出一個定理：在時間自動機中，屬性變量取值的變化只發(fā)生在位置改變的格局變換中，時間流逝的格局變換不會造成屬性變量取值的變化。

2.9 緊迫狀態(tài)與原子狀態(tài)

從緊迫狀態(tài)和原子狀態(tài)的定義中可以看出，緊迫狀態(tài)(位置)和原子狀態(tài)下都不包含時間流逝的格局變換。并且處于原子狀態(tài)的時間自動機在進入此狀態(tài)與進行位置改變的格局變換時，不能被其他的時間自動機的任何格局變換中斷。

2.10 時間自動機網(wǎng)絡

定義16時間自動機的積和時間自動機網(wǎng)絡。對于2個時間自動機A1=〈N1,l10,Σ1,X1,E1,I1〉和A2=〈N2,l20,Σ2,X2,E2,I2〉，如果它們的消息(動作)集合滿足Σ1∩Σ2≠?，則稱時間自動機A1、A2是能夠串聯(lián)(組裝)的，將A1和A2串聯(lián)的結(jié)果稱為2個時間自動機的積，記為：A1‖A2。

時間自動機A1和A2的積，可以看成一個新的時間自動機，即A1‖A2=〈N1∪N2,〈l10,l20〉,Σ1∪Σ2,X1∪X2,E1∪E2,I1∪I2〉，對于新的時間自動機Ai如果也滿足(Σ1∪Σ2)∩Σi≠?，則可以繼續(xù)串聯(lián)時間自動機進行積的運算。

將2個或者2個以上時間自動機串聯(lián)的結(jié)果M=A1‖A2‖…‖An,n≥2 稱為時間自動機網(wǎng)絡。

3 時間自動機建模方法

物聯(lián)網(wǎng)系統(tǒng)的時間自動機建模主要分為2個步驟。首先針對物聯(lián)網(wǎng)系統(tǒng)中的每一個資源進行時間自動機建模，然后再把不同資源的時間自動機模型，通過發(fā)送和接收消息組合起來，形成時間自動機網(wǎng)絡。接下來我們以物理環(huán)境和溫度傳感器為例，探討基于時間自動機理論進行物聯(lián)網(wǎng)系統(tǒng)建模的方法。

假設對夏日的某個室內(nèi)空氣溫度進行建模，室外溫度為50 ℃，室內(nèi)溫度初始為40 ℃，由于室內(nèi)溫度低于室外溫度，室內(nèi)溫度以每100個時間單位增長1 ℃的速度增長，直到50 ℃。室內(nèi)溫度可以被物聯(lián)網(wǎng)系統(tǒng)中的傳感器物理實體所感知，讀取當前的室內(nèi)溫度進入物聯(lián)網(wǎng)系統(tǒng)。

對于室內(nèi)溫度物理環(huán)境時間自動機，首先從狀態(tài)上進行分析，室內(nèi)空氣溫度會隨時間而變化，但這是其屬性的變化，并沒有新的狀態(tài)產(chǎn)生，因此空氣只有一個狀態(tài)loop，loop是空氣的初始狀態(tài)，后續(xù)所有屬性變化也一直停留在此狀態(tài)，即有：

NAir={loop}，lAir0=loop

空氣能夠被傳感器感知其溫度狀態(tài)，則空氣時間自動機與傳感器時間自動機之間必然有消息傳遞，因為是感知溫度，命名為GetAirTemperature，所以有：

ΣAir={GetAirTemperature}

從時鐘變量和屬性變量的角度分析，空氣本身擁有屬性溫度，命名為temperature。為了模擬空氣每100個時間單位增加1 ℃的性質(zhì)，還應該為空氣建立一個時鐘計數(shù)器inc_clock，故有：

XAir={temperature,inc_clock}

為了使得溫度能夠在100個時間單位內(nèi)完成自增，必須限制空氣時間自動機停留在loop狀態(tài)的時間不得超過100個時間單位。因此有：

IAir={loop→〈inc_clock≤100〉}

在傳感器進行溫度感知的時候，空氣時間自動機無條件地將自身的溫度狀態(tài)發(fā)送給傳感器時間自動機，因此溫度感知的格局變換沒有任何守衛(wèi)約束與變量賦值操作，只有消息的發(fā)送：

圖2 空氣溫度時間自動機模型

使用同樣的分析方法對溫度傳感器進行建模，可以得到溫度傳感器的形式化模型：

ASensor=〈NSen,lSen0,ΣSen,XSen,ESen,ISen〉，其中：

Nsen={run,fault}，lSen0=run,

ΣSen={GetAirTemperature},

XSen={sen_clock},

ISen={run→〈sen_clock≤10〉},

對溫度傳感器時間自動機形式化模型進行等效轉(zhuǎn)換，得到圖形化的溫度傳感器時間自動機如圖3所示。其中：“?”代表接收消息GetAirTemperature。

圖3 溫度傳感器時間自動機模型

將建立的空氣溫度與溫度傳感器模型應用基于時間自動機的積的理論串聯(lián)起來，形成時間自動機網(wǎng)絡，就完成了一個具有簡單溫度感知功能的物聯(lián)網(wǎng)系統(tǒng)時間自動機模型。

由于時間自動機建模分析和時間自動機形式化表述占用的篇幅過長，且形式化時間自動機表述與圖形化時間自動機表述完全等效，為了節(jié)約篇幅，我們在后續(xù)的時間自動機建模討論中，不再贅述建模分析和形式化模型表述，而直接給出圖形化形式模型。但這并不意味著時間自動機理論對于建模是不重要的。事實上，時間自動機理論研究對于建立時間自動機模型具有十分重要的意義。

從時間自動機的建模方法中可以看出，物聯(lián)網(wǎng)系統(tǒng)的建模過程，就是通過分析物聯(lián)網(wǎng)系統(tǒng)組成資源的性質(zhì)，填充其時間自動機形式化定義中所規(guī)定的內(nèi)容集合，從而得到對應資源的時間自動機模型，最后再把這些物聯(lián)網(wǎng)資源的時間自動機模型串聯(lián)組裝起來組成時間自動機網(wǎng)絡，從而得到整個物聯(lián)網(wǎng)系統(tǒng)的時間自動機模型。所以時間自動機理論是進行物聯(lián)網(wǎng)系統(tǒng)建模的基礎(chǔ)。

對時間自動機的形式化理論進行研究，不僅能夠從數(shù)學的形式化的思維上加深對于時間自動機建模的理解，而且有助于在建模過程中對于模型中出現(xiàn)的概念和屬性，例如時間自動機的狀態(tài)和格局，時鐘約束、不變性約束、守衛(wèi)約束等，有清晰而深刻的認識，更有助于規(guī)范使用時間自動機進行建模的過程。在時間自動機理論的指導下使用正確的狀態(tài)或者約束，刻畫物聯(lián)網(wǎng)系統(tǒng)資源所具有的性質(zhì)，建立正確的符合客觀系統(tǒng)資源性質(zhì)和規(guī)律的時間自動機模型，從而更好地研究物聯(lián)網(wǎng)系統(tǒng)在時間和狀態(tài)變換方面的性質(zhì)和規(guī)律，把控物聯(lián)網(wǎng)系統(tǒng)設計的正確性和實時性是否滿足預期的需求。

4 時間自動機建模工具

UPPAAL是由瑞典的Uppsala大學與丹麥的Aalborg大學聯(lián)合研發(fā)的時間自動機建模和模型驗證檢測工具，主要針對實時系統(tǒng)的建模、仿真和性質(zhì)驗證。UPPAAL目前已經(jīng)成功地運用于實時控制器的設計和通信協(xié)議的性質(zhì)驗證。

文獻[8]在其研究中指出，相比于其他的時間自動機建模工具，比如HYTECH、Kronos(Grenoble)和Epsilon(Aalborg)等，UPPAAL在時間和空間上的性能明顯更好，具有顯著的高效性。

UPPAAL具有可視化的描述界面，使用方便、高效，實用性高。 UPPAAL設計了一個易于用戶操作和使用的圖形界面，主要包括三個部分：系統(tǒng)編輯器(system editor)、模擬器(simulator)和驗證器(verifier)。

使用UPPAAL的編輯器界面進行時間自動機的建模。UPPAAL的編輯器界面如圖4所示，詳細的布局區(qū)域和功能菜單介紹可以參考文獻[17]。

圖4 UPPAAL編輯器視圖

基于時間自動機的形式化模型，使用UPPAAL可以很快建立出時間自動機的圖形化模型。使用圖4所示工具欄中的“創(chuàng)建位置”功能，可以創(chuàng)建時間自動機位置集合N中的所有位置。雙擊圖中的具體位置節(jié)點，可以編輯此位置的名稱、不變性約束與節(jié)點類型(包括初始狀態(tài)，緊迫狀態(tài)和原子狀態(tài))信息，如圖5左側(cè)所示。

圖5 編輯時間自動機的位置和邊

使用圖4所示工具欄中的“創(chuàng)建邊”按鈕可以創(chuàng)建時間自動機邊的集合E中的所有狀態(tài)轉(zhuǎn)換邊。雙擊圖中具體的邊，可以編輯此狀態(tài)轉(zhuǎn)換邊的守衛(wèi)約束、發(fā)送接收消息和需要重新賦值或者歸零的時鐘變量與屬性變量，如圖5右側(cè)所示。

使用UPPAAL的模擬器界面進行時間自動機模型的仿真。UPPAAL的模擬器界面如圖6所示。

圖6 UPPAAL模擬器視圖

圖6中間所示的組裝視圖展示了組成時間自動機網(wǎng)絡的所有時間自動機組件，包含了第3節(jié)中介紹的空氣模型和傳感器模型。

圖6下側(cè)的消息傳遞視圖展示了在執(zhí)行時間自動機位置改變的格局變換時，伴隨發(fā)生的時間自動機之間的信息傳遞情況。

圖6右側(cè)的“變量”窗口打印出了在當前的時鐘屬性解釋之下，時間自動機網(wǎng)絡所有全局和私有時鐘變量和屬性變量的取值。

圖6左側(cè)的“使能遷移”視圖列出了在此時鐘解釋之下，時間自動機網(wǎng)絡中能夠執(zhí)行的所有的位置改變格局變換。左下的“模擬Trace”軌跡記錄視圖記錄了模擬仿真過程經(jīng)歷的所有時間自動機位置改變格局變換，并支持對這些格局變換進行前進、后退、重放和保存等功能。

使用UPPAAL的驗證器界面進行時間自動機網(wǎng)絡模型性質(zhì)的驗證。驗證器界面如圖7所示。

圖7 UPPAAL驗證器視圖

圖7中，“性質(zhì)列表”展示了所有已經(jīng)編輯的系統(tǒng)性質(zhì)，右側(cè)的按鈕可以對物聯(lián)網(wǎng)系統(tǒng)的性質(zhì)進行添加、刪除等操作。在“待驗證性質(zhì)”中輸入或者修改系統(tǒng)性質(zhì)。在“備注”中可以添加這個系統(tǒng)性質(zhì)的文字說明。選中一條性質(zhì)，點擊“開始驗證”按鈕，就可以在“驗證進度與結(jié)果”視圖中展示所設計的時間自動機網(wǎng)絡是否滿足該性質(zhì)。

5 物聯(lián)網(wǎng)溫度感知系統(tǒng)建模驗證實踐

本節(jié)以溫度感知物聯(lián)網(wǎng)系統(tǒng)為例，進行一個相對比較完整的物聯(lián)網(wǎng)實時系統(tǒng)時間自動機建模和模型仿真驗證，從而對前文論述的理論研究進行實踐。

5.1 溫度感知物聯(lián)網(wǎng)系統(tǒng)建模

5.1.1空氣物理環(huán)境建模

溫度感知物聯(lián)網(wǎng)系統(tǒng)中，空氣物聯(lián)網(wǎng)環(huán)境包含室外溫度和室內(nèi)溫度2個可變的溫度參數(shù)，只有在系統(tǒng)初始化的時候，才能確定具體的室內(nèi)和室外溫度。如果室內(nèi)溫度小于室外溫度，則室內(nèi)溫度每隔一定的時間間隔(時間間隔可變)，以一定的增量(增量可變)升高，但最高不超過室外溫度。如果室內(nèi)溫度大于室外溫度，則室內(nèi)溫度每隔一定的時間間隔，以一定的增量減小，但最低不低于室外溫度。室內(nèi)溫度可以被溫度傳感器感知(在UPPAAL建模中體現(xiàn)為信號的發(fā)送)。

在UPPAAL中可以使用UPPAAL的模板功能來處理這些參數(shù)可變的情況，如圖8上側(cè)的參數(shù)欄所示，使用OUTSIDE_TEMPERATURE代表室外溫度，INIT_TEMPERATURE代表初始的室內(nèi)溫度，INTERVAL代表溫度變化間隔，布爾變量INC代表進行溫度的增加或者降低，INCREMENT代表每次溫度變化的增量。

圖8 使用模板建?？諝鉁囟葧r間自動機模型

聲明了可變參數(shù)后，在建模時就可以將可變參數(shù)視為已知的量，在時間自動機模型變量聲明時直接使用，如圖8下側(cè)所示的“變量”聲明中進行空氣溫度的初始化時，使用了INIT_TEMPERATURE，對小屋的初始溫度進行賦值。

在需要建模一個具體的空氣溫度時間自動機模型時，只需要在“模型聲明”中填入?yún)?shù)并引入系統(tǒng)，就可以很快完成不同資源組件的建模。假定在夏季室外溫度50 ℃，室內(nèi)初始溫度為35 ℃，溫度每100個時間間隔上升1 ℃；而在冬季室外溫度為0 ℃，室內(nèi)初始溫度為15 ℃，每100個時間間隔下降1 ℃。如圖9所示，分別完成了夏季和冬季空氣溫度物理環(huán)境的建模。

圖9 使用模板創(chuàng)建空氣溫度時間自動機模型的聲明

5.1.2溫度傳感器建模

溫度感知系統(tǒng)使用了三個溫度傳感器(可以基于溫度傳感器模板聲明接入更多的傳感器)進行溫度的感知。在云端實現(xiàn)了一個溫度傳感器管理服務，來管理和展示溫度傳感器的工作狀態(tài)，并收集溫度傳感器感知的溫度數(shù)據(jù)。

溫度傳感器每隔一定的時間間隔進行一次溫度感知，并將感知到的溫度發(fā)送給云端溫度傳感器管理服務。如果在規(guī)定的時間間隔內(nèi)溫度傳感器沒有完成溫度感知，則認為溫度傳感器發(fā)生了故障。按照溫度傳感器建模要點，我們可以很快使用UPPAAL建立溫度傳感器的時間自動機模板，如圖10所示。

圖10 溫度傳感器時間自動機模板

可以觀察到，相比于圖3討論的溫度傳感器模型，圖10中溫度傳感器時間自動機模型多出了一個sent狀態(tài)，這是由于在UPPAAL中，不能在一個有向邊上同時處理2個消息的發(fā)送或者接收，為了建模溫度傳感器從空氣物理環(huán)境中感知溫度并將感知到的結(jié)果發(fā)送給云端服務的行為，引入了一個虛擬的狀態(tài)。我們給這個虛擬的sent狀態(tài)一個原子狀態(tài)的屬性，在sent節(jié)點沒有任何時間流逝的格局變換，在溫度傳感器通過GetAirTemperature感知外部溫度，并通過SentAirTemperature發(fā)送溫度數(shù)據(jù)到云端服務的過程中，不會被時間自動機網(wǎng)絡中其他任何的格局變換所打斷，從而達到了將sent狀態(tài)和run狀態(tài)合并為一個狀態(tài)建模的目的。

5.1.3云端管理服務建模

云端溫度傳感器管理服務在運行時啟動時鐘計數(shù)器開始計時，接收所有溫度傳感器實體發(fā)送的溫度并歸零計時時鐘，如果10個時間單位都沒有接收到任何溫度傳感器發(fā)送的溫度信息，則認為所有的溫度傳感器都故障了，服務指示出溫度傳感器故障狀態(tài)。云端溫度傳感器管理服務的時間自動機模型如圖11所示。

圖11 溫度傳感器管理服務時間自動機模型

值得注意的是，在云端溫度傳感器管理服務模型中，將c>10作為進入故障狀態(tài)的守衛(wèi)約束，而不是run狀態(tài)的不變性約束。這是因為溫度傳感器管理服務建模與溫度傳感器是不同的，溫度傳感器陷入故障狀態(tài)的行為與其時鐘計數(shù)器無關(guān)。因此在圖3和圖10對于溫度傳感器的建模中，進入故障狀態(tài)是無條件的。但是云端溫度傳感器管理服務則不同，故考慮溫度傳感器管理服務的實現(xiàn)方式：定義一個時鐘從服務開始工作的時候計時，如果接收到溫度傳感器發(fā)送的消息，就把時鐘歸零；實現(xiàn)一個守衛(wèi)進程來實時監(jiān)測時鐘計數(shù)器的取值，當發(fā)現(xiàn)其計數(shù)值大于10的時候，就使得服務展示溫度傳感器故障狀態(tài)。重點在于，當服務進入故障狀態(tài)的一瞬間，必然有時鐘計數(shù)器計數(shù)結(jié)果大于10。因此c>10是云端溫度傳感器服務進入故障狀態(tài)的必要條件，所以將c>10作為守衛(wèi)約束更加準確。

5.1.4溫度感知系統(tǒng)模型組裝

按照夏季參數(shù)，將圖8所示的空氣溫度物理環(huán)境模板初始化為空氣溫度時間自動機模型；按照每10個時間單位將圖10所示溫度傳感器物理實體模板進行溫度感知創(chuàng)建時間自動機模型；最后將圖11所示的溫度感知云端服務時間自動機模型組裝起來形成物聯(lián)網(wǎng)系統(tǒng)時間自動機網(wǎng)絡，如圖12所示。在這個物聯(lián)網(wǎng)系統(tǒng)中，接入3個溫度傳感器，在對大規(guī)模性的實際系統(tǒng)建模時可以接入更多，只要為溫度傳感器多聲明一個實例并接入物聯(lián)網(wǎng)系統(tǒng)時間自動機網(wǎng)絡即可。

圖12 溫度感知服務物聯(lián)網(wǎng)系統(tǒng)時間自動機模型組裝

5.2 溫度感知物聯(lián)網(wǎng)系統(tǒng)模型驗證

5.2.1溫度感知系統(tǒng)模型仿真

通過UPPAAL的仿真工具驗證了物聯(lián)網(wǎng)系統(tǒng)時間自動機模型具有正確的感知溫度的功能。如圖13所示，當溫度傳感器進行溫度感知的時候，空氣物理環(huán)境的溫度SummarAir.temperature就被賦值給系統(tǒng)全局變量X。此時在“使能遷移”的視圖[17]中，只能繼續(xù)進行溫度發(fā)送這一唯一的格局變換。當執(zhí)行完溫度發(fā)送的格局變換時，空氣物理環(huán)境的溫度就被賦值到云端溫度感知服務的Manager.temp中(被物聯(lián)網(wǎng)系統(tǒng)采集感知)，如圖14所示，由此證明了此物聯(lián)網(wǎng)系統(tǒng)能夠有效感知溫度。

圖13 溫度傳感器感知空氣溫度

圖14 溫度傳感器發(fā)送溫度到云服務

5.2.2溫度感知系統(tǒng)模型驗證

通過UPPAAL的驗證器來驗證所設計的溫度感知物聯(lián)網(wǎng)系統(tǒng)具有動態(tài)性和容錯性。本文期望所有傳感器都可以進入故障狀態(tài)，用UPPAAL的驗證語言表述為：

E〈〉Sensor1.fault

這里只給出了傳感器1的驗證表達式，傳感器2和傳感器3完全類似。

為了體現(xiàn)系統(tǒng)具有不會死鎖的系統(tǒng)活性，將期望只要任意一個傳感器還在運行，溫度感知系統(tǒng)就不會陷入死鎖，使用UPPAAL的驗證語言表述為：

A[](Sensor1.run or Sensor2.run or Sensor3.run)

imply not deadlock

為了體現(xiàn)系統(tǒng)具有容錯性，將期望只要傳感器不全部發(fā)生故障，溫度管理服務就處于正常狀態(tài)，UPPAAL驗證語言表述為：

A[]not (Sensor1.fault and Sensor2.fault and

Sensor3.fault) imply Manager.run

將上述3條驗證語言表述輸入驗證器，使用3.5節(jié)中介紹的方法進行模型檢測，檢測的結(jié)果，如圖15所示。證明了此溫度感知的物聯(lián)網(wǎng)系統(tǒng)具有動態(tài)性和容錯性，且具有不會死鎖的系統(tǒng)活性。

圖15 溫度感知虛擬實體服務模型檢測

6 結(jié) 語

時間自動機建模與模型檢測是驗證物聯(lián)網(wǎng)系統(tǒng)設計正確性的重要方法。本文從時間自動機的理論、時間自動機建模工具的層面上，結(jié)合物聯(lián)網(wǎng)溫度感知系統(tǒng)的建模實踐，對使用時間自動機進行物聯(lián)網(wǎng)系統(tǒng)的建模方法、模型仿真和模型檢測方法以及建模時容易陷入的誤區(qū)進行了比較完整和詳細的論述，為使用時間自動機進行物聯(lián)網(wǎng)系統(tǒng)建模的建模者和研究者提供了一些比較完善的經(jīng)驗和一個很好的建模參考。

未來可研究如何將時間自動機理論和建模方法應用到物聯(lián)網(wǎng)系統(tǒng)和物理信息融合系統(tǒng)的建模中，從而豐富時間自動機的建模應用面，積累更多的時間自動機建模經(jīng)驗。

還可研究如何更好地利用物聯(lián)網(wǎng)系統(tǒng)時間自動機模型，比如怎樣將時間自動機中描繪的時鐘屬性約束和格局變換轉(zhuǎn)換為軟件工程中可實現(xiàn)編碼的方法，而后在構(gòu)件運行平臺和代碼生成工具的支持下實現(xiàn)物聯(lián)網(wǎng)系統(tǒng)資源的自動組裝和系統(tǒng)服務代碼的直接生成，從而縮小物聯(lián)網(wǎng)系統(tǒng)時間自動機模型到系統(tǒng)實現(xiàn)之間的距離，提高物聯(lián)網(wǎng)系統(tǒng)建設的效率，降低物聯(lián)網(wǎng)系統(tǒng)的實現(xiàn)成本。