區(qū)域控制器移動授權(quán)的統(tǒng)一建模語言（UML）建模與驗證

王 露 王長林

（西南交通大學(xué)信息與科學(xué)技術(shù)學(xué)院，610031，成都∥第一作者，碩士研究生）

區(qū)域控制器移動授權(quán)的統(tǒng)一建模語言（UML）建模與驗證

王 露 王長林

（西南交通大學(xué)信息與科學(xué)技術(shù)學(xué)院，610031，成都∥第一作者，碩士研究生）

探討了基于通信的列車控制（CBTC）系統(tǒng)中區(qū)域控制器（ZC）子系統(tǒng)不同運營場景下移動授權(quán)的生成過程。采用統(tǒng)一建模語言（UML），與CBTC中列車運行控制的特殊要求相結(jié)合，以規(guī)范ZC子系統(tǒng)實現(xiàn)的過程和改善系統(tǒng)的開發(fā)效率。通過UML建模直觀展現(xiàn)系統(tǒng)的結(jié)構(gòu)，檢查系統(tǒng)完整性，并完成該系統(tǒng)模型的仿真驗證。

基于通信的列車控制；區(qū)域控制器；移動授權(quán)；統(tǒng)一建模語言建模；模型驗證

First-author's addressSchool of Computer Science and Technology，Southwest Jiaotong University，610031，Chengdu，China

基于通信的列車控制（CBTC）系統(tǒng)用于控制城市軌道交通列車的運行。其區(qū)域控制器（ZC）子系統(tǒng)為每列車分配一個移動授權(quán)（MA），控制列車在管轄范圍內(nèi)安全行駛。因此，MA的實現(xiàn)是ZC子系統(tǒng)的核心部分所在，也是ZC存在的根本目的［1］。本文通過對ZC子系統(tǒng)移動授權(quán)生成進(jìn)行統(tǒng)一建模語言（Unified Modeling Language，簡為UML）建模，在模型邏輯完備性分析的基礎(chǔ)上驗證模型的正確性，進(jìn)而從開發(fā)初期發(fā)現(xiàn)設(shè)計中可能存在的隱患和漏洞。同時，模型的規(guī)范化減少了系統(tǒng)設(shè)計和代碼實現(xiàn)之間的隨意性［2-3］。

1 移動授權(quán)的計算

1.1 區(qū)域控制器系統(tǒng)結(jié)構(gòu)

ZC作為城市軌道交通列車防護(hù)必不可少的軌旁設(shè)備，在CBTC系統(tǒng)中需要與如圖1所示的子系統(tǒng)進(jìn)行交互。其中，數(shù)據(jù)通信系統(tǒng)（DCS）通過以太網(wǎng)的接入為CBTC設(shè)備提供內(nèi)外部通信功能；列車自動監(jiān)視（ATS）系統(tǒng)提供操作和維護(hù)功能，為列車安排運行計劃表，并且匯總提供有關(guān)CBTC設(shè)備、CBTC系統(tǒng)控制下的車輛和軌旁設(shè)備的信息；計算機(jī)聯(lián)鎖（CIL）子系統(tǒng)保證基本的列車進(jìn)路設(shè)置功能，以及與軌旁設(shè)備（如站臺屏蔽門、計軸設(shè)備、緊急制動按鈕等）的接口；區(qū)域控制器從CIL和車載設(shè)備獲得所有軌旁設(shè)備的安全輸入信息及列車識別和位置接收信息，實現(xiàn)線路上所有列車的管理并向每列車發(fā)送移動授權(quán)。

1.2 移動授權(quán)生成原理

為了實現(xiàn)列車安全間隔，CBTC系統(tǒng)通過ZC子系統(tǒng)生成移動授權(quán)。該授權(quán)范圍包括了一段帶有行車許可方向的軌道線路，如圖2所示［4］。ZC在移動授權(quán)的生成過程中每次為列車計算授權(quán)時，需要明確授權(quán)方向、授權(quán)起點和授權(quán)終點這三個要素。

移動授權(quán)的生成過程需要各個系統(tǒng)的互相配合。首先，ATS提供進(jìn)路請求和列車的實際位置，報告給ZC的授權(quán)處理單元；其次，CIL通過ZC請求進(jìn)路，把搜索出來的該進(jìn)路上的設(shè)備狀態(tài)安全性檢查結(jié)果發(fā)送給ZC；最后，進(jìn)路請求經(jīng)過聯(lián)鎖確認(rèn)后，ZC根據(jù)內(nèi)部的動態(tài)線路地圖、障礙物信息和車載信息計算生成移動授權(quán)，并發(fā)送給車載設(shè)備。

圖1 ZC系統(tǒng)外部接口

圖2 移動授權(quán)定義

2 ZC移動授權(quán)UML建模

基于UML模型的系統(tǒng)開發(fā)基于嚴(yán)格的數(shù)學(xué)理論，使系統(tǒng)描述模型化，并在模型的基礎(chǔ)上進(jìn)行設(shè)計、分析和驗證，最終基于模型來實現(xiàn)系統(tǒng)［5-6］。目前，在安全苛求領(lǐng)域，該模型的應(yīng)用越來越廣泛?；赨ML來建立ZC的移動授權(quán)模型，正是應(yīng)用了該建模工具利于交流、不易產(chǎn)生歧義和系統(tǒng)結(jié)構(gòu)直觀可視化等顯著特點?？梢杂美龍D和類圖把ZC系統(tǒng)的靜態(tài)結(jié)構(gòu)元素及其接口、交互關(guān)系等清晰地表現(xiàn)出來，用順序圖和狀態(tài)圖等模型將ZC系統(tǒng)的行為元素及其變化過程展現(xiàn)出來。這對代碼開發(fā)具有重要的指導(dǎo)意義。

2.1 ZC運營場景

CBTC系統(tǒng)的控車過程包括了列車上電啟動、列車在CBTC級別下出段、列車在CBTC級別下進(jìn)站、列車在CBTC級別下出站、ZC切換、ZC切換注銷、列車在CBTC級別下折返、列車在CBTC級別下折返注銷（返回車輛段）等運營場景。本文以ZC切換場景建立UML模型，并且實現(xiàn)該模型的功能驗證。

列車在線路上行駛需要從一個ZC控制的區(qū)域到達(dá)另一個ZC的覆蓋區(qū)域。在兩區(qū)域的重疊區(qū)，列車控制權(quán)的切換過程和列車移動授權(quán)的計算應(yīng)該是無縫的，不會對安全行車和效率造成影響。因此，移動授權(quán)計算必須考慮在邊界處列車移動授權(quán)的生成。邊界處場景如圖3所示。

圖3 ZC邊界示意圖

列車需要在切換預(yù)告應(yīng)答器處向管理ZC提出位置報告，以提示ZC列車進(jìn)入邊界區(qū)；ZC從此開始做出一系列措施，保證列車控制權(quán)平滑可靠地移交。

2.2 ZC切換場景UML建模

以圖3的ZC2為例，邊界處列車的運行使得ZC2針對該列車的狀態(tài)變化如圖4所示。

圖4 ZC切換狀態(tài)圖

由圖4可以看出，當(dāng)ZC2接收到ZC1的注銷信息后對列車進(jìn)行正式的接管，進(jìn)入Takeover（接管狀態(tài)）；列車運行到ZC2和ZC3的邊界處，由ZC3發(fā)送一個空的移動授權(quán)給ZC2，ZC2進(jìn)入到Mix MA（交互計算MA狀態(tài)），接收ZC3計算的移動授權(quán)范圍并整合計算出混合移動授權(quán)，發(fā)送給列車，此時的混合移動授權(quán)應(yīng)該是越過ZC2的管轄范圍的；列車尾部通過切換應(yīng)答器后，ZC2進(jìn)入Handover（移交狀態(tài)），根據(jù)列車的位置報告結(jié)束車地通話，注銷該列車信息。其中任何狀態(tài)的轉(zhuǎn)換過程中出現(xiàn)了超時或未知狀態(tài)的變遷，則自動將ZC2的移動授權(quán)計算轉(zhuǎn)入ErrorStatus（失效狀態(tài)），由失效管理單元進(jìn)行處理，完成列車的移動授權(quán)計算。

邊界處計算移動授權(quán)過程可通過順序圖的建立進(jìn)一步展示，如圖5所示。

圖5 ZC切換順序圖

以ZC2為例，CBTC列車在ATP（列車自動防護(hù)）模式下正常運行，到達(dá)ZC2邊界并通過切換預(yù)告應(yīng)答器時，車載設(shè)備發(fā)送位置信息給ZC2，ZC2的列車管理單元對列車位置信息進(jìn)行處理確定列車到達(dá)切換點，將切換申請發(fā)送給移動授權(quán)計算單元進(jìn)行處理。移動授權(quán)計算單元獲得申請后立即和ZC3溝通，發(fā)送移交列車預(yù)告信息和列車進(jìn)路請求信息。ZC3接收到ZC2的進(jìn)路申請后，結(jié)合其管轄范圍內(nèi)聯(lián)鎖系統(tǒng)的信息，生成其管轄范圍的移動授權(quán)范圍并且發(fā)還給ZC2。ZC2根據(jù)ZC3提供的移動授權(quán)許可，將兩區(qū)域的授權(quán)終點混合計算，生成新的移動授權(quán)范圍。ZC2將混合計算的移動授權(quán)發(fā)送給車載設(shè)備，直至列車最大安全前端越過切換點。一旦列車最大前端越過切換點，車載設(shè)備將只接收ZC2傳遞的終止會話信息。ZC2接收到列車最小安全末端越過切換點的位置報告后，切斷與車載設(shè)備的通信，此時列車的控制權(quán)將由ZC3接替；ZC2列車管理模塊將刪除該列車的相關(guān)信息；ZC2將車載設(shè)備已經(jīng)與其注銷的信息循環(huán)發(fā)送給ZC3，直至得到ZC3接管列車的回復(fù)。一旦ZC2接收到ZC3的確認(rèn)接管信息，兩ZC間將終止會話。至此，ZC切換的移動授權(quán)計算過程完畢。

3 ZC切換模型的授權(quán)生成仿真驗證

由所建模型可以確認(rèn)移動授權(quán)所需要的類及其關(guān)系，對應(yīng)關(guān)系清晰，代碼編寫有序。以圖5為例，模型代碼化過程如圖6所示。圖6中，順序圖的方框中包含了切換過程所涉及的對象及其所屬類，左邊有每個類的函數(shù)和變量構(gòu)成。根據(jù)該結(jié)構(gòu)，就能夠在設(shè)計初期明確代碼的構(gòu)成框架，進(jìn)而從類、函數(shù)及關(guān)鍵變量逐層遞進(jìn)，明確系統(tǒng)實現(xiàn)所需要的代碼結(jié)構(gòu)。同時，每個對象的生命線上涉及的操作進(jìn)一

步交代了相關(guān)函數(shù)需要完成的動作，以MACacu類為例，邊界處移動授權(quán)的計算過程需要完成兩個ZC的移動授權(quán)的信息整合工作，從而輸出MixMA的范圍。該動作在順序圖中清晰展現(xiàn)，對代碼具有清晰的指導(dǎo)意義。結(jié)合所建立的模型，邏輯不完善、狀態(tài)變化不正確等問題會從直觀簡潔的模型圖暴露出來，從而可在設(shè)計初始階段避免很多錯誤，減少后續(xù)開發(fā)測試的工作量。ZC切換模型的代碼實現(xiàn)結(jié)果如圖7所示。

圖6 模型代碼化

圖7 模型功能驗證

在ZC邊界上，列車運行到切換點時進(jìn)入邊界處的移動授權(quán)處理，為了使仿真結(jié)果更為形象，在移動授權(quán)的生成過程中，每個ZC計算的移動授權(quán)都有自己特有的顏色以示區(qū)別。仿真圖中，邊界處列車的移動授權(quán)呈現(xiàn)兩種色彩，兩部分移動授權(quán)整合起來又使得MA整體連續(xù)，由此可以明確MA是由兩個ZC分別計算以后混合生成的。代碼完美實現(xiàn)了模型定義的功能，ZC在邊界處生成的MA保證了控制列車連續(xù)平穩(wěn)地越過邊界。

4 結(jié)語

本文應(yīng)用UML實現(xiàn)了ZC移動授權(quán)模型的生成和驗證。通過模型與代碼間的對應(yīng)關(guān)系實現(xiàn)模型和代碼的邏輯一致。UML模型將模型設(shè)計人員與代碼實現(xiàn)人員之間的溝通規(guī)范化，避免了以往進(jìn)行系統(tǒng)設(shè)計時出現(xiàn)的隨意性和個人理解差異性。結(jié)果表明，運用UML建立的模型使得系統(tǒng)在設(shè)計階段就更為具體精確；同時，建模工具Rational Rose在模型的構(gòu)造上結(jié)合代碼實現(xiàn)的框架，將UML模型映射到代碼的實現(xiàn)過程上，對代碼的編寫具有指導(dǎo)意義，從而實現(xiàn)模型的功能驗證。

［1］ 毛保華.城市軌道交通［M］.北京：科學(xué)出版社，2001.

［2］ 劉敏，金茂忠，劉超.基于UML活動圖模型生成測試場景的設(shè)計［J］.計算機(jī)工程與應(yīng)用，2002（12）：122.

［3］ Schmuller J.UML基礎(chǔ)、案例與應(yīng)用［M］.李虎，趙龍剛，譯.北京：人民郵電出版社，2004.

［4］ 耿鵬.基于安全狀態(tài)機(jī)的RBC系統(tǒng)行車許可模塊的建模與驗證［D］.北京：北京交通大學(xué)，2009.

［5］ 楊柳倩，張友鵬.基于UML與有色Petri網(wǎng)的RBC切換場景的建模方法研究［J］.計算機(jī)測量與控制，2010，20（4）：1116.

［6］ 楊旭文.基于UML的CBTC系統(tǒng)區(qū)域控制器的建模與安全性驗證［D］.北京：北京交通大學(xué)，2008.

Establishment and Verification of UML Model Based on Limit Movement Authority of ZCSystem

Wang Lu，Wang Changlin

The generative process of movement authority under different operation scenes of ZC system is discussed，which is based on metro CBTC system.UML is combinedwith special requirements of CBTC train operation to realize the specificationsin ZC system process and improve the efficiency of its development.Through UML modeling，the system structure is demonstrated directly，the system integrity can be inspected and the system model be validated by simulation.

communication based train control（CBTC）；zone controller（ZC）；limit movement authority；unified modeling language（UML）model establishment；model verification

U 231.6

2012-11-26）