高 昕

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

鐵路信號設(shè)備是重要的鐵路行車設(shè)備，加強(qiáng)對鐵路信號設(shè)備運(yùn)用狀態(tài)監(jiān)督和管理，有助于提高鐵路信號設(shè)備的工作效率和穩(wěn)定性，進(jìn)而減少故障發(fā)生率。

通過建模能夠模擬系統(tǒng)的運(yùn)行，建模是分析、研究系統(tǒng)性能的有效手段。在建立系統(tǒng)模型時做必要的抽象和假設(shè)，對系統(tǒng)的主要功能和特性進(jìn)行合理說明和設(shè)計，忽略與研究分析不相關(guān)的細(xì)節(jié)，將有助于突出研究的重點(diǎn)，完成系統(tǒng)重要特性的驗(yàn)證。

1 軌道電路微機(jī)監(jiān)測系統(tǒng)中的通信協(xié)議介紹

軌道電路微機(jī)監(jiān)測系統(tǒng)主要由采集終端、采集處理機(jī)及微機(jī)監(jiān)測站機(jī)3部分組成。采集終端負(fù)責(zé)從軌道電路設(shè)備采集電壓、電流、頻率以及開關(guān)量并定時傳送到采集處理機(jī);采集處理機(jī)需要能夠正確地讀取采集終端發(fā)送的各種數(shù)據(jù)信息，包括開關(guān)量、模擬量、CAN(網(wǎng)絡(luò))設(shè)備狀態(tài)及報警信息等，并對信息進(jìn)行分類處理后發(fā)送到監(jiān)測站機(jī);監(jiān)測站機(jī)用于接收采集處理機(jī)發(fā)送來的監(jiān)測信息，對軌道電路的狀態(tài)進(jìn)行實(shí)時監(jiān)測。

1.1 串口通信的數(shù)據(jù)幀類型

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

表1 串口數(shù)據(jù)幀類型

1.2 通信流程分析

按照上述通信格式及通信內(nèi)容，微機(jī)監(jiān)測站機(jī)與采集處理機(jī)的數(shù)據(jù)幀交換流程可簡單概括如下:

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

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

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

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

(5)微機(jī)監(jiān)測站機(jī)接收數(shù)據(jù)的過程中，若發(fā)現(xiàn)了發(fā)送序號的不連續(xù)跳變，則認(rèn)為出現(xiàn)了數(shù)據(jù)丟失，則將缺失的幀序號包含于Resend幀中發(fā)向子系統(tǒng)，采集處理機(jī)根據(jù)該序號重新發(fā)送該幀。

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

ZPW－2000A子系統(tǒng)對微機(jī)監(jiān)測站機(jī)的通信流程時序如圖1所示。

圖1 采集處理機(jī)與監(jiān)測站機(jī)通信時序圖

2 時間自動機(jī)及實(shí)時系統(tǒng)驗(yàn)證軟件UPPAAL

自動機(jī)理論(Automata Theory)是在開關(guān)網(wǎng)絡(luò)理論和數(shù)理邏輯中圖靈機(jī)理論的基礎(chǔ)上形成和發(fā)展起來的?，F(xiàn)在己經(jīng)成為研究離散數(shù)字系統(tǒng)的功能、結(jié)構(gòu)以及兩者之間關(guān)系的有效數(shù)學(xué)工具，成為理論計算機(jī)科學(xué)的重要組成部分。

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

圖2 節(jié)能燈的時間自動機(jī)模型

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

UPPAAL是由丹麥的 Aalborg大學(xué)和瑞典的Uppsala大學(xué)于1995年聯(lián)合開發(fā)的一個基于時間自動機(jī)的驗(yàn)證工具，已經(jīng)在通信協(xié)議、多媒體等眾多領(lǐng)域成功應(yīng)用。它特別適合實(shí)時系統(tǒng)的安全性和有界活性的自動驗(yàn)證，不僅可以有效地發(fā)現(xiàn)系統(tǒng)設(shè)計中出現(xiàn)的錯誤，而且可以清楚地顯示導(dǎo)致出現(xiàn)錯誤的判定路徑。

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

3 監(jiān)測系統(tǒng)通信流程的建模

在使用UPPAAL建模時至少需要建立2個模板分別用來代表監(jiān)測站機(jī)的通信模型和采集處理機(jī)的通信模型。另外，隨機(jī)產(chǎn)生的數(shù)據(jù)丟幀的情況也使用一個獨(dú)立的模板為系統(tǒng)提供隨即命令的發(fā)送。

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

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

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

圖3 監(jiān)測站機(jī)通信的時間自動機(jī)模型

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

表2 監(jiān)測站機(jī)模型中的變量名稱及意義

子系統(tǒng)采集處理機(jī)模型多數(shù)情況下都是接受監(jiān)測站機(jī)發(fā)送來的指令，然后按照要求應(yīng)答。

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

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

4 通信模型功能的驗(yàn)證

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

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

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

在對系統(tǒng)進(jìn)行建模后，自建了一些簡單的驗(yàn)證語句，基本上能夠涵蓋了系統(tǒng)的通信功能的驗(yàn)證。對系統(tǒng)功能驗(yàn)證的語句如下。

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

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

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

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

(5)S.Time120＞120－ － ＞not S.SendTIME含義:監(jiān)測站機(jī)系統(tǒng)120 s沒有收到數(shù)據(jù)，一定導(dǎo)致停止發(fā)送TIME幀。

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

(7)A.LostData and S.S_Commok==true－ －＞M.ResendData 含義:監(jiān)測站機(jī)通信正常且出現(xiàn)數(shù)據(jù)丟失時，將導(dǎo)致采集處理機(jī)重發(fā)數(shù)據(jù)。

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

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

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

5 結(jié)語

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

使用UPPAAL軟件提供的驗(yàn)證功能確保模型功能的正常實(shí)現(xiàn)，使模型能夠?yàn)檐壍离娐肺C(jī)監(jiān)測系統(tǒng)軟件開發(fā)的思路進(jìn)行指導(dǎo)，規(guī)范軟件的模塊化設(shè)計，縮短軟件的開發(fā)周期，使編制出的軟件盡量減少功能缺陷，滿足功能的需求。

［1］曾欣.淺談微機(jī)監(jiān)測系統(tǒng)在信號設(shè)備中的應(yīng)用［J］.鐵道工程企業(yè)管理，2007(2):45.

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

［3］周清雷.姬莉霞.基于UPPAAL的實(shí)時系統(tǒng)模型驗(yàn)證［J］.計算機(jī)應(yīng)用，2004，9(9):129.