基于模型的CBTC區域控制系統安全軟件開發

王海峰 楊旭文 劉 朔 劉 超

(北京交通大學電子信息工程學院 北京 100044)

1 研究背景

近年來，隨著軌道交通的蓬勃發展，為確保列車運行安全和提高運輸效率，基于通信的列車運行控制(communication based train control，CBTC)系統［1］已成為發展方向。CBTC系統通過高精度的列車定位和連續的車地通信技術，提供更精確的列車安全間隔控制和速度防護，最大限度地提高列車運行效率。CBTC是典型的具有SIL4等級要求的高安全系統，伴隨著功能的不斷增強，系統對軟件的依賴性越來越強。在傳統的軟件開發方法中，系統的設計過程多利用自然語言表達，易引起理解上的歧義，對系統設計的分析驗證更多地依賴于人工方式，很難保證設計的正確性，對系統功能的測試需要在開發周期的后期進行，一旦發現錯誤，修正的成本極其昂貴。所以，傳統軟件開發方法已不能很好地應對CBTC開發所面臨的挑戰。

基于模型系統開發(model-based development，MBD)方法的出現［2-4］，引起了安全關鍵領域系統開發方式的變革。這種方法基于嚴格的數學理論，使系統描述模型化，在模型的基礎上進行設計、分析和驗證，最終基于模型來實現系統。目前，在安全苛求領域，基于模型的開發方法發展比較迅速，出現了諸如Matlab-Simulink/Stateflow、UML、SCADE 的開發工具［4-7］。20 世紀80年代，SCADE在Lustre同步模型語言的基礎上被開發用來進行航空系統的設計，90年代推廣應用到安全關鍵軟件開發領域，它具有面向模型的圖形用戶接口、動態仿真和系統狀態分析的功能，并且支持連續或離散時間的線性和非線性系統。

下面結合北京地鐵亦莊線CBTC系統的研究項目，以區域控制(zone controller，ZC)系統為例，介紹基于SCADE模型的CBTC系統安全苛求軟件開發方法。

2 ZC系統

ZC系統是CBTC系統中的地面列車自動防護子系統，負責所轄區域內所有列車運行的安全。ZC系統是安全完整性等級要求最高的子系統之一，對系統安全軟件的設計開發要求極為苛刻。

2.1 亦莊線項目概況

亦莊線是連接北京市中心城和亦莊新城的軌道交通線路，如圖1所示。全線設置6座設備集中站、6個ZC系統，初期配置23組列車的車載設備，是國產CBTC系統的首次運用。亦莊線起點位于宋莊路與石榴莊路交叉口南側，全線共設車站14座，其中地下車站6座、高架車站8座。全線換乘車站共5座在宋家莊站與M5、M10換乘，在舊宮站及榮京東街站與L5換乘，在經海路站與M12換乘，在亦莊火車站與京津城際及S6換乘。控制中心設在小營，備用控制中心設在車輛段信號樓內。全線設置宋家莊停車場和亦莊車輛段。

圖1 北京地鐵亦莊線線路

2.2 ZC系統體系結構

ZC系統運行于2取2乘2安全計算機平臺，通過以太網與其他部分進行信息交互，從總體上劃分為列車狀態信息管理、設置與處理移動授權(moving athority，MA)、強制命令與輔助功能、數據庫版本比較、故障處理以及為系統提供維護診斷信息等幾大功能模塊。ZC系統對管轄范圍內的列車進行管理，根據列車位置信息，計算生成移動授權，并輔助聯鎖等設備完成列車的定位和室外設備的控制，并周期性地與車載設備(VOBC)、聯鎖設備(CI)、列車自動監控設備(ATS)、數據存儲單元(DSU)系統進行信息交互，監控通信情況，實時更新管轄范圍內的設備運行等信息，并作為控制列車運行的因素。

在系統開發中，ZC系統采用了2取2雙版本安全軟件容錯結構，如圖2所示。ZC系統的雙版本代碼基于同一個詳細設計，采用兩種不同的方式進行開發，一種為傳統的手工編寫代碼的開發方式，另一種為基于SCADE模型開發的方式，通過比較雙版本軟件的運行結果來輸出最終結果。

圖2 ZC系統雙版本容錯結構

3 ZC系統建模方法

基于SCADE對ZC系統進行建模，主要分為數據流圖和安全狀態機。兩套機制都建立在嚴格的數學模型基礎之上，具有嚴格的數學語義，能夠保證設計模型的精確性、完整性、一致性和無二義性。作為ZC系統的核心功能，移動授權計算以及列車管理在控車過程中發揮了關鍵作用，ZC系統其他功能模塊的實現都會依托于這兩個功能模塊。考慮移動授權計算著重于邏輯處理，選擇數據流圖予以實現;而列車管理主要涉及狀態跳轉，選擇安全狀態機予以實現。

3.1 MA 計算

移動授權是指車載VOBC按照給定的運行方向被授權進入和通過一個特定的軌道區段(見圖3)，它在每個通信周期前動態計算生成。系統執行移動授權，以維持安全的列車間隔，并通過聯鎖提供防護。

圖3 移動授權原理

移動授權在每個周期內更新，全部為安全信息，其組成可以劃分為ZC發送給車載VOBC的移動授權限制、移動授權范圍內包含的所有軌旁設備狀態、由于運營需要設置的臨時限速等影響列車行車安全的信息。在生成移動授權的過程中，ZC系統會處理很多種類的障礙物，從中選取符合條件的、能夠作為列車此周期運行終點的障礙物。終點障礙物既有可能是靜態障礙物，如道岔、進路終點等，又有可能是動態障礙物，如前方列車等。列車的移動授權會有規律、周期性地重建。

按照MA計算步驟，將模型劃分為MA初始化節點、遍歷通信車節點、遍歷非通信車節點等部分，通過各部分相互間的數據流向組成MA計算整體模型(見圖4)。MA初始化結果作為是否繼續計算MA的判斷依據，遍歷通信車節點判斷所處理列車前方是否包含通信列車，遍歷非通信節點判斷所處理列車前方是否包含非通信列車。

3.2 列車管理

區域控制器處理的主要對象是在區域控制器管轄范圍內的列車。根據列車在ZC范圍內的不同行為，可以將列車劃分為不同狀態;按照不同狀態，ZC將會對列車進行不同處理，以滿足列車當前狀態的需求。

圖4 MA計算模型主節點

不同狀態的列車之間存在相互轉換的關系(見圖5)。當列車在ZC管轄范圍內滿足一定條件時，可以從一個狀態轉換至另一個狀態;ZC通過對列車實施狀態跳轉控制，完成對管轄范圍內列車的管理工作。

圖5 列車狀態轉移

基于SCADE軟件，采用狀態機建模(見圖6)方式，實現列車管理功能。首先定義模型層次，將所有列車狀態抽象劃分為正常狀態與故障狀態。正常狀態包含列車正常行駛過程中可能經歷的全部狀態，其中初始狀態被設置為狀態機模型的起始端。處于正常狀態中的各個列車狀態通過一系列的變遷約束條件相互關聯，一旦條件滿足，則狀態轉換會被馬上觸發。當ZC判斷出列車發生故障時，狀態機內層將會終止，正常狀態直接轉換至故障狀態。

在建立數據流圖與安全狀態機的模型后，可以將兩套模型的開發機制融合在一起，將數據流圖模型的嵌套在狀態機中，以實現混合系統的開發。

4 系統安全性保障方法

圖6 列車管理狀態機模型

在完成模型建立工作后，需從安全角度對所建立的模型進行測試及驗證，以保證基于模型開發的ZC系統的安全性及可靠性。SCADE軟件提供模型覆蓋率功能和形式驗證功能來完成對所建立模型的驗證，前者能夠對模型的完備程度進行定量評估，后者則基于嚴格的數學推理過程，是被廣泛認可的驗證方式。

4.1 模型覆蓋率

利用模型覆蓋率的分析功能，可以根據預定義或自定義的覆蓋率準則，分析仿真場景在模型中的覆蓋程度，并能指明未覆蓋的路徑。當覆蓋率未達到要求時，很有可能會暴露開發過程中的諸多問題，如需求錯誤、模型設計錯誤等。

針對ZC系統的不同功能模塊，設計了一系列的仿真場景，通過基于模型的覆蓋率分析，直觀地展現測試的效果(見圖7)。通過不同顏色的顯示，可以直觀地看出哪些模塊單元部件已經充分測試，哪些還沒有被徹底測試。在分析過程中，發現問題并解決問題，直至系統達到完備。

圖7 模型覆蓋率分析

4.2 形式驗證

模擬仿真和模型覆蓋率分析能夠在一定程度上測試系統模型是否實現所期望的功能，但并不能保證系統滿足所有的安全性要求。

借助于形式驗證功能，可以借助形式驗證工具，對ZC系統進行自動化的驗證過程(見圖8)。由于是基于嚴格的數學推理過程，因而保證了該驗證過程是詳盡、可信的。形式驗證不需要借助測試用例，只需模型在描述安全性要求和建立一個“特性觀察器”之后，即可自動驗證模型的安全性。如果模型是安全的，它能給出一個安全的證明;如果模型是不安全的，它能給出一個反例來幫助糾錯。可見，形式驗證在很大程度上保證了目標系統的安全性。對于ZC系統中的核心功能(如MA計算)，采用形式驗證能夠有效地保障系統安全。

圖8 ZC系統形式驗證

5 結語

筆者結合北京地鐵亦莊線的科研項目，介紹了一種基于模型的CBTC區域控制ZC系統的安全關鍵軟件開發方法，給出了系統的容錯結構，闡述了ZC系統的建模方法和安全性保障措施。亦莊線已于2010年12月30日正式開通運營，系統安全、穩定。結果表明，基于模型系統開發具有如下優點:一是利用嚴格的形式化模型手段描述系統的功能，可使系統設計更為精確;二是模型能夠充分地刻畫系統的行為，能夠更加完備地分析驗證系統的設計;三是給設計人員提供了在系統開發早期進行安全性分析驗證的手段，可以從根本上提高軟件的安全性，降低開發成本。

［1］IEEE STD 1474.1—2004 IEEE standard for communicationsbased train control(CBTC)performance and functional requirements［S］.New York:IEEE Vehicular Technology Society，2005.

［2］Henriksson A，A?man U，Hunt J.Improving software quality in safety-criticalapplications by model-driven verification［J］.Electronic Notes in Theoretical Computer Science，2005，133(31):101-117.

［3］Mohagheghi P，Dehlen V，Neple T.Definitions and approaches to model quality in model-based software development-review of literature［J］.Information and Software Technology，2009，51(12):1646-1669.

［4］Giese H，Henkler S.A survey of approaches for the visual model-driven development of next generation software-intensive systems［J］.Journal of Visual Languages and Computing，2006，17(6):528-550.

［5］Abdulla P A，Deneux J，Stalmarck G，et al.Designing safe，reliable systems using SCADE［C］//Proceedings of ISOLA’04.Springer-Verlag，2004.

［6］Faber J，Meyer R.Model checking data-dependent real-time properties of the European Train Control System［C］//IEEE Conferences on Formal Methods in Computer Aided Design.2006:76-77.

［7］Pretschner A，L?tzbeyer H，Philipps J.Model based testing in incremental system development［J］.Journal of Systems and Software，2004，70(3):315-329.