高 昕

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

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

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

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

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

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

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

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

1.2 通信流程分析

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

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

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

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

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

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

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

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

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

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

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

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

圖2 節(jié)能燈的時(shí)間自動(dòng)機(jī)模型

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

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

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

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

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

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

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

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

圖3 監(jiān)測(cè)站機(jī)通信的時(shí)間自動(dòng)機(jī)模型

此通信模型中有bool變量和int 2個(gè)時(shí)鐘變量，另外還有一個(gè)全局變量FrameIndex，用于在2個(gè)模型之間傳遞幀序號(hào)。各個(gè)變量所表示意義見(jiàn)表2。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 結(jié)語(yǔ)

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

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

［1］曾欣.淺談微機(jī)監(jiān)測(cè)系統(tǒng)在信號(hào)設(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í)時(shí)系統(tǒng)模型驗(yàn)證［J］.計(jì)算機(jī)應(yīng)用，2004，9(9):129.