物聯(lián)網(wǎng)系統(tǒng)時(shí)間自動(dòng)機(jī)建模的研究與應(yīng)用

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

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

0 引 言

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

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

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

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

1 相關(guān)工作

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

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

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

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

2 時(shí)間自動(dòng)機(jī)建模理論

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

2.1 屬性變量和屬性約束

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

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

2.2 時(shí)鐘變量和時(shí)鐘約束

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

2.3 時(shí)鐘屬性約束集合

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

時(shí)間自動(dòng)機(jī)引入了位置的概念，時(shí)間自動(dòng)機(jī)的所有位置組成時(shí)間自動(dòng)機(jī)的位置集合N。對(duì)于N中的某個(gè)位置l，可以對(duì)應(yīng)兩種不同形式的約束。

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

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

2.5 時(shí)間自動(dòng)機(jī)約束之間的關(guān)系

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

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

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

圖1 時(shí)間自動(dòng)機(jī)中的約束

2.6 時(shí)鐘屬性映射與滿足約束

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

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

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

2.7 時(shí)間自動(dòng)機(jī)的形式化定義

2.8 時(shí)間自動(dòng)機(jī)的狀態(tài)和格局

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

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

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

從時(shí)間自動(dòng)機(jī)格局變換的定義中可以很容易推導(dǎo)出一個(gè)定理：在時(shí)間自動(dòng)機(jī)中，屬性變量取值的變化只發(fā)生在位置改變的格局變換中，時(shí)間流逝的格局變換不會(huì)造成屬性變量取值的變化。

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

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

2.10 時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)

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

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

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

3 時(shí)間自動(dòng)機(jī)建模方法

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

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

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

NAir={loop}，lAir0=loop

空氣能夠被傳感器感知其溫度狀態(tài)，則空氣時(shí)間自動(dòng)機(jī)與傳感器時(shí)間自動(dòng)機(jī)之間必然有消息傳遞，因?yàn)槭歉兄獪囟?，命名為GetAirTemperature，所以有：

ΣAir={GetAirTemperature}

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

XAir={temperature,inc_clock}

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

IAir={loop→〈inc_clock≤100〉}

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

圖2 空氣溫度時(shí)間自動(dòng)機(jī)模型

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

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

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

ΣSen={GetAirTemperature},

XSen={sen_clock},

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

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

圖3 溫度傳感器時(shí)間自動(dòng)機(jī)模型

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

由于時(shí)間自動(dòng)機(jī)建模分析和時(shí)間自動(dòng)機(jī)形式化表述占用的篇幅過長(zhǎng)，且形式化時(shí)間自動(dòng)機(jī)表述與圖形化時(shí)間自動(dòng)機(jī)表述完全等效，為了節(jié)約篇幅，我們?cè)诤罄m(xù)的時(shí)間自動(dòng)機(jī)建模討論中，不再贅述建模分析和形式化模型表述，而直接給出圖形化形式模型。但這并不意味著時(shí)間自動(dòng)機(jī)理論對(duì)于建模是不重要的。事實(shí)上，時(shí)間自動(dòng)機(jī)理論研究對(duì)于建立時(shí)間自動(dòng)機(jī)模型具有十分重要的意義。

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

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

4 時(shí)間自動(dòng)機(jī)建模工具

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

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

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

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

圖4 UPPAAL編輯器視圖

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

圖5 編輯時(shí)間自動(dòng)機(jī)的位置和邊

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

使用UPPAAL的模擬器界面進(jìn)行時(shí)間自動(dòng)機(jī)模型的仿真。UPPAAL的模擬器界面如圖6所示。

圖6 UPPAAL模擬器視圖

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

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

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

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

使用UPPAAL的驗(yàn)證器界面進(jìn)行時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型性質(zhì)的驗(yàn)證。驗(yàn)證器界面如圖7所示。

圖7 UPPAAL驗(yàn)證器視圖

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

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

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

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個(gè)可變的溫度參數(shù)，只有在系統(tǒng)初始化的時(shí)候，才能確定具體的室內(nèi)和室外溫度。如果室內(nèi)溫度小于室外溫度，則室內(nèi)溫度每隔一定的時(shí)間間隔(時(shí)間間隔可變)，以一定的增量(增量可變)升高，但最高不超過室外溫度。如果室內(nèi)溫度大于室外溫度，則室內(nèi)溫度每隔一定的時(shí)間間隔，以一定的增量減小，但最低不低于室外溫度。室內(nèi)溫度可以被溫度傳感器感知(在UPPAAL建模中體現(xiàn)為信號(hào)的發(fā)送)。

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

圖8 使用模板建模空氣溫度時(shí)間自動(dòng)機(jī)模型

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

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

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

5.1.2溫度傳感器建模

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

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

圖10 溫度傳感器時(shí)間自動(dòng)機(jī)模板

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

5.1.3云端管理服務(wù)建模

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

圖11 溫度傳感器管理服務(wù)時(shí)間自動(dòng)機(jī)模型

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

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

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

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

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

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

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

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

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

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

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

E〈〉Sensor1.fault

這里只給出了傳感器1的驗(yàn)證表達(dá)式，傳感器2和傳感器3完全類似。

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

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

imply not deadlock

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

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

Sensor3.fault) imply Manager.run

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

圖15 溫度感知虛擬實(shí)體服務(wù)模型檢測(cè)

6 結(jié) 語

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

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

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