王海峰 楊旭文 劉 朔 劉 超

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

1 研究背景

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

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

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

2 ZC系統(tǒng)

ZC系統(tǒng)是CBTC系統(tǒng)中的地面列車自動(dòng)防護(hù)子系統(tǒng)，負(fù)責(zé)所轄區(qū)域內(nèi)所有列車運(yùn)行的安全。ZC系統(tǒng)是安全完整性等級(jí)要求最高的子系統(tǒng)之一，對(duì)系統(tǒng)安全軟件的設(shè)計(jì)開發(fā)要求極為苛刻。

2.1 亦莊線項(xiàng)目概況

亦莊線是連接北京市中心城和亦莊新城的軌道交通線路，如圖1所示。全線設(shè)置6座設(shè)備集中站、6個(gè)ZC系統(tǒng)，初期配置23組列車的車載設(shè)備，是國(guó)產(chǎn)CBTC系統(tǒng)的首次運(yùn)用。亦莊線起點(diǎn)位于宋莊路與石榴莊路交叉口南側(cè)，全線共設(shè)車站14座，其中地下車站6座、高架車站8座。全線換乘車站共5座在宋家莊站與M5、M10換乘，在舊宮站及榮京東街站與L5換乘，在經(jīng)海路站與M12換乘，在亦莊火車站與京津城際及S6換乘?？刂浦行脑O(shè)在小營(yíng)，備用控制中心設(shè)在車輛段信號(hào)樓內(nèi)。全線設(shè)置宋家莊停車場(chǎng)和亦莊車輛段。

圖1 北京地鐵亦莊線線路

2.2 ZC系統(tǒng)體系結(jié)構(gòu)

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

在系統(tǒng)開發(fā)中，ZC系統(tǒng)采用了2取2雙版本安全軟件容錯(cuò)結(jié)構(gòu)，如圖2所示。ZC系統(tǒng)的雙版本代碼基于同一個(gè)詳細(xì)設(shè)計(jì)，采用兩種不同的方式進(jìn)行開發(fā)，一種為傳統(tǒng)的手工編寫代碼的開發(fā)方式，另一種為基于SCADE模型開發(fā)的方式，通過(guò)比較雙版本軟件的運(yùn)行結(jié)果來(lái)輸出最終結(jié)果。

圖2 ZC系統(tǒng)雙版本容錯(cuò)結(jié)構(gòu)

3 ZC系統(tǒng)建模方法

基于SCADE對(duì)ZC系統(tǒng)進(jìn)行建模，主要分為數(shù)據(jù)流圖和安全狀態(tài)機(jī)。兩套機(jī)制都建立在嚴(yán)格的數(shù)學(xué)模型基礎(chǔ)之上，具有嚴(yán)格的數(shù)學(xué)語(yǔ)義，能夠保證設(shè)計(jì)模型的精確性、完整性、一致性和無(wú)二義性。作為ZC系統(tǒng)的核心功能，移動(dòng)授權(quán)計(jì)算以及列車管理在控車過(guò)程中發(fā)揮了關(guān)鍵作用，ZC系統(tǒng)其他功能模塊的實(shí)現(xiàn)都會(huì)依托于這兩個(gè)功能模塊?？紤]移動(dòng)授權(quán)計(jì)算著重于邏輯處理，選擇數(shù)據(jù)流圖予以實(shí)現(xiàn);而列車管理主要涉及狀態(tài)跳轉(zhuǎn)，選擇安全狀態(tài)機(jī)予以實(shí)現(xiàn)。

3.1 MA 計(jì)算

移動(dòng)授權(quán)是指車載VOBC按照給定的運(yùn)行方向被授權(quán)進(jìn)入和通過(guò)一個(gè)特定的軌道區(qū)段(見圖3)，它在每個(gè)通信周期前動(dòng)態(tài)計(jì)算生成。系統(tǒng)執(zhí)行移動(dòng)授權(quán)，以維持安全的列車間隔，并通過(guò)聯(lián)鎖提供防護(hù)。

圖3 移動(dòng)授權(quán)原理

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

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

3.2 列車管理

區(qū)域控制器處理的主要對(duì)象是在區(qū)域控制器管轄范圍內(nèi)的列車。根據(jù)列車在ZC范圍內(nèi)的不同行為，可以將列車劃分為不同狀態(tài);按照不同狀態(tài)，ZC將會(huì)對(duì)列車進(jìn)行不同處理，以滿足列車當(dāng)前狀態(tài)的需求。

圖4 MA計(jì)算模型主節(jié)點(diǎn)

不同狀態(tài)的列車之間存在相互轉(zhuǎn)換的關(guān)系(見圖5)。當(dāng)列車在ZC管轄范圍內(nèi)滿足一定條件時(shí)，可以從一個(gè)狀態(tài)轉(zhuǎn)換至另一個(gè)狀態(tài);ZC通過(guò)對(duì)列車實(shí)施狀態(tài)跳轉(zhuǎn)控制，完成對(duì)管轄范圍內(nèi)列車的管理工作。

圖5 列車狀態(tài)轉(zhuǎn)移

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

在建立數(shù)據(jù)流圖與安全狀態(tài)機(jī)的模型后，可以將兩套模型的開發(fā)機(jī)制融合在一起，將數(shù)據(jù)流圖模型的嵌套在狀態(tài)機(jī)中，以實(shí)現(xiàn)混合系統(tǒng)的開發(fā)。

4 系統(tǒng)安全性保障方法

圖6 列車管理狀態(tài)機(jī)模型

在完成模型建立工作后，需從安全角度對(duì)所建立的模型進(jìn)行測(cè)試及驗(yàn)證，以保證基于模型開發(fā)的ZC系統(tǒng)的安全性及可靠性。SCADE軟件提供模型覆蓋率功能和形式驗(yàn)證功能來(lái)完成對(duì)所建立模型的驗(yàn)證，前者能夠?qū)δＰ偷耐陚涑潭冗M(jìn)行定量評(píng)估，后者則基于嚴(yán)格的數(shù)學(xué)推理過(guò)程，是被廣泛認(rèn)可的驗(yàn)證方式。

4.1 模型覆蓋率

利用模型覆蓋率的分析功能，可以根據(jù)預(yù)定義或自定義的覆蓋率準(zhǔn)則，分析仿真場(chǎng)景在模型中的覆蓋程度，并能指明未覆蓋的路徑。當(dāng)覆蓋率未達(dá)到要求時(shí)，很有可能會(huì)暴露開發(fā)過(guò)程中的諸多問(wèn)題，如需求錯(cuò)誤、模型設(shè)計(jì)錯(cuò)誤等。

針對(duì)ZC系統(tǒng)的不同功能模塊，設(shè)計(jì)了一系列的仿真場(chǎng)景，通過(guò)基于模型的覆蓋率分析，直觀地展現(xiàn)測(cè)試的效果(見圖7)。通過(guò)不同顏色的顯示，可以直觀地看出哪些模塊單元部件已經(jīng)充分測(cè)試，哪些還沒有被徹底測(cè)試。在分析過(guò)程中，發(fā)現(xiàn)問(wèn)題并解決問(wèn)題，直至系統(tǒng)達(dá)到完備。

圖7 模型覆蓋率分析

4.2 形式驗(yàn)證

模擬仿真和模型覆蓋率分析能夠在一定程度上測(cè)試系統(tǒng)模型是否實(shí)現(xiàn)所期望的功能，但并不能保證系統(tǒng)滿足所有的安全性要求。

借助于形式驗(yàn)證功能，可以借助形式驗(yàn)證工具，對(duì)ZC系統(tǒng)進(jìn)行自動(dòng)化的驗(yàn)證過(guò)程(見圖8)。由于是基于嚴(yán)格的數(shù)學(xué)推理過(guò)程，因而保證了該驗(yàn)證過(guò)程是詳盡、可信的。形式驗(yàn)證不需要借助測(cè)試用例，只需模型在描述安全性要求和建立一個(gè)“特性觀察器”之后，即可自動(dòng)驗(yàn)證模型的安全性。如果模型是安全的，它能給出一個(gè)安全的證明;如果模型是不安全的，它能給出一個(gè)反例來(lái)幫助糾錯(cuò)?？梢姡问津?yàn)證在很大程度上保證了目標(biāo)系統(tǒng)的安全性。對(duì)于ZC系統(tǒng)中的核心功能(如MA計(jì)算)，采用形式驗(yàn)證能夠有效地保障系統(tǒng)安全。

圖8 ZC系統(tǒng)形式驗(yàn)證

5 結(jié)語(yǔ)

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

［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.