基于時間自動機的智慧實訓室通信模式研究

黃麗芬

(廣東行政職業學院 實訓中心, 廣東 廣州 510800)

物聯網系統很好地融合了物理世界和信息世界,但物理世界的連續變化和不確定性對物聯網服務和通信有較高的實時性、動態性、可靠性和安全性要求[1-3]。為滿足物聯網通信和服務的穩定性、正確性需求,通信的時間屬性異常重要。目前已有許多學者在進行相關研究,嘗試將時間屬性的約束引入物聯網系統感知和服務過程中[4-7],在系統設計的過程中引入時間自動機的概念,避免產生設計缺陷,提升系統的安全性及正確性。這些研究主要是將時間自動機對接物聯網系統應用服務層進行建模,且止步于模型邏輯論證,但未涉及建模后具體實現。本文嘗試在物聯網系統感知層設備通信模式的設計中加入時間屬性約束機制,探索由各設備自主約束和管理感知層的通信抉擇機制,提出一種基于時間自動機的設備自主管理通信過程的智慧通信模式,并深入研究這一智慧通信模式的具體設計與實現,用以提升智慧實訓室系統通信的智慧性、可靠性、安全性和運行效率。

1 時間自動機的概念

1.1 時間自動機的定義

時間自動機有以下定義[4-9]。

(1) 時鐘約束:一個時鐘變量集X,時鐘約束φ的集合中φ(X)定義為:

φ=x≤c|x≥c|xc|φ1∧φ2

其中c是常量。

(2) 時鐘解釋:時鐘集合X的一個時鐘解釋v給每個時鐘分配一個實數值。即:它是一個從X到非負實數集R的一個映射。X的一個時鐘解釋v滿足x上的一個時鐘約束φ,當且僅當φ=v為真。

(3) 時間自動機:一個六元組A=,其中,L是有窮狀態集合；L0是初始狀態集合；Σ是有窮符號集合；X是有窮時鐘集合；I為狀態節點上的時鐘約束映射,即對L中每個狀態節點指定一個φ(X)中的時鐘約束L→φ(X)；E是轉換集合,有E?L×Σ×2X×φ(X)×L。表示從位置s到位置s′的轉換,輸入狀態為a,φ是X上一個時鐘約束,它達到時轉變發生；λ?X它是復位零值的時鐘集合。

(4) 時間自動機積:表達復雜系統時用多個時間自動機復合組成的時間自動機網絡,即積自動機。設

1.2 感知層通信模式里時間自動機概念

假設在物聯網感知層通信過程中,各感知設備地位均等。各感知設備既可接收數據,也可發送數據,各設備只是在通信模式的類別設計上有所不同。基于時間自動機的通信模式是以時間為軸,根據通信模式規則對各設備數據傳輸動作形成約束,以此支持在各設備間自主、有序地完成通信過程。

在感知層設備通信過程中,系統進行數據傳輸有時間和狀態約束。根據通信過程中設備狀態和約束,定義有連接通信模式的時間自動機模型為Connect_TA= <{ Closed,Idle, Wait,Connecting},{ Closed},{Val_Connect},{n1,n2},CNTAI,CNTAE>,其中有連接時間自動機有Closed、Idle、Wait、Connecting等4個工作狀態集合,分別代表關閉、空閑、傳輸等待(即數據已發送,等待接收端數據確認)、連接中(即連接請求已發送,等待連接確認)。初始狀態為Closed。無連接時間自動機模型為NConnect_TA=<{Closed,Idle,Wait},{Closed},{Val_Connect},{n},NNTAI,NNTAE>,有Closed、Idle、Wait等3個基本工作狀態集合,分別代表關閉、空閑、傳輸等待。n為狀態節點時系統時鐘限制。NNTAI、NNTAE為狀態節點時間自動機時鐘約束關系與狀態轉換關系,后根據通信模式及具體需求進行定義并設計。

在設備的時間自動機通信模式設計中,自動機在同一時刻只能處于一個狀態。當外部觸發事件或時鐘約束發生時,自動機會根據當前規定的時鐘狀態和約束關系轉換至下一狀態,當某一觸發事件或狀態出現異常或時鐘約束溢出時,時間自動機會返回初始狀態,等待下一系列觸發事件的發生。物聯網系統感知層所有通信節點均內置統一設計的通信時間自動機,每種通信機制由對應的時間自動機自主完成約束管理；當前設備受制的通信機制及時間約束屬性,只能對當前設備的通信狀態形成約束。設備通信模式里設計的時間自動機約束機制和時間約束屬性可以根據通信機制的需求統一變換。

2 基于時間自動機的物聯網感知層通信模式

物聯網控制系統常見的通信服務模式主要有:(1)點對多點無連接,多播通信模式；(2)點對域無連接,廣播；(3)點對所有點無連接,系統廣播；(4)點對點無連接；(5)點對點有連接[10-12]。以建立連接與否劃分,可分為有連接通信和無連接通信。其中以點對點有連接通信模式過程最為復雜,可以用于設備參數讀/寫操作、授權管理、密鑰管理等重要功能。

2.1 有連接通信時間自動機模型

點對點有連接通信模式是指傳輸層用戶在點對點連接可使用之前先建立傳輸連接,再傳遞數據；數據傳輸完成后,再釋放連接的通信模式。連接建立過程是:發送端先發送建立連接請求幀,接收端收到請求幀后,分析原語中的目的地址和自身可利用資源情況,如果允許建立連接,接收端就發送連接確認幀,指示發送端與接收端之間連接建立成功。之后,發送端再發送連接數據請求幀,進行數據傳遞,接收端接收完數據后發送數據連接確認信息,在數據傳送完成后再釋放連接,并向接收機發送釋放連接請求幀。有連接點對點通信的工作流程如圖1所示。

圖1 有連接通信的工作流程

有連接通信的輸入事件主要有:

(1) 連接請求(T_connect_req)；

(2) 連接建立指示(T_connect_ind)；

(3) 連接建立響應,連接建立確認(T_connect_con)；

(4) 數據傳遞請求(T_data_req)；

(5) 數據傳遞指示(T_data_ind)；

(6) 數據傳遞確認(T_data_ack)；

(7) 連接釋放請求(T_disconnect_req)；

(8) 連接釋放指示(T_disconnect_ind)。

具體描述如圖2所示:

圖2 有連接通信時間自動機模型

圖2中,T1、T2分別為通信連接最大時間周期、數據處理最大時間周期,具體設計時由兩個時鐘控制來實現,連接超時和確認超時。連接狀態轉換的管理由連接時間自動機完成,數據傳遞確認的管理主要由T1、T2進行約束和管理。連接通信開始運行之時處于Closed狀態,經各事件輸入在Connecting、Idle、Wait狀態中切換。在約定時間內沒有收到對應的連接確認和數據確認幀,可重發數據幀；超出約定時間周期后放棄操作,回到初始Closed狀態。

系統內各設備的最大時鐘周期限制和狀態轉移條件、結果均保持一致,才能保證設備間的連接能有序、可靠完成。另外,時間自動機的程序設計應充分考慮容錯處理問題,系統各狀態持續時間超出時間周期且沒有狀態變化則回歸初始狀態。

2.2 無連接通信時間自動機模型

無連接通信模式是指傳輸層用戶不先建立傳輸通道即進行數據傳輸。無連接通信過程連接簡單,具體數據傳輸過程是:發送端直接發送帶目標地址的數據請求幀,進行數據傳遞,接收端收到數據幀后,分析原語中的目的地址,確認地址無誤后,存儲數據信息和接收數據,完成后發送數據接收確認信息回發送端。無連接通信的工作流程如圖3所示。

圖3 無連接通信的工作流程

無連接通信的輸入事件主要有:數據傳遞請求(T_Data_Req),數據傳遞指示(T_Data_Ind),數據傳遞確認(T_Data_Ack),等。

圖4中,T為設置的數據傳輸超時約束,具體設計時由1個時鐘控制實現。無連接時的狀態轉換管理由無連接時間自動機完成,數據傳遞確認的管理主要由T來約束。無連接通信未開啟之前和開始運行之時,均屬于Closed狀態,經各事件輸入切換狀態在Idle、Wait各狀態中轉換。如果在約定時間內沒有收到來自任一設備的對應數據確認幀,可重發數據幀。重發時間超出約定時間周期后放棄操作,回歸到初始Closed狀態,并向傳遞無連接數據所在網絡發出數據傳輸錯誤提示信號。

圖4 無連接通信時間自動機模型

2.3 模型驗證分析

假設連接確認時鐘參數為100單位,數據確認時間為50單位,系統內各設備設置的主頻相同。模型驗證包括模型邏輯正確性驗證和過程正確性驗證。

邏輯正確性驗證主要是通信死鎖驗證,驗證結果如表1所示。

表1 邏輯正確性驗證

對兩種通信模式主要執行過程進行驗證,驗證結果如表2所示。

表2 執行過程驗證

表1、2中,A[ ]p表示必然的,即所有路徑的所有狀態都滿足p；E< >p表示可能的,即某些路徑中存在狀態滿足p,E< >p為真,當且僅當在轉換系統中從初始狀態s0開始存在一個序列s0→…→p[4-6]。

3 基于時間自動機的智慧通信模式設計

以比較復雜的有連接點對點通信模式為例,介紹基于時間自動機的通信模式設計與實現。

3.1 有連接時間自動機的數據結構

在傳輸層定義時間自動機結構體用以保存連接時間自動機在各個時刻的屬性值,涉及的參數包括:(1)地址參數,用于保存建立連接的接收端或發送端源地址；(2)時間自動機狀態參數,用于保存時間自動機當前狀態屬性值；(3)數據幀下標參數,保存當前數據幀的操作次數,用于管理重接和重發數據幀；(4)時間屬性參數,保存連接時間屬性值和確認時間屬性值,用于管理時間約束情況。

連接時間自動機(Connec_Timer_Object)結構體設計參考如下:

Struct Connec_Timer_Object

{

/* ID is the Serial number of this connect */

Struct Address [ ID]

{

Send_addr； //// Address of Send Target

Rcv_addr； // Address of Receive Target

}

Status[ ID]； // Status of Connect

Struct SeqNoes [ ID]

{

SeqNoSend； //Serial number of Send Data Frame

}

Struct AutoTimer [ ID]

{

ConnectTimer； //Timer for connect overtime

AckTimer； // Timer for acknowlege overtime

}

}

連接時間自動機結構體的各部分值可獨立存取操作,并以下標序號ID來保證整個時間自動機的統一操作。當輸入事件發生時,系統調用連接時間自動機結構體讀取當前狀態參數和時間約束參數,根據約束機制完成操作后向自動機結構體寫屬性值。一次通信事件周期完成后自動設置時間自動機參數置位或清零動作。一個連接通信由單獨的時間自動機管理,使用多個連接可申請多個有連接時間自動機來管理,連接數量受設備存儲空間和處理速度限制。發送端和接收端的連接時間自動機狀態轉移,需機制統一和時間同步才能確保連接通信能有序、穩定、可靠地進行。

3.2 感知層設備通信工作過程

圖5所示為感知層設備通信時各層工作任務和結構的布局。基于時間自動機的通信過程控制和管理主要由鏈路層、網絡層和傳輸層實現,時間自動機的定義和控制主要在傳輸層實現。控制信息存放在升降機中,鏈路層、網絡層和傳輸層根據本層任務可以讀取和寫入控制字段中信息。

鏈路層提供數據幀的差錯檢測功能并實現對數據鏈路地址的識別。接收信息時,它負責從接收緩沖區檢測數據幀的校驗字符,判斷幀的完整性,放棄校驗錯誤或目的地址不屬于本設備的數據幀,對正確接收的數據幀反饋接收正確回復幀,錯誤的幀反饋接收錯誤回復幀,并將接收緩沖區(外部變量表)的數據幀和本層判定寫入的自動機屬性值加載到升降機中,告知網絡層接收處理完成。發送時,它根據幀的任務需求在升降機加載相應類型的地址信息,計算并添加數據幀的校驗字符,形成完整數據幀后復制到發送緩沖區(外部變量表),通知物理層進行發送。發送完成后,處理接收方發送回復幀。如果發送失敗,讀取時間自動機時間限制和發送幀序號完成限定時間內的重發功能。

網絡層實現網絡路由的分配和識別工作,判斷當前數據幀的通信模式,并據此對數據信息進行分服務處理。接收時,它負責從升降機中提取并識別地址類型、路由信息、設備類別、自動機地址屬性等信息,根據識別結果將不同通信模式的數據幀進行分類處理,通知傳輸層進行工作。發送時,它根據通信模式的不同,在升降機中對應位置上添加相應地址類型標識,加載設備路由及設備類別信息,通知鏈路層進行工作。

傳輸層負責分配、識別傳輸層控制字段信息,對屬于不同通信模式的數據信息提供不同的傳輸層原語服務,例如指示、請求、確認等原語。傳輸層支持無連接和有連接等多種通信模式。在接收處理幀時,它從升降機中提取數據幀及自動機控制信息,據此判斷幀的通信模式,響應該模式的指示原語服務,調用應用層的應用服務進行后續處理；在發送封裝幀時,根據應用層應用服務對通信模式的不同需求,響應請求、確認原語,并將數據幀及自動機控制信息封裝進升降機中,通知網絡層進一步封裝加載數據幀信息。

圖5 感知層設備通信各層任務和結構布局

4 應用舉例——智慧實訓室照明子系統

智慧實訓室照明子系統采用EIB通信協議,定義有開關節點設備、被控燈具等設備。以上位機向接收端設備寫地址服務為例來分析基于時間自動機通信模式的實現過程及結果。圖6為寫地址服務流程序列。

圖6 寫地址服務流程序列

寫地址服務可以對接收端的物理地址、組地址表和關聯表信息進行配置。設計測試用例完成對目標程序的測試,從調試窗口察看程序運行過程,比較寫地址操作的執行結果。其中1個測試用例是將0x0001、0x0024、0x0002、0x0003、0x0004等5個地址內容寫入物理地址存儲的內存位置。圖7是寫地址操作時接收和回復數據幀信息。

圖7 數據幀傳輸情況串口監測

根據數據幀往返情況可以看出,發送端與接收端經發送請求、寫地址數據幀請求、數據接收確認后,實現對接收端地址的寫操作,應答幀及時反饋了寫地址的結果。從調試窗口觀察到的時間自動機狀態轉移結果均符合設計要求,在連接或確認超時情形下,能適時正確處理,回到初始狀態。

5 結語

在智慧實訓室感知層通信中應用時間自動機理論并得到驗證。這一研究的結果有助于提升物聯網系統的智慧性、穩定性、可靠性和運行效率。隨著單設備連接自動機數量增多,通信線路上設備并發數增多,系統復雜性也將急劇增加并影響處理速度,通信沖突等情況也有可能出現。在進一步的研究中將繼續深入檢驗和驗證基于時間自動機的通信模式在多連接、多設備并發處理時的狀態執行情況和穩定性。

References)

[1] 黃麗芬,黃大榮,陳迪泉,等.數據驅動的智慧實訓室服務模式設計[J].實驗室研究與探索,2017,36(2):125-130.

[2] 羅國濤,裴廣,鄧祖樸,等.面向物聯網的工作流服務架構模型[J].計算機應用與軟件,2014，31(2):9-13.

[3] 叢新宇,虞慧群.基于實時UML順序圖的物聯網交互模型[J].計算機科學,2014,41(11):79-87.

[4] 李力行,金芝,李戈.基于時間自動機的物聯網服務建模和驗證[J].計算機學報,2011,34(8):1365-1377.

[5] 鄧雪峰,孫瑞志,聶娟,等.基于時間自動機的溫室環境監控的物聯網系統建模[J].農業機械學報,2016,47(7):301-308.

[6] 姬莉霞,馬建紅.基于時間自動機的UML模型轉換與驗證研究[J].鄭州大學學報(理學版),2013,45(1):50-55.

[7] 任龍濤,張超,崔磊,等.基于時間自動機的嵌入式軟件壓縮與驗證[J].計算機工程與設計,2016,37(5):1217-1223.

[8] Alur R, Dill D L. A Theory of Timed Automata[J]. Theoretical Computer Science, 1994, 126(2): 183-235.

[9] Larsen K G,Pettersson P, Wang Y. Uppaal in a nutshell[J]. International Journal on Software Tools for Technology Transfer,1997,1(1):134-152.

[10] 陳迪泉,黃麗芬.談物聯網感知層的技術特征與實現方法[J].智能建筑,2012(9):68-72,75.

[11] 全國工業過程測量和控制標準化技術委員會.控制網絡HBES技術規范 住宅和樓宇控制系統:GB/T20965—2013[S].北京:中國標準出版社,2013.

[12] 徐艷萍.KNX/EIB協議棧的研究與實現[D].合肥:合肥工業大學,2014.