區域控制器移動授權的統一建模語言（UML）建模與驗證

王 露 王長林

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

區域控制器移動授權的統一建模語言（UML）建模與驗證

王 露 王長林

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

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

基于通信的列車控制；區域控制器；移動授權；統一建模語言建模；模型驗證

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

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

1 移動授權的計算

1.1 區域控制器系統結構

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

1.2 移動授權生成原理

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

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

圖1 ZC系統外部接口

圖2 移動授權定義

2 ZC移動授權UML建模

基于UML模型的系統開發基于嚴格的數學理論，使系統描述模型化，并在模型的基礎上進行設計、分析和驗證，最終基于模型來實現系統［5-6］。目前，在安全苛求領域，該模型的應用越來越廣泛。基于UML來建立ZC的移動授權模型，正是應用了該建模工具利于交流、不易產生歧義和系統結構直觀可視化等顯著特點。可以用例圖和類圖把ZC系統的靜態結構元素及其接口、交互關系等清晰地表現出來，用順序圖和狀態圖等模型將ZC系統的行為元素及其變化過程展現出來。這對代碼開發具有重要的指導意義。

2.1 ZC運營場景

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

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

圖3 ZC邊界示意圖

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

2.2 ZC切換場景UML建模

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

圖4 ZC切換狀態圖

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

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

圖5 ZC切換順序圖

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

3 ZC切換模型的授權生成仿真驗證

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

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

圖6 模型代碼化

圖7 模型功能驗證

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

4 結語

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

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

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

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

［4］ 耿鵬.基于安全狀態機的RBC系統行車許可模塊的建模與驗證［D］.北京：北京交通大學，2009.

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

［6］ 楊旭文.基于UML的CBTC系統區域控制器的建模與安全性驗證［D］.北京：北京交通大學，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）