基于UPPAAL的列車自動(dòng)防護(hù)系統(tǒng)形式化建模與驗(yàn)證

蔣建軍，王長(zhǎng)林

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

基于UPPAAL的列車自動(dòng)防護(hù)系統(tǒng)形式化建模與驗(yàn)證

蔣建軍，王長(zhǎng)林

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

本文分析列車自動(dòng)防護(hù)（ATP）系統(tǒng)的結(jié)構(gòu)和功能需求，建立系統(tǒng)的時(shí)間自動(dòng)機(jī)模型，采用UPPAAL模型驗(yàn)證工具對(duì)模型的活性和安全性進(jìn)行驗(yàn)證。結(jié)果表明，采用時(shí)間自動(dòng)機(jī)對(duì)安全苛求實(shí)時(shí)系統(tǒng)進(jìn)行建模與驗(yàn)證，可以有效地保證系統(tǒng)的可靠性和實(shí)時(shí)性。

安全苛求系統(tǒng)；時(shí)間自動(dòng)機(jī)；模型驗(yàn)證；UPPAAL

軌道交通作為旅客出行的首選，其安全性與廣大旅客的生命息息相關(guān)。因此，需要可靠的列車運(yùn)行控制系統(tǒng)保障軌道交通的運(yùn)行安全。列車的安全防護(hù)是由列車自動(dòng)防護(hù)（ATP）系統(tǒng)提供的，研究ATP系統(tǒng)的正確性和安全性具有重要意義。

1 時(shí)間自動(dòng)機(jī)理論和UPPAAL

R.Alur等學(xué)者將時(shí)鐘約束加入到有限狀態(tài)自動(dòng)機(jī)中，提出了時(shí)間自動(dòng)機(jī)理論。時(shí)間自動(dòng)機(jī)可以很好的描述實(shí)時(shí)系統(tǒng)的并發(fā)行為，其模型狀態(tài)添加了時(shí)鐘不變式約束，表明系統(tǒng)停留在此狀態(tài)必須滿足不變式約束。為了滿足系統(tǒng)功能實(shí)時(shí)性的要求，模型中定義了多個(gè)時(shí)鐘，所有時(shí)鐘從模型中的初始狀態(tài)開始同步工作，在狀態(tài)轉(zhuǎn)移上的時(shí)鐘約束滿足時(shí)，系統(tǒng)將執(zhí)行狀態(tài)轉(zhuǎn)移。每個(gè)時(shí)鐘都可以在一個(gè)狀態(tài)轉(zhuǎn)移完成后復(fù)位。

UPPAAL是一種基于時(shí)間自動(dòng)機(jī)理論開發(fā)的模型驗(yàn)證工具，包括編輯器、模擬器、驗(yàn)證器3個(gè)部分。編輯器以有向圖的形式描述實(shí)時(shí)系統(tǒng)的并發(fā)行為，模擬器模擬系統(tǒng)中各個(gè)狀態(tài)的轉(zhuǎn)移過程，驗(yàn)證器使用BNF語言驗(yàn)證系統(tǒng)要求的安全性和活性，從而保證系統(tǒng)的安全性和正確性。復(fù)雜的實(shí)時(shí)系統(tǒng)是由相互通信和同步的多個(gè)子系統(tǒng)組成，UPPAAL使用管道和共享變量來實(shí)現(xiàn)子系統(tǒng)之間的通信和狀態(tài)同步轉(zhuǎn)移。UPPAAL是描述安全苛求實(shí)時(shí)系統(tǒng)比較理想的工具，本文將采用UPPAAL對(duì)ATP超速防護(hù)系統(tǒng)進(jìn)行建模與驗(yàn)證。

2 基于時(shí)間自動(dòng)機(jī)的ATP系統(tǒng)的建模與驗(yàn)證

2.1 ATP系統(tǒng)結(jié)構(gòu)及功能需求分析

ATP系統(tǒng)包括車載系統(tǒng)和地面系統(tǒng)兩部分。它的主要功能是處理與列車運(yùn)行安全有關(guān)的任務(wù)，進(jìn)而防護(hù)列車的運(yùn)行安全。ATP系統(tǒng)的地面設(shè)備和車載設(shè)備通過無線通信雙向傳遞行車信息。地面設(shè)備接收從車載設(shè)備傳遞過來的列車實(shí)時(shí)運(yùn)行速度和位置信息，根據(jù)這些信息以及線路數(shù)據(jù)等生成移動(dòng)授權(quán)并發(fā)送給車載設(shè)備；車載設(shè)備接收到移動(dòng)授權(quán)后，根據(jù)移動(dòng)授權(quán)和列車速度、位置、臨時(shí)限速、線路數(shù)據(jù)等生成列車速度防護(hù)曲線，從而完成列車安全追蹤及超速防護(hù)。ATP系統(tǒng)能夠防護(hù)車門和屏蔽門的開關(guān)，保證旅客的上下車安全。其中ATP車載設(shè)備組成如圖1所示。

圖1 車載系統(tǒng)結(jié)構(gòu)圖

ATP車載系統(tǒng)主要功能：

（1）超速防護(hù)功能：當(dāng)列車實(shí)際運(yùn)行速度接近列車最高限制速度時(shí)，司機(jī)顯示屏發(fā)出警告，提醒司機(jī)列車即將超速，要求司機(jī)制動(dòng)減速，在司機(jī)未能實(shí)施制動(dòng)的情況下，ATP系統(tǒng)啟動(dòng)常用制動(dòng)裝置使列車減速；當(dāng)列車實(shí)際運(yùn)行速度超過列車最高限制速度時(shí)，ATP系統(tǒng)實(shí)施緊急制動(dòng)迫使列車停車，在列車停車后緊急制動(dòng)緩解。

（2）防止列車溜滑功能：列車停車后，如果出現(xiàn)溜滑移動(dòng)的情況，ATP系統(tǒng)實(shí)施緊急制動(dòng)。

（3）車門、屏蔽門開關(guān)防護(hù)功能：車站停車后，在ATP系統(tǒng)的監(jiān)控下司機(jī)或者ATO系統(tǒng)才能執(zhí)行車門和屏蔽門開關(guān)的動(dòng)作，以此來保證乘客的上下車安全。

（4）其它功能：自動(dòng)補(bǔ)償輪徑磨損；故障自診斷及發(fā)出報(bào)警，記錄司機(jī)操作信息、運(yùn)行狀態(tài)信息和設(shè)備工作狀況等信息。

2.2 基于UPPAAL的建模

根據(jù)系統(tǒng)的需求分析，采用時(shí)間自動(dòng)機(jī)模型對(duì)ATP超速防護(hù)系統(tǒng)進(jìn)行形式化設(shè)計(jì)建模。整個(gè)系統(tǒng)建立6個(gè)時(shí)間自動(dòng)機(jī)模型，分別是Speedsupervision（速度監(jiān)督）時(shí)間自動(dòng)機(jī)，ATPInterface（接口）時(shí)間自動(dòng)機(jī)，CPU（微機(jī)處理）時(shí)間自動(dòng)機(jī)，TODShow（司機(jī)顯示）時(shí)間自動(dòng)機(jī)，Brake（制動(dòng)）時(shí)間自動(dòng)機(jī)，Drag（牽引）時(shí)間自動(dòng)機(jī)。它們之間通過管道進(jìn)行通信，每個(gè)時(shí)間自動(dòng)機(jī)加以時(shí)間約束。系統(tǒng)的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型如圖2，圖3和圖4所示。

圖2 接口和牽引模塊時(shí)間自動(dòng)機(jī)模型

圖3 司機(jī)顯示和微機(jī)處理模塊時(shí)間自動(dòng)機(jī)模型

圖4 速度監(jiān)督和制動(dòng)模塊時(shí)間自動(dòng)機(jī)模型

建立的列車超速防護(hù)系統(tǒng)的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型實(shí)現(xiàn)功能：

（1）Speedsupervision向CPU發(fā)出速度請(qǐng)求，CPU計(jì)算列車當(dāng)前運(yùn)行速度和限制速度的差，并將結(jié)果發(fā)送給Speedsupervision。

（2）當(dāng)列車當(dāng)前限制速度與當(dāng)前運(yùn)行速度之差小于0 km/h時(shí)，表明當(dāng)前運(yùn)行速度超過限制速度，Speedsupervision通過ATPInterface給BE發(fā)送一個(gè)緊急制動(dòng)命令，BE在收到命令后的100 ms內(nèi)執(zhí)行緊急制動(dòng)。待緊急制動(dòng)完成后，BE給ATPInterface發(fā)送反饋消息，通知Speedsupervision解除緊急制動(dòng)命令。

（3）當(dāng)列車當(dāng)前限制速度與當(dāng)前運(yùn)行速度之差大于0 km/h而小于4 km/h時(shí)，Speedsupervision通過ATPInterface給BE發(fā)送一個(gè)常規(guī)制動(dòng)命令，BE在收到命令后的150 ms內(nèi)執(zhí)行常規(guī)制動(dòng)。待制動(dòng)完成后， BE給ATPInterface發(fā)送反饋消息，通知Speedsupervision解除常規(guī)制動(dòng)命令。

（4）當(dāng)列車當(dāng)前限制速度與運(yùn)行速度之差大于4 km/h而小于10 km/h時(shí)，Speedsupervision通過ATPInterface給TODShow發(fā)送輸出報(bào)警命令，TODShow在收到命令后的200 ms內(nèi)向司機(jī)輸出報(bào)警命令。待TODShow正確輸出報(bào)警命令后，將反饋一個(gè)消息給ATPInterface，通知Speedsupervision解除報(bào)警命令。

從問卷的調(diào)查數(shù)據(jù)來看，廬山西海的游客主要集中于廬山西海及周邊地區(qū)，省內(nèi)外的游客較少，這也是影響廬山西?？驮吹囊粋€(gè)重要原因。

（5）當(dāng)列車當(dāng)前限制速度與當(dāng)前運(yùn)行速度之差大于10 km/h時(shí)，Speedsupervision會(huì)通知ATPInterface，要求ATPInterface發(fā)送一個(gè)牽引命令給Drag，而Drag則必須在250 ms內(nèi)完成列車牽引加速。Drag會(huì)發(fā)送一個(gè)反饋消息給ATPInterface，通知Speedsupervision解除牽引加速命令。

3 模型的仿真和驗(yàn)證

模型建立完成后，UPPAAL模擬器可以模擬時(shí)間自動(dòng)機(jī)模型中各個(gè)狀態(tài)的轉(zhuǎn)移情況。把相關(guān)的性質(zhì)查詢語言輸入到驗(yàn)證器中，可以對(duì)超速防護(hù)系統(tǒng)的安全性和活性進(jìn)行驗(yàn)證。

3.1 活性驗(yàn)證

Speedsupervision.WaitDif-->Cpu.ComputeDif當(dāng)速度監(jiān)督模塊發(fā)出速度差計(jì)算后，CPU計(jì)算速度差。

Speedsupervision.WaitBrake-->Brake. BrakeApplied 當(dāng)速度監(jiān)督模塊發(fā)出常規(guī)制動(dòng)命令后，制動(dòng)裝置實(shí)施常用制動(dòng)。

Speedsupervision.WaitEmerge-->Brake. EmergeApplied 當(dāng)速度監(jiān)督模塊發(fā)出緊急制動(dòng)命令后，制動(dòng)裝置實(shí)施緊急制動(dòng)。

Speedsupervision.WaitWarnB-->TODShow. WarnDisplayed當(dāng)速度監(jiān)督模塊發(fā)出報(bào)警命令后，司機(jī)顯示屏輸出報(bào)警顯示。

Speedsupervision.WaitDrag-->Drag. DragApplied當(dāng)速度監(jiān)督模塊發(fā)出牽引命令后，牽引裝置實(shí)施牽引。

在UPPAAL的驗(yàn)證器中執(zhí)行上述程序，得到具體的系統(tǒng)活性驗(yàn)證結(jié)果如圖5所示。

從圖5中可以得到速度監(jiān)督模塊發(fā)出速度差計(jì)算后，CPU計(jì)算速度差；速度監(jiān)督模塊發(fā)出常規(guī)制動(dòng)命令后，制動(dòng)裝置實(shí)施常用制動(dòng)；速度監(jiān)督模塊發(fā)出緊急制動(dòng)命令后，制動(dòng)裝置實(shí)施緊急制動(dòng)；速度監(jiān)督模塊發(fā)出報(bào)警命令后，司機(jī)顯示屏輸出報(bào)警顯示；速度監(jiān)督模塊發(fā)出牽引命令后，牽引裝置實(shí)施牽引。結(jié)果顯示各個(gè)狀態(tài)之間是可達(dá)的，系統(tǒng)的功能需求可以滿足。

3.2 安全性驗(yàn)證

執(zhí)行程序得到具體的系統(tǒng)安全性驗(yàn)證結(jié)果如圖6所示。

圖6 系統(tǒng)安全性驗(yàn)證結(jié)果

結(jié)果顯示系統(tǒng)無死鎖，處理器在20 ms內(nèi)完成速度計(jì)算，報(bào)警命令在200 ms內(nèi)輸出，制動(dòng)裝置在150 ms內(nèi)實(shí)施常規(guī)制動(dòng)，在100 ms內(nèi)實(shí)施緊急制動(dòng)，牽引裝置在250 ms內(nèi)實(shí)施牽引等要求滿足，表明系統(tǒng)是安全的。

圖5 系統(tǒng)活性驗(yàn)證結(jié)果

4 結(jié)束語

本文分析了列車自動(dòng)防護(hù)系統(tǒng)的結(jié)構(gòu)和功能需求，采用UPPAAL工具對(duì)系統(tǒng)進(jìn)行建模和驗(yàn)證，使用規(guī)范的BNF查詢語言驗(yàn)證了系統(tǒng)功能的安全性和受限活性。時(shí)間自動(dòng)機(jī)是描述和分析安全苛求實(shí)時(shí)系統(tǒng)的一種有效手段，是保障實(shí)時(shí)系統(tǒng)正確性和可靠性的重要途徑。

[1]唐 濤，郜春海，李開成，燕 飛.基于通信的列車運(yùn)行控制技術(shù)發(fā)展戰(zhàn)略探討[J].都市快軌交通，2005，18（6）.

[2] 周清雷，姬莉霞，王艷梅.基于UPPAAL的實(shí)時(shí)系統(tǒng)模型驗(yàn)證[J].計(jì)算機(jī)應(yīng)用，2004，24（9）.

[3] 燕 飛.軌道交通列車運(yùn)行控制系統(tǒng)的形式化建模和模型檢驗(yàn)方法研究[D].北京：北京交通大學(xué)，2006.

[4] 林瑜綺.城市軌道交通信號(hào)設(shè)備[M].北京：中國(guó)鐵道出版社，2006.

[5] 劉傳會(huì)，張廣泉.一種基于時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)的實(shí)時(shí)系統(tǒng)形式化驗(yàn)證方法[J].蘇州大學(xué)學(xué)報(bào)，2008，24（1）：35-40.

責(zé)任編輯 陳 蓉

UPPAAL based modeling for Train Automatic Protection System

JIANG Jianjun, WANG Changlin
( School of Information Science and Technology, Chengdu 610031, China )

This paper analyzed the structure and functional requirements of Train Automatic Protection(ATP) System, set up a timed automata model, activity and safety of the model was verif i ed by using the UPPAAL model verif i cation tool. The results showed that, using timed automata to model and analyze the safety critical real-time systems, could provide effective guarantee for the real-time and reliability of the System.

Safety Critical System; timed automata; model validation; UPPAAL

U284.48∶TP39

A

1005-8451（2014）08-0042-04

2014-02-17

蔣建軍，在讀碩士研究生；王長(zhǎng)林，教授。