物聯網系統時間自動機建模的研究與應用

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

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

0 引 言

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

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

時間自動機可以直觀地刻畫實時系統與時間有關的行為[8]，是物聯網實時系統進行設計和建模的重要方法。基于時間自動機的理論研究，也產生了許多時間自動機建模和模型檢測工具[9]。

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

1 相關工作

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

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

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

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

2 時間自動機建模理論

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

2.1 屬性變量和屬性約束

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

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

2.2 時鐘變量和時鐘約束

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

2.3 時鐘屬性約束集合

2.4 不變性約束與守衛約束

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

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

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

2.5 時間自動機約束之間的關系

在進行時間自動機物聯網體系結構建模的時候，必須明確時鐘約束與屬性約束、守衛約束與不變性約束之間的關系，在設計時間自動機的約束條件時做到概念清晰。

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

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

圖1 時間自動機中的約束

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

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

對應地，時鐘屬性解釋u滿足守衛時鐘約束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 時間自動機的狀態和格局

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

定義12時間自動機的格局(Status)。一個時間自動機的格局定義為一個二元組〈l,u〉，其中l∈N代表一個位置，u代表此時間自動機時鐘屬性變量集合X下的一個時鐘屬性解釋。可以理解時間自動機的格局為包含某個時鐘屬性解釋的位置，也就是包含了時間和屬性取值的狀態。

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

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

2.9 緊迫狀態與原子狀態

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

2.10 時間自動機網絡

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

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

將2個或者2個以上時間自動機串聯的結果M=A1‖A2‖…‖An,n≥2 稱為時間自動機網絡。

3 時間自動機建模方法

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

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

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

NAir={loop}，lAir0=loop

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

ΣAir={GetAirTemperature}

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

XAir={temperature,inc_clock}

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

IAir={loop→〈inc_clock≤100〉}

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

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

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

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

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

ΣSen={GetAirTemperature},

XSen={sen_clock},

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

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

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

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

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

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

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

4 時間自動機建模工具

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

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

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

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

圖4 UPPAAL編輯器視圖

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

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

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

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

圖6 UPPAAL模擬器視圖

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

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

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

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

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

圖7 UPPAAL驗證器視圖

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

5 物聯網溫度感知系統建模驗證實踐

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

5.1 溫度感知物聯網系統建模

5.1.1空氣物理環境建模

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

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

圖8 使用模板建模空氣溫度時間自動機模型

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

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

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

5.1.2溫度傳感器建模

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

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

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

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

5.1.3云端管理服務建模

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

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

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

5.1.4溫度感知系統模型組裝

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

圖12 溫度感知服務物聯網系統時間自動機模型組裝

5.2 溫度感知物聯網系統模型驗證

5.2.1溫度感知系統模型仿真

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

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

圖14 溫度傳感器發送溫度到云服務

5.2.2溫度感知系統模型驗證

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

E〈〉Sensor1.fault

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

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

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

imply not deadlock

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

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

Sensor3.fault) imply Manager.run

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

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

6 結 語

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

未來可研究如何將時間自動機理論和建模方法應用到物聯網系統和物理信息融合系統的建模中，從而豐富時間自動機的建模應用面，積累更多的時間自動機建模經驗。

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