楊艷艷，王 祺，柴 銘，3

（1．北京城市軌道交通咨詢有限公司，北京 100068；2．北京交通大學(xué)電子信息工程學(xué)院，北京 100044；3．軌道交通運(yùn)行控制系統(tǒng)國家工程研究中心，北京 100044）

1 概述

近年來城市軌道交通取得了飛速發(fā)展。全自動(dòng)運(yùn)行（FAO）是進(jìn)一步解決高速、高密度城市軌道交通安全、高效、節(jié)能、靈活運(yùn)輸?shù)闹匾侄?，是目前城市軌道交通的重要發(fā)展方向。

FAO系統(tǒng)是一種在基于通信的列車運(yùn)行控制系統(tǒng)（CBTC）上將列車駕駛員/調(diào)度員執(zhí)行的工作由自動(dòng)化、智能化的設(shè)備所替代的控制系統(tǒng)。其優(yōu)勢(shì)主要表現(xiàn)為：通過減少人因影響提高系統(tǒng)的安全性和可靠性；提高系統(tǒng)運(yùn)行效率及列車運(yùn)行準(zhǔn)點(diǎn)率和舒適度；降低系統(tǒng)整體能耗；降低系統(tǒng)全生命周期成本。

與CBTC系統(tǒng)相比，F(xiàn)AO系統(tǒng)更加智能，軟件承擔(dān)的安全功能及處理的異常場景更為復(fù)雜，系統(tǒng)組件間以及和人員、環(huán)境之間的交互更加復(fù)雜。此外，對(duì)于FAO系統(tǒng)而言，由于軟件承擔(dān)了更多的功能，減弱了司機(jī)在系統(tǒng)失效時(shí)的防護(hù)作用，給行車安全帶來了新的挑戰(zhàn)。

目前已有EN 50128和EN 50129等鐵路控制與防護(hù)標(biāo)準(zhǔn)規(guī)范軌道交通系統(tǒng)不同安全級(jí)別(SIL0～SIL4)的軟件設(shè)計(jì)與測試，尤其是對(duì)于高安全性功能（SIL3和SIL4）強(qiáng)制要求使用形式化方法保障安全性。但是，由于FAO系統(tǒng)涉及計(jì)算、通信與控制這3個(gè)方面的高頻實(shí)時(shí)協(xié)作，其系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)異常復(fù)雜，傳統(tǒng)的形式化驗(yàn)證方法存在狀態(tài)空間爆炸問題。

為解決上述問題，本文基于一種運(yùn)行時(shí)驗(yàn)證的形式化方法，通過構(gòu)建形式化監(jiān)控器實(shí)現(xiàn)對(duì)FAO系統(tǒng)運(yùn)行時(shí)行為的實(shí)時(shí)驗(yàn)證，預(yù)測列車運(yùn)行危險(xiǎn)并施實(shí)報(bào)警，將系統(tǒng)導(dǎo)向安全側(cè)。相比于傳統(tǒng)的形式化驗(yàn)證，該方法可降低計(jì)算復(fù)雜度，為FAO系統(tǒng)的實(shí)驗(yàn)室完備驗(yàn)證提供有效手段，以保證系統(tǒng)安全。

2 FAO的運(yùn)行時(shí)驗(yàn)證系統(tǒng)

2.1 運(yùn)行時(shí)驗(yàn)證系統(tǒng)框架

運(yùn)行時(shí)驗(yàn)證系統(tǒng)框架如圖1所示。該系統(tǒng)與FAO系統(tǒng)并行運(yùn)行，實(shí)時(shí)預(yù)測FAO系統(tǒng)的運(yùn)行行為。運(yùn)行時(shí)驗(yàn)證系統(tǒng)中包含列車控制模型，根據(jù)列車運(yùn)行時(shí)行為計(jì)算模型中列車未來所有可能行為的可達(dá)集，進(jìn)而通過判斷可達(dá)集是否滿足安全約束，實(shí)現(xiàn)對(duì)列車運(yùn)行危險(xiǎn)的預(yù)測。

圖1 運(yùn)行時(shí)驗(yàn)證系統(tǒng)框架Fig.1 Framework of runtime verification system

2.2 FAO系統(tǒng)運(yùn)行控制模型

運(yùn)行時(shí)驗(yàn)證系統(tǒng)的核心是參數(shù)化模型，該模型為參數(shù)化混成自動(dòng)式，是列車運(yùn)行控制行為的形式化描述。該模型如圖2所示。

該模型包含4個(gè)狀態(tài)，分別代表牽引（ACC）、惰行（COA）、常用制動(dòng)（SB）和緊急制動(dòng)（EB）。狀態(tài)間通過列車的速度、位置關(guān)系實(shí)施狀態(tài)遷移。上述關(guān)系通過狀態(tài)遷移條件描述，當(dāng)列車的速度位置滿足遷移條件時(shí)，則發(fā)生狀態(tài)遷移。由于緊急在停車前無法緩解，因而該狀態(tài)只有遷入而無法遷出。列車的運(yùn)行行為由狀態(tài)中的流條件（Flow）描述，即?=v,v˙ =a-w(s,v,a,w分別代表列車走行距離、速度、加速度和阻力)。

在實(shí)際應(yīng)用中，不同線路中列車擁有不同的阻力，且不同移動(dòng)授權(quán)條件下列車的遷移、制動(dòng)速度位置關(guān)系亦有所不同，因而模型采用參數(shù)化建模方法，模型參數(shù)每周期根據(jù)車載運(yùn)行時(shí)數(shù)據(jù)及相關(guān)線路工程數(shù)據(jù)配置，以得到符合列車實(shí)際運(yùn)行狀況的實(shí)例化模型進(jìn)行驗(yàn)證。

模型的參數(shù)依據(jù)列車動(dòng)力學(xué)模型計(jì)算：基于微分方程理論，通過如公式（1） 、（2）所示的列車受力特征及動(dòng)力學(xué)定律模型，描述列車的速度位置約束關(guān)系，從而得到列車運(yùn)行控制形式化模型中的參數(shù)取值。

其中，Se/km代表制動(dòng)距離，b/（N/kN）代表單位制動(dòng)力，w0/（N/kN）代表單位基本阻力，wr/（N/kN）代表單位坡度附加阻力，g為重力加速度（取9.8m/s2），M/t代表列車質(zhì)量，v0/（km/h）代表列車初始速度，ve/（km/h）代表列車經(jīng)過一段制動(dòng)后的速度，φh代表閘瓦換算摩擦系數(shù)，→代表每個(gè)車輪施加的閘瓦力。

2.3 模型可達(dá)集計(jì)算算法

FAO系統(tǒng)形式化模型的可達(dá)集是指所有可能出現(xiàn)的列車速度位置狀態(tài)的集合。對(duì)于一般的混成模型而言，其復(fù)雜度過高會(huì)導(dǎo)致模型無法在合理時(shí)間內(nèi)計(jì)算其完備的執(zhí)行軌跡，因而需進(jìn)一步基于模型的過近似理論，利用多面體（Zonotope）精化模型可達(dá)集以提升列車行為預(yù)測效率。該方法的原理如圖3所示。

圖3 多面體模型可達(dá)集計(jì)算理論Fig.3 Theory of computation of reachable set for polyhedral model

該方法基于對(duì)任意中心狀態(tài)的演化矢量，得到所有可能的下一狀態(tài)。進(jìn)而以下一狀態(tài)為中心狀態(tài)，計(jì)算新的演化矢量。該過程迭代進(jìn)行，直至狀態(tài)不再演化或滿足預(yù)設(shè)的終止條件。

2.4 FAO系統(tǒng)安全約束

FAO系統(tǒng)的頂層危險(xiǎn)為列車超速和越過移動(dòng)授權(quán)終點(diǎn)（EoA）。該危險(xiǎn)有多種致因，包括車載線路坡度計(jì)算錯(cuò)誤、測速測距故障、地面進(jìn)路辦理錯(cuò)誤、移動(dòng)授權(quán)(MA)計(jì)算錯(cuò)誤、臨時(shí)限速未送至車載等。當(dāng)系統(tǒng)出現(xiàn)復(fù)雜的多點(diǎn)故障時(shí)，可能無法保證行車安全。

在運(yùn)行時(shí)驗(yàn)證中，預(yù)測上述危險(xiǎn)的安全約束為：計(jì)算得到的系統(tǒng)可達(dá)集不包含超速或越過EoA的狀態(tài)。這樣，根據(jù)列車當(dāng)前速度位置狀態(tài)，如果驗(yàn)證滿足安全約束，則可認(rèn)為從當(dāng)前狀態(tài)直至停車，在所有可能運(yùn)行工況的情況下，列車不會(huì)出現(xiàn)危險(xiǎn)；反之，則認(rèn)為列車存在危險(xiǎn)的可能。

3 仿真驗(yàn)證

以北京燕房線為例，通過注入故障，驗(yàn)證所提出方法的有效性。

基于上述方法，利用混成自動(dòng)機(jī)模型檢驗(yàn)器SpaceEx開發(fā)了運(yùn)行時(shí)驗(yàn)證系統(tǒng)。該系統(tǒng)獨(dú)立于所監(jiān)視的FAO系統(tǒng)運(yùn)行。在每個(gè)系統(tǒng)控制周期中，監(jiān)視器從不同的子系統(tǒng)接收重要的接口數(shù)據(jù):從相應(yīng)的傳感器接收到列車速度和位置，從ZC接收到EoA位置。運(yùn)行時(shí)驗(yàn)證系統(tǒng)中配置了線路拓?fù)浣Y(jié)構(gòu)，根據(jù)線路拓?fù)浣Y(jié)構(gòu)將列車位置和EoA位置轉(zhuǎn)換為MA長度。在給定MA條件下，計(jì)算EBI和目標(biāo)速度曲線，據(jù)此配置模型參數(shù)。運(yùn)行時(shí)驗(yàn)證系統(tǒng)進(jìn)而調(diào)用SpaceEx來計(jì)算列車速度位置(S,V)可達(dá)集。如果可達(dá)集包含S=MA且V>0的狀態(tài)，則運(yùn)行時(shí)驗(yàn)證系統(tǒng)報(bào)告危險(xiǎn)，表明列車有可能超過EoA。如果可達(dá)集中不包含危險(xiǎn)狀態(tài)，監(jiān)控器報(bào)告安全，表明列車在當(dāng)前運(yùn)行狀態(tài)下沒有潛在的危險(xiǎn)。

3.1 危險(xiǎn)場景設(shè)計(jì)

本文以下述2個(gè)危險(xiǎn)場景為例，通過在FAO仿真平臺(tái)中注入故障，驗(yàn)證所設(shè)計(jì)的運(yùn)行時(shí)驗(yàn)證系統(tǒng)的有效性。

錯(cuò)誤的坡度(IGt)。坡度列車運(yùn)行中一個(gè)重要的附加阻力來源，通過對(duì)FAO系統(tǒng)中坡度數(shù)據(jù)注入故障，導(dǎo)致出現(xiàn)列車越過EoA。

錯(cuò)誤的MA長度(ILMA)。通過不同方式注入錯(cuò)誤MA長度故障，線路數(shù)據(jù)中注入故障、MA長度計(jì)算模塊中注入錯(cuò)誤以及聯(lián)鎖與ZC接口中注入故障，這些錯(cuò)誤導(dǎo)致FAO車載系統(tǒng)依據(jù)錯(cuò)誤的MA行車，最終導(dǎo)致列車越過EoA。

3.2 仿真試驗(yàn)結(jié)果及分析

運(yùn)行時(shí)驗(yàn)證系統(tǒng)的仿真試驗(yàn)結(jié)果如表1所示。

表1 不同場景下的預(yù)測結(jié)果Tab.1 Predicted results in different scenarios

表1中，第一列顯示了評(píng)估的CBTC場景，包括一個(gè)正常的執(zhí)行場景和4個(gè)危險(xiǎn)場景，每個(gè)場景都涉及上述危險(xiǎn)之一。第2～5列為FAO車載運(yùn)行數(shù)據(jù)，其中ST為列車位置，V為列車速度，SEoA為EoA位置，Gt為線路坡度。Pha表示列車運(yùn)行階段，其中Acc、Coa和Bak分別代表加速、惰行和制動(dòng)。ResRV和ResATC分別表示部署運(yùn)行時(shí)驗(yàn)證系統(tǒng)和不部署運(yùn)行時(shí)驗(yàn)證系統(tǒng)的列車運(yùn)行結(jié)果。由于驗(yàn)證需要消耗時(shí)間，當(dāng)列車運(yùn)行狀態(tài)出現(xiàn)危險(xiǎn)時(shí)，監(jiān)控器報(bào)警信息存在延時(shí)。表1中t為運(yùn)行時(shí)驗(yàn)證系統(tǒng)所需的運(yùn)算時(shí)間，SA表示收到報(bào)警信號(hào)時(shí)列車的實(shí)際位置。

在正常的場景，運(yùn)行時(shí)驗(yàn)證系統(tǒng)未給出危險(xiǎn)信號(hào)，表明該系統(tǒng)未發(fā)生誤報(bào)情況。

在IGt場景中，F(xiàn)AO系統(tǒng)使用了錯(cuò)誤線路坡度18‰控制列車運(yùn)行，而實(shí)際線路坡度為-18‰。在該場景中，當(dāng)列車以21.1 m/s的速度行駛至1891.52 m的位置時(shí)，運(yùn)行時(shí)驗(yàn)證系統(tǒng)預(yù)測出危險(xiǎn)（在該狀態(tài)之前，如果列車實(shí)施制動(dòng)則可在EoA前停車）。該狀態(tài)的可達(dá)集如圖4所示，驗(yàn)證時(shí)間為6.03 s，此時(shí)列車已行駛至2018.75 m的位置。

圖4 運(yùn)行時(shí)驗(yàn)證可達(dá)集計(jì)算結(jié)果Fig.4 Calculation result of reachable set of runtime verification

收到危險(xiǎn)信號(hào)開始制動(dòng)，最終在EoA前停車。

在（21.1 m/s，1891.52 m）之后的每個(gè)列車運(yùn)行狀態(tài)，運(yùn)行驗(yàn)證系統(tǒng)均預(yù)測存在危險(xiǎn)。列車最早收到的警報(bào)是當(dāng)列車位置位于1926.1 m和速度21.1 m/s的狀態(tài)下。基于該狀態(tài)運(yùn)行時(shí)驗(yàn)證系統(tǒng)花費(fèi)2.01 s計(jì)算可達(dá)集，列車行駛至1968.45 m時(shí)收到報(bào)警信息并開始實(shí)施制動(dòng)，最終停在EoA之前。系統(tǒng)的運(yùn)行過程如圖5所示。

圖5 運(yùn)行時(shí)驗(yàn)證實(shí)施效果對(duì)比Fig.5 Comparison of implementation results of runtime verification

4 總結(jié)

本文提出了一種面向FAO系統(tǒng)的在線危險(xiǎn)預(yù)測技術(shù)，通過構(gòu)建運(yùn)行時(shí)驗(yàn)證系統(tǒng)實(shí)現(xiàn)對(duì)真實(shí)系統(tǒng)運(yùn)行時(shí)行為的可信性驗(yàn)證。該技術(shù)基于形式化模型，完備的計(jì)算列車從當(dāng)前時(shí)刻至停車時(shí)刻的速度位置狀態(tài)可達(dá)集，進(jìn)而實(shí)現(xiàn)對(duì)行車危險(xiǎn)的預(yù)測。實(shí)驗(yàn)結(jié)果表明,本文所述技術(shù)可有效預(yù)測FAO系統(tǒng)運(yùn)行危險(xiǎn)，避免了傳統(tǒng)形式化方法對(duì)大規(guī)模系統(tǒng)的可驗(yàn)證性問題，為系統(tǒng)的實(shí)驗(yàn)室安全性驗(yàn)證提供一種有效手段。