CTCS-N等級轉換場景形式化建模與驗證

高卓凡,何 濤,姜 飛,吳永成

(1. 蘭州交通大學 自動化與電氣工程學院,蘭州 730070;2. 甘肅省工業交通自動化工程技術研究中心,蘭州 730070;3. 甘肅省軌道交通信號與控制評測行業技術中心,蘭州 730070)

隨著我國鐵路網不斷向著高效快捷、分布遼闊的方向發展,目前我國在既有線改造及客運專線建設中已使用CTCS-3級(Chinese train control system level three)列控系統。青藏鐵路格拉段于2006年7月開通,其信號系統采用美國通用電氣公司的增強型列控系統(incremental train control system,ITCS),并且通用電氣公司對其安全保障承諾至2024年。針對青藏鐵路存在地理環境惡劣、行車密度低、軌旁維修困難、與標準體系不兼容等缺陷[1],2020年中國國家鐵路集團有限公司組織制定了新型列控系統(Chinese train control system-new,CTCS-N)的技術條件[2]。

CTCS-N系統符合既有CTCS的總體架構,具有無線通信、移動閉塞、列車多源融合定位、取消軌道電路等特點[3]。系統由車載設備和地面設備兩部分組成:車載設備由列尾設備、列車自動防護系統(automatic train protection,ATP)、車載主機構成;地面設備由軌旁設備、列控聯鎖一體化系統(train control center and interlocking integrated system,TIS)、無線閉塞中心(radio block center,RBC)、臨時限速服務器(temporary speed restriction server,TSRS)構成。CTCS-N具有少軌旁、高效率的特點,以車載設備為中心,將列控系統的功能進一步集中到車載設備中[4]。等級轉換場景是車地交互的典型場景,有嚴格的時間約束,對它進行形式化建模不僅可以證明等級轉換的正確性,更可以確定整個車載設備的可靠性[5-6]。

目前針對CTCS-N建模與驗證的研究較少,但是針對CTCS-3的建模與驗證研究已經趨于成熟。大量的研究方法表明,形式化的建模方法更適用于列控系統。形式化建模的方法有著色Petri網(hierarchical coloured petri net,HCPN)[7]、時間Petri網(timed petri net,TPN)、時間自動機(timed automata,TA)等。孫維正等[8]基于統一建模語言(unified modeling language,UML)與層次賦時有色Petri網(hierarchical timed colored petri nets,HTCPN)相結合的方法構建區域控制器(zone controller,ZC)切換場景的模型,并在CPN Tools仿真平臺上進行了驗證;張振海等[9]基于TA對具體場景下CTCS-3系統功能是否符合其系統規范進行建模與驗證,并進行了仿真驗證。其中TA可以刻畫系統的連續時間特性和信息交互特性,并且有專門的驗證工具UPPAAL,所以十分適合列控系統的建模。本文基于時間自動機理論對CTCS-N的等級轉換流程進行建模,并利用UPPAAL進行仿真分析,最后按照正常模式和故障模式下車載設備轉換的功能與性能需求驗證該模型。

1 時間自動機理論及UPPAAL

時間自動機通過在傳統自動機的狀態和變遷中添加時間約束,實現對實時系統進行建模和驗證。時間自動機包含若干個時鐘,系統開始啟動后,這些時鐘以相同的速率運行,并且在任意位置的變遷時鐘都可以進行重置[10]。

時間自動機通常用一個六元組來進行表述,其中:L為有限個位置的集合;L0(L0?L)為模型初始位置的集合;∑為所有事件的集合;X為有限個時鐘的集合;I∶L→Φ(X)表示發生的一個映射,Φ(X)為時鐘X的約束;E為位置變遷的集合,E?L×Φ(X)×∑×2x×L。E中的一個狀態遷移表示輸入a后,系統從s經過φ的觸發變遷到位置s′,其中λ是在遷移過程中進行復位操作的時鐘集合。

對于復雜系統,分別對該系統的子系統進行建模,再將模型組合起來,此時各個子系統的模型存在同步通信的行為,可以用積的形式來描述整個系統[11]。

UPPAAL是一個專門用于實時系統建模和驗證的工具,可以使用建模語言來描述時間自動機的積,各個子系統之間的信息通過全局變量或者同步通道來實現[12]。UPPAAL主要包含三部分:編輯器使用TA語言描述需要建模分析的系統,模擬器利用模型仿真來確認系統模型是不是正確的,驗證器通過搜索系統可以檢查時鐘約束和反應限制性質[13]。UPPAAL驗證器使用快速搜索的方法檢查系統的約束條件以及狀態跳轉,以避免搜索過程中的空間爆炸問題,其中驗證器中的自動機語言(Backus Naur form,BNF)及含義見表1[14-15],其中:A表示“所有”,E表示“存在”,p表示“表達式”。

表1 BNF語法及含義

2 CTCS-N等級轉換場景概述

2.1 CTCS-3到CTCS-N等級轉換場景分析

CTCS-3轉換至CTCS-N的轉換過程分為RBC切換和車載設備等級轉換兩部分,如圖1所示,其中:RBC1表示CTCS-3區域內的RBC(簡稱C3-RBC),RBC2表示CTCS-N區域內的RBC(簡稱CN-RBC),CN-TSRS表示新型列控系統的TSRS。新型列控系統區域內的RBC與相鄰的CTCS-3區域內的RBC應保持連接,以CTCS-3的協議和流程完成列車移交。

圖1 CTCS-3轉換至CTCS-N的示意圖

當列車的行車許可終點到達RBC切換應答器時,C3-RBC發送預告信息給CN-RBC,并申請新型列控系統的進路信息;C3-RBC收到新型列控系統的進路信息后,則發送延長至CN-RBC區域內的行車許可到車載設備;列車安全前端經過TSRS呼叫應答器后,車載設備呼叫CN-TSRS,并且注冊和下載CN-TSRS提供的行車許可;C3-RBC在列車靠近RBC切換應答器時發送RBC切換命令到車載設備;CN-RBC在列車安全前端越過RBC切換應答器后向C3-RBC發送接管信息,車載設備接收CN-RBC的等級轉換命令和行車許可;列車安全后端越過RBC切換應答器后,車載設備中斷與C3-RBC之間的通信;列車越過等級轉換應答器時車載設備自動轉入CTCS-N控車。信息交互順序圖如圖2所示。

圖2 CTCS-3轉換至CTCS-N的信息交互圖

2.2 CTCS-N到CTCS-3等級轉換場景分析

CTCS-N轉換至CTCS-3的轉換過程(見圖3)分為車載等級轉換和RBC切換兩部分。新型列控系統區域內的RBC與相鄰的CTCS-3區域內的RBC應保持連接,以CTCS-3的協議和流程完成列車移交。

圖3 CTCS-N轉換至CTCS-3的示意圖

當列車的行車許可終點到達RBC切換應答器組時,CN-RBC發送列車預告信息至C3-RBC,并且申請進路信息;CN-RBC收到C3-RBC發送的進路信息后,向車載設備發送延長至C3-RBC區域的行車許可;車載設備在列車越過等級轉換應答器后,自動轉換到CTCS-3控車;CN-RBC在接近RBC切換邊界時向車載設備發送RBC切換命令,車載設備與C3-RBC建立通信;車載設備在列車前端越過RBC切換應答器后僅接收C3-RBC的行車許可;車載設備在列車后端越過RBC切換應答器后終止與CN-RBC的通信會話。信息交互順序圖如圖4所示。

圖4 CTCS-N轉換至CTCS-3的信息交互圖

2.3 故障模式下CTCS-3到CTCS-N等級轉換場景分析

根據青藏鐵路新型列控技術規范,CTCS-3轉換至CTCS-N的過程中車載設備故障模式主要有兩種。根據鐵路信號“故障-安全”原則,即當信號設備發生故障后,應以特殊的方式做出反應并導向安全[16]。所以CTCS-3到CTCS-N等級轉換場景在故障模式下導向安全有兩種情況:

1) 列車安全前端越過RBC切換應答器后,車載設備未收到CN-RBC的期望消息,則車載設備仍按C3-RBC的行車許可行車,即列車降級運行,這樣會影響行車效率。

2) 車載設備在移交RBC前僅與C3-RBC通信正常時,車載設備應該重新呼叫CN-RBC,并且完成列車注冊和進路信息的申請。

3 等級轉換場景的模型構建

等級轉換場景的主要研究對象為車載設備、應答器、C3-RBC、CN-RBC、TSRS。

基于UPPAAL構建整個系統的TA模型:TA=Onboard‖Balise‖RBC1‖RBC2‖TSRS,其中:Onboard表示車載設備,Balise表示應答器。在系統模型中,各個子系統之間通過同步通道實現通信,其中:“!”表示發出此信號后轉換發生,“?”表示接收此信號后轉換發生。

設時間自動機的位置集合為L,則L=LOnboard∪LBalise∪LRBC1∪LRBC2∪LTSRS,其中:LOnboard、LBalise、LRBC1、LRBC2、LTSRS分別表示車載設備、應答器、RBC1、RBC2、TSRS的時間自動機模型的非空狀態集。系統的狀態位置集合如下所示:

LOnboard={idle,GetRBC2MA,ConnectCmd,StartConTSRS,Getversion_TSRS,Connectbuild_TSRS,…};

LBalise={idle,sendTSRSCall,sendRBCchange,sendLTO,sendLTA};

LRBC1={idle,ApplyInfo,RecRoute,GetRouteSuc,SendRBC2MA,ApprochRBC,SendRBCcmd,…};

LRBC2={idle,GetPreview,SendRoute,GetconRBC2,Sendversion_RBC2,Buildcnnect_RBC2,…};

LTSRS={idle,GetconTSRS,Sendversion_TSRS,Buildcnnect_TSRS,SendEM}。

等級轉換場景中,應答器的時間自動機模型如圖5所示,臨時限速服務器的時間自動機模型如圖6所示,車載設備的時間自動機模型如圖7所示,CTCS-3區域內無線閉塞中心的時間自動機模型如圖8所示,CTCS-N區域內無線閉塞中心的時間自動機模型如圖9所示。

圖5 Balise的時間自動機模型

圖6 TSRS的時間自動機模型

圖7 Onboard時間自動機模型

圖8 RBC1的時間自動機模型

圖9 RBC2的時間自動機模型

Onboard時間自動機模型中狀態位置與變量的含義見表2。

表2 模型中關鍵位置與關鍵變量

Tab.2 Key positions and key variables in the model

4 模型仿真和驗證

4.1 模型仿真

時間自動機模型的仿真通過UPPAAL的模擬器生成消息順序圖來實現[17],用于保證模型的完整性與一致性。圖10為模型輸入到UPPAAL模擬器中的模型,圖11為車載設備由CTCS-3等級轉換到CTCS-N等級生成的消息順序圖,圖12為車載設備由CTCS-N等級轉換到CTCS-3等級的消息順序圖。

圖10 模擬器中系統模型

圖11 CTCS-3轉換至CTCS-N的消息順序圖

圖12 CTCS-N轉換至CTCS-3的消息順序圖

4.2 模型驗證

時間自動機模型的驗證是通過UPPAAL的驗證器進行驗證的[18]。模型的驗證主要是從系統的功能要求、性能要求和故障狀態下的系統要求3個方面進行分析。基于表1所列的BNF范式進行模型驗證,程序實體如下:

a.系統的功能要求

1) 系統無死鎖:A[]not deadlock。

2) C3-RBC在行車許可終點到達RBC切換應答器時向CN-RBC發送列車預告信息并且申請進路信息。當收到CN-RBC的進路信息時,向車載設備發送CN-RBC區域的行車許可(CN-RBC在行車許可到達RBC切換應答器時向C3-RBC發送列車預告信息并申請進路信息;當收到C3-RBC的進路信息時,向車載設備發送C3-RBC區域的行車許可)。此功能的驗證程序為:E<>((RBC1.idle imply RBC1.ApplyInfo) and (RBC1.idle imply RBC1.GetRouteSuc) and (RBC1.idle imply RBC1.SendRBC2MA)) and ((RBC2.idle imply RBC2.ApplyInfo) and (RBC2.idle imply RBC2.GetRouteSuc) and (RBC2.idle imply RBC2.SendRBC1MA))。

3) 車載設備根據應答器信息向TSRS發起會話。若車載設備收到TSRS發送的版本信息,則表明會話建立成功,接著下載電子地圖。此功能的驗證程序為:E<>((Onboard.idle imply Onboard.ConnectCmd) and (Onboard.idle imply Onboard.Connectbuild_TSRS) and (Onboard.idle imply Onboard.DownloadEM))。

4) CTCS-3轉換至CTCS-N時,列車接近RBC轉換應答器,C3-RBC向車載設備發送RBC切換命令。若車載通信電臺正常則呼叫CN-RBC;若通信電臺故障,則呼叫失敗(CTCS-N轉換至CTCS-3時,列車接近RBC轉換應答器,CN-RBC向車載設備發送RBC切換命令。若車載通信電臺正常,則呼叫C3-RBC;若通信電臺故障,則呼叫失敗)。此功能的驗證程序為:E<>((RBC1.idle imply RBC1.ApprochRBC) and (RBC1.idle imply RBC1.SendRBCcmd) and (Onboard.idle imply Onboard.StartcomRBC2)) and ((RBC2.idle imply RBC2.ApprochRBC) and (RBC2.idle imply RBC2.sendRBCcmd) and (Onboard.idle imply Onboard.StartcomRBC1))。

5) CTCS-3轉換至CTCS-N時,在移交列車控制權前,若車載設備僅與C3-RBC通信正常,則車載設備重新呼叫CN-RBC(CTCS-N轉換至CTCS-3時,在移交列車控制權前,若車載設備僅與CN-RBC通信正常,則車載設備重新呼叫C3-RBC)。此功能的驗證程序為:E<>((Onboard.idle imply Onboard.FailComRBC2) and (Onboard.idle imply Onboard.StartcomRBC2)) and ((Onboard.idle imply Onboard.FailComRBC1) and (Onboard.idle imply Onboard.StartcomRBC1))。

6) CTCS-3轉換至CTCS-N時,車載設備在列車前端越過等級轉換應答器后轉換至CTCS-N等級(CTCS-N轉換至CTCS-3時,車載設備在列車前端越過等級轉換應答器后轉換至CTSCS-3等級)。此功能的驗證程序為:E<>(Onboard.idle imply Onboard.HeadpassLTO) and (Onboard.idle imply Onboard.ConversionCN) and ((Onboard.idle imply Onboard.PassLTA) and (Onboard.idle imply Onboard.ConversionC3))。

7) 等級轉換場景中,CN-RBC應能接收CTCS-3級車載設備的位置報告,并發送相應的行車許可。此功能的驗證程序為:E<>((RBC2.idle imply RBC2.Getloc) and (RBC2.idle imply RBC2.SendCCandMA))。

b.系統的性能要求

1) 車載設備呼叫RBC、TSRS的時間不應該大于20 s。此性能的驗證程序為:A<>((Onboard.Connectbuild_TSRS imply Ttsrs<=20) and (Onboard.Connectbuild_RBC2 imply Trbc<=20) and (Onboard.Connectbuild_RBC1 imply Trbc<=20))。

2) 車載設備與RBC進行通信的時間不應該大于20 s。此性能的驗證程序為:A<>(Onboard.GetCCandMA imply Tcom<=20)。

c.故障狀態下的系統要求

1) CTCS-3轉換至CTCS-N時,列車越過RBC切換應答器后,當車載設備未收到CN-RBC的消息時,車載設備降級運行。故障狀態下系統的驗證程序為:E<>((Onboard.Sendloc imply MA<1) and (Onboard.idle imply Onboard.FailConCN) and (Onboard.idle imply Onboard.InC3))。

2) CTCS-3轉換至CTCS-N時,車載設備在移交RBC前,如果與CN-RBC通信中斷,車載設備重新呼叫CN-RBC并且完成列車注冊與進路信息的申請。故障狀態下系統的驗證程序為:E<>((Onboard.Connectbuild_RBC2 imply RBC_2<1) and (Onboard.idle imply Onboard.FailComRBC2) and (Onboard.idle imply Onboard.GetRBCcmd))。

將上述驗證該系統需求的BNF語句輸入到驗證器中進行驗證。在驗證器中驗證語句后面的綠色圓圈表示驗證通過,紅色表示不通過。驗證結果如圖13所示,可以看出,本文所建立的模型滿足CTCS-N的需求。

圖13 模型驗證圖

5 結論

1) 基于技術規范分析了新型列控系統等級轉換場景的具體流程,并且對該場景的車載設備、應答器、C3-RBC、CN-RBC、TSRS的信息交互進行了準確描述。然后提取功能需求,基于TA語言使用UPPAAL建立時間自動機模型。

2) 建立新型列控系統在該場景的時間自動機模型后,使用模擬器生成消息順序圖,用于仿真各個子模型之間的信息交互場景。通過仿真模型的通信過程可以使系統設備間信息交互的理解更加形象,并且可以檢驗出模型是否存在缺陷、錯誤,完善系統的設計。

3) 根據新型列控規范整理車載設備由CTCS-3轉換至CTCS-N的主要故障模式,通過驗證器對模型的正常和故障模式進行了驗證,確保了所建模型的功能與性能滿足技術規范。驗證通過后,本文建立的時間自動機模型可以作為場景原型在系統功能測試階段和故障分析時起到重要作用,有助于減少測試的投入。