葉安君

(中鐵第一勘察設計院集團有限公司，710043，西安//高級工程師)

我國現運營的高速鐵路采用的是國產化CTCS-3級列車運行控制系統(tǒng)(以下簡稱“列控系統(tǒng)”)。中國鐵路總公司是2014年開始開展自主化CTCS-3級列控系統(tǒng)技術研究的，研發(fā)了一批具有自主知識產權的自主化C3等級列控系統(tǒng)安全關鍵設備[1-2]。其中，自主化ATP(列車自動保護)系統(tǒng)是我國鐵路的重要技術裝備，是保證高速列車行車安全、提高運輸效率的關鍵設備[3-4]。

自主化ATP系統(tǒng)在國產化ATP系統(tǒng)的基礎上，增加和優(yōu)化了一些安全功能需求，具有SIL4級的安全需求，一旦失效可能導致列車出軌等行車事故。目前，自主化ATP系統(tǒng)的研究主要集中在需求規(guī)范和系統(tǒng)測試方面[5-6]，理論研究相對較少。

時間自動機[7]具有嚴謹的數學基礎，能夠分析實時系統(tǒng)的功能邏輯需求及時間性能，在鐵路信號安全關鍵系統(tǒng)中得到了廣泛應用[8-9]。文獻[10]采用時間自動機對ATP系統(tǒng)的超速防護功能進行形式化建模，驗證了ATP系統(tǒng)的安全性和活性；文獻[11]采用時間自動機分析了ATP系統(tǒng)的2乘2取2結構，驗證了冗余結構的安全屬性；文獻[12-13]基于時間自動機分析了C3等級列控系統(tǒng)等級轉換的系統(tǒng)需求；文獻[14]基于時間自動機建立了等級轉換時間自動機網絡模型，驗證了等級轉換過程中的安全性和實時性；文獻[15]采用時間自動機分析了自主化C3列控系統(tǒng)碼序校驗以及RBC(無線閉塞中心)切換等場景。研究表明，采用時間自動機對鐵路信號系統(tǒng)進行建模和驗證，對系統(tǒng)的需求分析和設計具有良好的指導作用。本文采用時間自動機方法，以自主化ATP系統(tǒng)的C2等級轉換到C3等級功能為例，從理論上分析ATP系統(tǒng)需求的安全性、正確性和實時性，對自主化ATP系統(tǒng)的研究具有一定的理論意義。

1 自主化C3列控系統(tǒng)概述

1. 1 自主化C3列控系統(tǒng)發(fā)展過程

2007年，原鐵道部成立C3技術攻關組開展C3列控系統(tǒng)的研發(fā)工作,在引進國外技術的基礎上，實現了ATP和RBC設備的國產化，并成功應用于武廣、鄭西和京滬等高速鐵路，這項研究對我國列控系統(tǒng)的發(fā)展和鐵路裝備現代化發(fā)揮了重要作用。

2014年，中國鐵路總公司依托科研開發(fā)重點課題“列控系統(tǒng)設備自主化及技術要求研究”，開發(fā)具有自主知識產權的列控系統(tǒng)關鍵設備。2015年中國鐵道科學研究院集團有限公司立項“CTCS-3級列控系統(tǒng)關鍵設備自主化研究”，專項對C3列控系統(tǒng)自主化研究進行重點研究。在中國鐵路總公司的組織下，2016年6月至2017年1月，依托大西線綜合試驗段，對自主化C3列控系統(tǒng)進行了現場試驗。2018年6—10月，以京沈高鐵遼寧段為試驗平臺對自主化C3列控設備進行了綜合試驗，動態(tài)檢測了自主化C3列控設備的功能及性能[17]。

1. 2 自主化C3列控系統(tǒng)的特點

自主化C3列控系統(tǒng)在國產化C3列控系統(tǒng)的基礎上，對硬件、軟件和功能需求都提出了新的要求。

1) 硬件、軟件方面：自主化C3列控系統(tǒng)設備采用并列系工作，在保障系統(tǒng)安全性的同時增加設備可用性，擁有完全自主的知識產權。

2) 功能方面：自主化C3列控系統(tǒng)設備在國產化C3列控系統(tǒng)設備的基礎上，增加了一些新的功能需求。以自主化ATP系統(tǒng)為例，新增加的功能需求包括：①C3行車許可融合軌道電路信息。C3主控單元計算軌道電路信息許可，并根據列車當前位置確定軌道電路信息許可終點。②在應答器報文中增加開門側提示。③等級轉換時，不需要司機進行確認。④使用JRU(司法記錄單元)給各個主要模塊進行校驗時，保證各模塊的系統(tǒng)時間保持同步。

2 自主化ATP系統(tǒng)等級轉換功能

按照功能要求和設備配置劃分，我國列控統(tǒng)劃分為C0—C4共5個應用等級。同條線路上可以有多種應用等級，以滿足不同線路速度的需求。自主化列控系統(tǒng)等級轉換即是C3等級和C2等級之間的轉換。

2. 1 C2等級向C3等級轉換場景分析

自主化ATP系統(tǒng)等級轉換功能包括C2等級向C3等級轉換和C3等級向C2等級轉換兩種場景。這屬于自主化ATP系統(tǒng)運行過程中重要的安全功能。列車如果未在指定的位置或時機轉換到正確的運行等級，輕則可能造成行車中斷影響行車效率，重則可能導致行車事故造成人員傷亡。從理論上分析和驗證等級轉換功能邏輯的安全性和準確性，對保證列車行車安全具有重要意義。

自主化ATP系統(tǒng)在C3等級控車時，系統(tǒng)接收軌道電路的編碼信息，并與RBC發(fā)送的MA(移動授權)進行對比，判斷是否一致。自主化ATP系統(tǒng)與RBC、軌道電路和應答器信息交互關系如圖1所示。

圖1 自主化ATP系統(tǒng)信息交互關系

本文以C2等級向C3等級轉換為例進行分析。C2等級向C3等級轉換典型運營場景包括：

1) 列車由C2等級運營線路進入C3等級運營線路，如列車駛出C2等級的動車段進入C3等級的運營線路。

2) 列車由于無線通信中斷等原因由C3等級降級到C2等級后，需要重新轉換到C3等級控車。

為保障等級轉換功能的順利進行，運營線路在地面設置了RBC連接點(RE)、等級轉換預告(LTA)和等級轉換執(zhí)行點(LTO)3個轉換點。當列車前端通過RE時，ATP根據應答器信息呼叫RBC并進行注冊。當列車前端通過LTA點時，ATP將向RBC報告所在位置，RBC向ATP提供行車許可及等級轉換命令。當列車前端通過LTO點時，ATP執(zhí)行控車轉換。

2. 2 C2等級向C3等級轉換功能分析

C2等級向C3等級轉換的過程主要包括列車與GSM-R網建立連接、與RBC建立通信會話、獲取C3等級區(qū)域的MA和執(zhí)行等級轉換4個階段，轉換邏輯如圖2所示。

圖2 C2等級向C3等級轉換序列圖

1) 與GSM-R網建立連接。列車從C2等級向C3等級轉換，首先要建立與GSM-R電臺的連接。當ATP無線電臺檢測到GSM-R網后，自動與GSM-R網絡建立連接。

2) 與RBC建立通信會話。與GSM-R網連接成功后，ATP呼叫RBC，向RBC發(fā)送列車位置報告。RBC向車載設備發(fā)送位置報告參數信息和MA請求參數信息。車載設備收到配置參數后向RBC發(fā)送確認信息。

3) 獲取MA。列車前端通過預告應答器LTA后，RBC向車載設備發(fā)送包含C3等級區(qū)域的MA和等級轉換命令。若ATP不能收到MA和等級轉換命令，列車保持C2等級繼續(xù)運行。當列車重新獲得MA后，進行等級轉換處理。在C3等級完全模式下，自主化ATP系統(tǒng)接收軌道電路信息的行車許可，因此，自主化ATP系統(tǒng)需要判斷C2級行車許可和RBC發(fā)送的MA是否均越過等級轉換邊界。

根據自主化ATP系統(tǒng)C2等級向C3等級轉換的功能，正常轉換過程涉及應答器、RBC、C2行車許可、C3 MA等對象，轉換過程中可能出現應答器丟失、無線通信中斷、行車許可不一致(MA越過轉換邊界，但C2行車許可未越過)等故障場景。

3 時間自動機

時間自動機[18](TA)是針對帶有時間因素的狀態(tài)轉換關系，在傳統(tǒng)的有限狀態(tài)自動機的基礎上引入時間約束，提出的一種基于嚴謹的數學理論的描述方法，在實時系統(tǒng)的規(guī)范說明和形式化分析中占據重要地位。

定義1：時間約束

對于一個時鐘變量集合X，時間約束δ的集合Φ(X)定義如下：

δ：=x≤c|c≤x|δ|┐δ1∧δ2，

其中，x∈X,c∈Q，δ1、δ2表示時鐘約束。

定義2:時間自動機

一個時間自動機TA是一個六元組{S,S0,Σ,X,I,E}，其中：

S是一個有限位置的位置集合；

補救措施：一旦出現塌孔現象，需馬上增加護筒長度并用機械壓入。在下壓過程中如遇硬物阻擋無法下壓則應當適當加大或者縮小孔徑，使護筒順利下壓，但兩種方案都需重新處理護筒外的空隙。

S0是一個初始位置的位置集合，且S0?S；

Σ是一個有限字符的字符集合；

X是一個有限時鐘的時鐘集合；

I是一個映射，將S中的每個位置映射到Φ(X)中的某個時間約束；

E?SΣ2xΦ(X)S是轉移的集合。

一個狀態(tài)轉移{s,a,λ,δ,s′}表示當系統(tǒng)輸入字符a并滿足時鐘約束δ時，位置s遷移到位置s′。λ表示狀態(tài)轉移時，所有重置的時鐘變量的集合。

UPPAAL軟件是由瑞典Uppsala大學和丹麥Aalborg大學聯合開發(fā)的時間自動機集成工具環(huán)境。UPPAAL軟件對經典的時間自動機進行了擴展，包括編輯器、模擬器和驗證器，支持時間自動機的建模、仿真和驗證。UPPAAL軟件采用on-the-fly技術，對時間自動機的可達性進行分析，進而能夠驗證系統(tǒng)的安全性和活性等系統(tǒng)屬性。

4 C2等級向C3等級轉換建模

根據C2等級向C3等級的轉換邏輯，考慮到轉換過程的復雜性以及轉換過程中設備可能的故障，自主化ATP系統(tǒng)主要從正常轉換和故障場景兩個方面進行建模，如圖3所示。對于應答器丟失故障采用故障注入的方式，將應答器丟失行為注入到正常轉換模型中；對于無線通信中斷和行車許可不一致故障單獨建立時間自動機模型。

圖3 自主化ATP系統(tǒng)時間自動機建模方法

C2等級向C3等級轉換的時間自動機模型C2toC3TA劃分為ATP時間自動機模型ATPTA、RBC時間自動機模型RBCTA、Balise時間自動機模型BaliseTA、通信狀態(tài)時間自動機ConnectTA和行車許可時間自動機模型MATA5個部分，則C2等級向C3等級轉換的時間自動機模型為以上5個時間自動機模型的積，即：

C2toC3TA=

ATPTA‖RBCTA‖BaliseTA‖MATA‖ConnectTA。

C2等級向C3等級轉換的時間自動機模型如圖4所示，模型中主要狀態(tài)、變量的含義如表2所示。其中，ATPTA模型中注入了應答器丟失的場景，ConnectTA描述了無線通信中斷的故障情況，MATA描述了MA越過等級轉換邊界，但C2級行車許可未越過的故障情況。

C2等級向C3等級轉換的時間自動機模型具有1個時鐘變量x，所有通道信號均為broadcast chan類型，所有變量均為int類型。以“?”結尾的標記表示接收到該信號時轉換發(fā)生，以“!”結尾的標記表示發(fā)射該信號時轉換發(fā)生。

1) ATPTA模型。主要描述ATP和RBC之間的交互信息，主要包括請求與RBC建立通信會話、發(fā)送列車數據、請求MA和執(zhí)行等級轉換等過程。當等級轉換所有條件滿足時，ATPTA轉移到Switch狀態(tài)，表示等級轉換成功，ATPTA向RBCTA發(fā)送確認信息。ATPTA根據ConnectTA中Connect的值判斷連接狀態(tài)，連接失敗時，轉入SwitchFail狀態(tài)，放棄等級轉換。列車通過LTO時，ATPTA根據MATA中OverLTO的值判斷是否存在制動，如果存在制動狀態(tài)，ATPTA不進行等級轉換。

2) RBCTA模型。主要描述RBC和ATP之間的交互信息，包括ATP與RBC建立連接、發(fā)送MA和發(fā)送等級轉換命令3個部分。RBCTA根據ConnectTA的連接狀態(tài)，判斷ATP是否與RBC建立連接。在RBC與ATP成功建立連接的情況下，RBCTA與ATPTA交互列車數據、行車參數等數據，RBCTA根據列車位置及運行狀態(tài)，向ATPTA發(fā)送等級轉換命令。當列車通過LTO，但未接收到執(zhí)行應答器信息時，即PassLTOState為2，ATPTA發(fā)送等級轉換信號Switch。

3) MATA模型。描述C2級行車許可、C3級MA和等級轉換邊界的關系。當C2級行車許可和C3級MA均越過等級轉換邊界時，MATA將OverLTO變量置為1；當C2級行車許可未越過等級轉換邊界時，OverLTO為2。ATPTA根據OverLTO的值判斷是否進行等級轉換。

4) ConnectTA模型。描述列車與RBC的連接狀態(tài)。當列車于RBC斷開連接時，ConnectTA將連接狀態(tài)Connect變量置為0，表示ATP與RBC連接失敗。

5) BaliseTA模型。描述列車通過RE、LTA和LTO時的行為。當列車依次通過RE、LTA和LTO時，BaliseTA分別廣播RE、LTA和LTO信號，ATPTA接收到RE信號后發(fā)送login信號，請求RBC注冊。

5 C2等級向C3等級轉換形式化驗證

為驗證C2等級向C3等級轉換的時間自動機模型是否滿足自主化ATP系統(tǒng)的需求，本文從安全性、活性和實時性3個方面，利用UPPAAL軟件提供的模型檢測技術對C2toC3TA模型進行形式化驗證。

UPPAAL形式化驗證的基本原理是用時間自動機M描述系統(tǒng)行為，用BNF語法描述系統(tǒng)屬性φ，分析M是否為φ的一個模型M|=φ?。

UPPAAL軟件提供的BNF語法如下：

圖4 自主化ATP C2等級轉換C3等級時間自動機模型截圖

序號狀態(tài)含義序號變量或信號含義1getPara獲取行車參數7login請求注冊RBC2Switch等級轉換過程中8Connect通信狀態(tài),0表示中斷,1表示正常3OverC2行車許可和MA均越過等級轉換邊界9switchCfm通知RBC等級轉換成功4BeforeC2行車許可未越過等級轉換邊界10reset轉換結束5PassLTORBC檢測列車通過LTO應答器組11LTO列車通過LTO應答器組6LTOLostLTO應答器組丟失12PassLTOState列車通過LTO應答器組時的狀態(tài),1表示正常通過,2表示LTO應答器組丟失

φ::=E<>p|A[]p|E[]p|A<>p|p→q，

其中：E<>p表示p在1個狀態(tài)轉移序列s0→s1→…→sn的某個狀態(tài)下為真，則E<>p為真，s0表示初始狀態(tài)；A[]pnotE<> notp；E[]p表示存在某個狀態(tài)轉移序列s0→s1→…→sn，p在這個序列中的所有狀態(tài)下都為真，則E[]p為真；A<>pnotE[]notp；p→q表示p為真則q為真。

根據自主化ATP系統(tǒng)需求，提取C2等級向C3等級轉換過程中的安全性、活性和實時性要求。安全性指描述系統(tǒng)不期望發(fā)生的性質，如“連接RBC失敗時，ATP能轉換到C3等級”，通常表示“壞的事情不會發(fā)生”?；钚悦枋隽讼到y(tǒng)必定發(fā)生的性質，如“ATP能夠由C2等級轉換到C3等級”，通常表示“好的事情會發(fā)生”。實時性主要描述自主化ATP系統(tǒng)中的時間約束，如根據自主化ATP與RBC之間的通信功能，ATP與RBC連接超過10 s，則通信超時。自主化ATP系統(tǒng)形式化驗證需求提取方法如圖5所示。

自主化ATP系統(tǒng)C2等級轉換到C3等級需要滿足安全性需求：連接RBC失敗時，ATP不能轉換到C3等級，即ATP系統(tǒng)C2等級控車；未與RBC成功建立連接時，在任何情況下都不能轉移到C3等級。根據C2toC3TA模型，該安全性需求的BNF描述如下：

圖5 自主化ATP系統(tǒng)形式化驗證需求提取方法

A[] ConnectTA.ConnectFail imply not ATPTA. SwtichSucc

采用UPPAAL軟件的驗證器進行形式化驗證，驗證消耗時間0.001 s，消耗內存6 884 KB。驗證結果通過，表明C2toC3TA模型滿足該安全性需求。

C2toC3TA模型的安全性、活性和實時性需要及驗證結果如表3所示。驗證結果表明，自主化ATP系統(tǒng)C2等級轉換C3等級的系統(tǒng)需求滿足指定的安全性、活性和實時性要求。

表2 自主化ATP系統(tǒng)形式化驗證內容和驗證結果

6 結論

本文針對自主化ATP系統(tǒng)的安全性、活性和實時性，采用時間自動機作為形式化建模和驗證方法，以C2等級轉換C3等級的安全關鍵功能為例，建立了自主化ATP系統(tǒng)C2等級轉換C3等級的時間自動機模型；從安全性、活性和實時性3個方面，對時間自動機模型進行了形式化驗證；從理論上分析了自主化ATP系統(tǒng)C2等級轉換C3等級的功能邏輯。結果表明，自主化ATP系統(tǒng)滿足期望的系統(tǒng)性質，基于時間自動機的形式化建模和驗證方法對自主化ATP的系統(tǒng)需求分析具有一定的指導和應用價值。