基于時間自動機的監測系統通信流程建模分析

高 昕

(國電南瑞科技股份有限公司，211800，南京∥工程師)

鐵路信號設備是重要的鐵路行車設備，加強對鐵路信號設備運用狀態監督和管理，有助于提高鐵路信號設備的工作效率和穩定性，進而減少故障發生率。

通過建模能夠模擬系統的運行，建模是分析、研究系統性能的有效手段。在建立系統模型時做必要的抽象和假設，對系統的主要功能和特性進行合理說明和設計，忽略與研究分析不相關的細節，將有助于突出研究的重點，完成系統重要特性的驗證。

1 軌道電路微機監測系統中的通信協議介紹

軌道電路微機監測系統主要由采集終端、采集處理機及微機監測站機3部分組成。采集終端負責從軌道電路設備采集電壓、電流、頻率以及開關量并定時傳送到采集處理機;采集處理機需要能夠正確地讀取采集終端發送的各種數據信息，包括開關量、模擬量、CAN(網絡)設備狀態及報警信息等，并對信息進行分類處理后發送到監測站機;監測站機用于接收采集處理機發送來的監測信息，對軌道電路的狀態進行實時監測。

1.1 串口通信的數據幀類型

根據通信協議，采集處理機與微機監測站機之間需要用6種類型的數據幀交換(如表1所示)。其中的ACK(通信允許)幀及ZPW_DATA(周期性報文數據)幀是由監測站機發送，其它4種由采集處理機發送給微機監測子系統。

表1 串口數據幀類型

1.2 通信流程分析

按照上述通信格式及通信內容，微機監測站機與采集處理機的數據幀交換流程可簡單概括如下:

(1)監測站機請求與采集處理機通信或通信復位時向采集處理機發送ASK幀;采集處理機接到ASK后，以ASK幀中包含的時間信息校正自己的程序時間，將發送幀序號置1，然后以ACK幀應答。

(2)監測站機接到ACK幀后，表示與采集處理機的連接成功，同時設定面向該連接的定時器。如果2 min沒有接收到采集處理機發送來的任何數據，則重新發送ASK幀。

(3)監測站機10 min向采集處理機發送一次TIME幀，用于校正子系統中采集處理機軟件的程序時間。

(4)采集處理機每分鐘向微機監測站機發送ZPW_DATA數據幀，該數據幀中包括全站的所有數據信息。

(5)微機監測站機接收數據的過程中，若發現了發送序號的不連續跳變，則認為出現了數據丟失，則將缺失的幀序號包含于Resend幀中發向子系統，采集處理機根據該序號重新發送該幀。

(6)當出現報警信息時，采集處理機在發向微機監測站機的ZPW_DATA幀中對某一標志位置1，表示報警信息。微機監測站機接到該報警信息后，向采集處理機發回ZPW_ACK幀。如果采集處理機發送了報警信息幀后沒有收到微機監測站機發來的ZPW_ACK幀回應，則對該報警信息間隔2 s定時重復發送3次。

ZPW－2000A子系統對微機監測站機的通信流程時序如圖1所示。

圖1 采集處理機與監測站機通信時序圖

2 時間自動機及實時系統驗證軟件UPPAAL

自動機理論(Automata Theory)是在開關網絡理論和數理邏輯中圖靈機理論的基礎上形成和發展起來的。現在己經成為研究離散數字系統的功能、結構以及兩者之間關系的有效數學工具，成為理論計算機科學的重要組成部分。

時間自動機是在傳統有限狀態自動機基礎上為遷移添加時鐘約束，為狀態添加不變式約束而得到的。列舉一個可調亮度節能燈的例子來說明時間自動機的模型。假設一個燈泡具有關閉(off)、低亮度(low)和明亮(bright)3個狀態。3個狀態之間的轉換方式是:如果用戶在關閉狀態下按下開關，則燈泡進入低亮度狀態，再按開關則燈泡關閉;但若用戶迅速按下開關兩次，則燈泡變成明亮狀態。其時間自動機的模型如圖2所示。

圖2 節能燈的時間自動機模型

圖2中a)表示節能燈的模型，b)表示用戶按下開關的操作。用戶可以隨機地按下幾次或不按開關。開關按下后，使用通道Press(按)來傳遞同步消息。時鐘變量y用來監測用戶按下開關的間隔頻率為快(y＜5)或慢(y≥5)。

UPPAAL是由丹麥的 Aalborg大學和瑞典的Uppsala大學于1995年聯合開發的一個基于時間自動機的驗證工具，已經在通信協議、多媒體等眾多領域成功應用。它特別適合實時系統的安全性和有界活性的自動驗證，不僅可以有效地發現系統設計中出現的錯誤，而且可以清楚地顯示導致出現錯誤的判定路徑。

UPPAAL的用戶界面包括系統編輯器(system editor)、模擬器(simulator)和驗證器(verifier)3個主要部分。系統編輯器用于創建和編輯要分析的系統，一個系統被描述為一系列過程模板、一些全局聲明、過程分配和一個系統定義。驗證器通過快速搜索系統的狀態空間來檢查時鐘約束和活性，它還為系統要求的規范和文件提供了一個需求規范編輯器。

3 監測系統通信流程的建模

在使用UPPAAL建模時至少需要建立2個模板分別用來代表監測站機的通信模型和采集處理機的通信模型。另外，隨機產生的數據丟幀的情況也使用一個獨立的模板為系統提供隨即命令的發送。

在通信系統模型中，一共涉及9個通道變量，可分為 3 組:① chan ASK，ACK，Resend，TIME，ZPW_ACK，ZPW_DATA;② chan Alarm，DataLost;③broadcast chan AlarmLost。

其中，第一組通道用來模擬通信系統中傳遞的數據幀，比如ASK表示微機監測站機系統向采集處理機發送了ASK幀。第二組和第三組用來模擬報警、數據丟失及報警信息丟失的情況，屬于輔助通道。另外第三組還為廣播通道，可以同時使2個模板同時接收通道命令。

使用UPPAAL軟件對系統進行建模時，需要對系統的各個狀態及功能使用一個位置(Location)來表示。在UPPAAL軟件中建立的微機監測站機通信功能的模型如圖3所示，該圖為UPPAAL軟件界面截圖。

圖3 監測站機通信的時間自動機模型

此通信模型中有bool變量和int 2個時鐘變量，另外還有一個全局變量FrameIndex，用于在2個模型之間傳遞幀序號。各個變量所表示意義見表2。

表2 監測站機模型中的變量名稱及意義

子系統采集處理機模型多數情況下都是接受監測站機發送來的指令，然后按照要求應答。

為采集處理機通信功能建立的時間自動機模型如圖4所示，該圖為UPPAAL軟件界面截圖。

在對子系統采集處理機進行建模分析時，模型中涉及到了3個clock變量、2個int變量及一個bool變量，各個變量所代表的意義見表3。

4 通信模型功能的驗證

使用UPPAAL軟件中的系統驗證功能可以根據輸入的驗證語句進行系統功能的驗證。在UPPAAL軟件中，對性質的驗證使用綠燈表示性質滿足，紅燈表示性質不滿足。同時在驗證窗口的底部，通過中文顯示了某驗證的性質是否滿足。以驗證死鎖為例，性質A［］not deadlock表示系統一定無死鎖，其完全相反的性質為A［］deadlock，表示系統一定存在死鎖。

圖4 采集處理機通信的時間自動機模型

表3 采集處理機模型中的變量名稱及其涵義

在對系統進行建模后，自建了一些簡單的驗證語句，基本上能夠涵蓋了系統的通信功能的驗證。對系統功能驗證的語句如下。

(1)A［］not deadlock 含義:系統模型需要滿足的第一條語句，表示系統在任意狀態位置時不能出現死鎖的情況。若此條件不滿足，則其它的所有驗證都是沒有意義的。

(2)A［］M.GetASK imply S.WaitACK 含義:采集處理機獲取到ASK幀時，暗示監測站機一定在等待ACK幀。

(3)A［］S.SendTIME imply(S.Time600≥600 and S.S_Commok==true) 含義:監測站機系統發送了時間校正TIME幀，一定暗示了通信正常并且已經間隔了10 min。

(4)A ＜ ＞ (S.Time600 ＞ =600 and S.S_Commok==true)imply S.SendTIME 含義:監測站機通信正常狀態每10 min將會發送一次時間校正TIME幀。

(5)S.Time120＞120－ － ＞not S.SendTIME含義:監測站機系統120 s沒有收到數據，一定導致停止發送TIME幀。

(6)A ＜ ＞ A.LostData imply S.LocalIndex+1!=FrameIndex 含義:數據幀的丟失將造成監測站機保存幀序號與發送幀序號的跳變。

(7)A.LostData and S.S_Commok==true－ －＞M.ResendData 含義:監測站機通信正常且出現數據丟失時，將導致采集處理機重發數據。

(8)A［］S.GetAlarm imply not A.LostAlarm含義:監測站機接收到報警信息，暗示一定沒有錯誤或報警丟失。

(9)A.LostAlarm－ － ＞M.ResendALARM 含義:報警信息丟失將導致采集處理機重新發送報警信息。

(10)M.ResendALARM and M.n＞3－ － ＞not M.ALARM 含義:當報警信息已經重發3次后，將導致不再重發該報警。

5 結語

本文在介紹和分析軌道電路微機監測系統中采集處理機與監測站機間的通信協議的基礎上，使用實時系統建模及分析軟件UPPAAL分別建立了采集處理機與微機監測站機之間通信過程的時間自動機模型，將抽象的通信協議形象化。自建的10條的驗證語句，基本上能夠涵蓋了全部的通信功能。這些驗證語句成功通過驗證，標志著模型在功能完整性、正確性及運行無死鎖等方面均達到了協議的要求。

使用UPPAAL軟件提供的驗證功能確保模型功能的正常實現，使模型能夠為軌道電路微機監測系統軟件開發的思路進行指導，規范軟件的模塊化設計，縮短軟件的開發周期，使編制出的軟件盡量減少功能缺陷，滿足功能的需求。

［1］曾欣.淺談微機監測系統在信號設備中的應用［J］.鐵道工程企業管理，2007(2):45.

［2］Aalborg.UPPsala.UPPAAL Help［EB/OL］.(2009 － 10 － 16)［2013 －05 －25］.http://www.uppaal.com.

［3］周清雷.姬莉霞.基于UPPAAL的實時系統模型驗證［J］.計算機應用，2004，9(9):129.