基于TRSL的RBC等級轉換場景研究

陳永剛，丁春平

(蘭州交通大學自動化與電氣工程學院，蘭州　730070)

?

基于TRSL的RBC等級轉換場景研究

陳永剛，丁春平

(蘭州交通大學自動化與電氣工程學院，蘭州730070)

無線閉塞中心等級轉換場景作為中國列車運行控制系統主要場景之一，切換成功與否直接影響高速列車的安全和運行效率。通過對形式化驗證方法的分析，采用基于定理證明的時間化工業軟件工程規范語言的嚴格方法(Timed Rigorous Approach to Industrial Software Engineering Specification Language，TRSL)，在對等級轉換過程進行分析的基礎上，設計交互信息圖，構建狀態遷移圖，并結合域建模方法實現對該場景的TRSL描述，最后利用語言推理規則，結合系統特性，實現對切換正確性和實時性的雙重驗證，結果表明：該場景滿足系統規范對功能性和實時性的要求，繼而說明該方法的有效性、正確性和通用性，為我國列控系統的設計開發和驗證提供一種新的途徑和依據。

列車運行控制系統；RBC等級轉換；TRSL；場景切換正確性

為保證高速列車安全、高效地運行，我國鐵路部門在參照歐洲列車控制系統的基礎上，研發了滿足我國鐵路線路的中國列車運行控制系統(Chinese Train Control System，CTCS)[1]。CTCS-3級列控系統具有分布式結構、連續式響應、實時性強的特性，如何選取有效而又合適的方法來實現系統特性的描述和驗證，已成為高鐵列控系統研究領域中的重要研究內容。目前，一般通過3種手段：仿真、測試以及最具嚴格性的形式化方法來驗證系統特性，由于前兩者的代價昂貴、花費時長，而且只能在系統投入前處理典型情況，無法實現狀態、路徑的窮舉遍歷[2]，針對安全苛求系統，采用形式化方法不僅可實現更嚴謹的系統描述和驗證，而且可避免以上方法的不足[3，4]。

形式化方法可以精準地表述系統結構、行為、特征以及時間要求等，用形式化方法描述系統需求規范要求，可以最大程度地找出其他方法中忽視的錯誤和缺陷，同時還可以運用嚴格的數學邏輯實現對系統特性的驗證分析，來判斷系統特性是否成立[5]。

模型檢驗和定理證明是兩種形式化驗證方法，前者窮盡搜索系統狀態，驗證特性不滿足時可給出反例實現錯誤定位，然而，當架構復雜的系統有多個并發任務時，會產生狀態爆炸問題[6，7]；定理證明利用數學邏輯系統描述系統結構和特性，結合系統公理和推理方法實現對特性的證明過程，該方法可以實現對現實中無窮系統的描述和特性驗證[8]。

工業軟件工程的嚴格方法(Rigorous Approach to Industrial Software Engineering，RAISE)源自于缺乏模塊性、不能處理并發情況的維也納開發方法，在描述和驗證系統時，可以使用“||”操作符描述并發進程，module定義可以清晰、方便地描述系統模塊化結構，RAISE也可通過type、sets等更為自然地描述系統變量和實體定義，且RAISE的封裝性和繼承特性使得實體描述相對獨立，既增強了擴展性，又降低了不兼容性，并且在系統的各個開發層次中，均可采用RAISE規范語言進行描述，進而使得整個開發過程處于同一語義框架內[9，10]。但是，該方法無法應用于帶有實時性的混成系統描述中，從而嚴重制約了其發展，因此，對RAISE進行時間化擴展是解決問題的關鍵[11]。

無線閉塞中心(Radio Block Center，RBC)等級轉換場景的完成與否直接影響高速列車的運行效率和安全，在對該運營過程詳細分析的基礎上，采用擴展后的TRSL方法實現建模，并對切換正確性和實時性進行了推理證明，通過驗證系統規范對等級轉換功能性和實時性的要求，為優化、完善系統規范提供可靠的理論依據，從而說明該方法的正確性和通用性，將其推廣應用到整個列控系統或者更加復雜的系統中。

1　TRSL介紹

在標準的RAISE規范語言(RAISE Specification Language，RSL)中主要包括應用式、命令式和并行3種規范[12]。在應用式中，可以定義type、value和axiom，除了固有的Unit、Char、Bool等7種類型和let、case2個應用式表達式，還包括Functions、Sets、Lists、Maps定義以及各自對應操作符的應用；在命令式規范中，可以實現對用來貯存特定類型值的variable定義，而且until、for、while循環表達式，以local開始以in做以限制并以end表示結束的局部表達式，post后置表達式也包含其中；RSL提供了連接符來表述說明需要被并行計算的表達式，而且還對通信原語做了定義，使得多個需要被并行計算的表達式之間可以通過channel進行通信。通過靈活應用以上3種規范，可以實現對系統反應性、混成性以及并發性的進程描述。在RSL探究過程中，對其進行了擴展，引入一個Time類型和一個wait e表述延遲的表達式，從而形成TRSL新方法，增添了對實時性的描述機制[13]。

TRSL依賴數學邏輯來表達系統結構和驗證特性，由于高鐵列控系統結構復雜、規模龐大，直接使用形式化方法描述驗證，不僅成本需求高，而且驗證效率也會有一定程度的降低，故而引入域方法實現系統模塊的劃分，整個驗證框架如圖1所示。

圖1　基于TRSL的建模驗證框架

首先對系統需求規范進行抽象化處理得到系統域模型，并使用TRSL對其進行描述，得到由命題、定理等構成的TRSL模型，然后將系統特性表述為axiom形式，最后使用RAISE推理規則對模型進行驗證。在驗證時，根據系統性質和模型以及RAISE推理規則，不斷對公理進行恒等的推理演繹，直到推出驗證結果，并對結果做以分析判斷。

2　RBC等級轉換分析

RBC等級轉換主要包含C2-C3、C3-C2以及故障降級3種情況，本文主要對前2種進行描述驗證。C3/C2間的轉換需要設置相應的轉換點、標志牌和確認區，應答器的設置需滿足高鐵列控系統應答器應用原則(V2.0)中的規定，以保證列車能夠在運行過程中實現不停車自動切換，具體如圖2所示[14]。

2.1構建信息交互圖

當列車從C2級區域進入C3級區域時，為了提高列車運行速率，需從C2轉換到C3控車，主要工作包括：車載注冊到無線網絡、與RBC建立通信、從RBC獲得行車許可(Movement Authority，MA)等步驟[15，16]。當列車駛離C3區域進入C2區域范圍時，RBC根據等級轉化預告點(Lever Transition Anticipation，LTA)的信息向車載下達轉換預告命令，列車頭部通過等級轉換執行點(Lever Transition Operation，LTO)時轉為C2級，尾部越過執行應答器后車載向RBC報告位置信息，隨后斷開與RBC的連接，注銷列車信息，關閉與鐵路移動通信系統GSM-R (Global System for Mobile Communications-Railway)的連接，最后按照C2級控車[17]。

根據對RBC等級轉換原理的分析，可以得到轉換過程中各主要設備間信息傳遞的交互圖，如圖3、圖4所示。

圖2　C2/C3應答器布置和確認區設置

圖3　C2-C3級RBC等級轉換信息交互圖

圖4　C3-C2級RBC等級轉換信息交互圖

2.2建立狀態轉移圖

RBC等級轉換過程的發生在時間上來說是連續的，但是在整個進程中設備間卻是離散地傳遞信息，而且在執行操作以外的時間軸上，皆無連續動作的出現，從而可以將執行操作的那段時間段看成是一個連續進程，以RBC與列車車載交互時信息的傳輸為分界線，忽略沒有操作執行的時間段，繼而實現在時間上

離散化整個連續進程，最終得到RBC等級轉換的狀態轉移圖[18]，如圖5所示。針對RBC等級轉換，主要考慮了司機、列車、RBC和應答器4個對象，為了簡化描述，將動作操作比較少的應答器和司機歸于RBC和車載中，而且，對設備的每一個狀態進行了編號。

在圖5中，方框表示設備狀態，方框內則是設備在每一個狀態下需要執行的事件。隨著時間的推演，設備狀態不斷發生變化，而狀態在變化的同時要完成方框內需要執行的事件，在等級轉換過程中主要是通過信息的傳輸來觸發這些事件的發生，因而可以得出，信息的交互過程使得設備的狀態隨著時間的推移不斷地發生變化，最后達到每個設備的最終狀態，從而完成了等級轉換這一個過程。

3　形式化建模

3.1建立域模型

為了降低對復雜系統建模的難度，簡化后續對RBC等級轉換過程的TRSL描述，引入了域方法。域是一種抽象方法，在蘊含自己本身特性的同時，也涵蓋與其他域之間的聯系關系，其本質是對系統實現模塊化分解；域結構定義為D=(S，I，O，F(s)，T，D’)，其中，S是系統狀態集合(S1，S2，…，Si)，S1代表系統初始狀態；I是系統的輸入集，O是輸出集，而且此二集合與S相關；F(s)是系統域函數，實現從I到O的一系列操作行為，表示為F(s)=I(si)1 ×…×I(si)i→O(si)1 × …×O(si)i；T是域模型特性集合，主要體現F(s)的性質；D’子域集是一個可選項，與D有著相同的定義方式。

圖5　RBC等級轉換狀態轉移圖

RBC等級轉換的實質是通過車載和地面間持續不斷的信息交互傳遞，使設備的狀態不斷遷移發生變化，最終實現等級的轉換。將RBC等級轉換過程看作是一個域，得到域結構模型如圖6所示。

圖6　RBC等級轉換域結構模型

根據域的定義，針對RBC等級轉換場景，提出輸入In、輸出Out和函數F三個基本元素。在In和Out中包含了車載設備和RBC的狀態參數信息等，車載的等級、列車的速度和位置、軌道電路區間占用情況等均可以看作是域的In，這些信息在F的推動下，不斷遷移不斷變化，直至Out進入轉換后的狀態參數。根據前述對RBC等級轉換過程的描述和分析可知，等級轉換的實現是在信息交互的推動下完成的，因而，函數F的作用就相當于信息交互的進行，即整個信息交互的過程就是F函數。

3.2域模型到TRSL模型的轉化

RBC等級轉換域模型描述了系統的抽象靜態結構，只有匹配動態行為后才可完成系統完整表述，而且域模型特性T的驗證最終是要使用形式化方法TRSL來實現，因而需要實現域模型到TRSL描述的轉化。

域模型元素分為非特性元組S、I、O、F(S)和特性元組T，若系統域結構模型已被搭建，系統的I、O集合不僅表示了系統的輸入、輸出狀態，而且體現了系統的邊界范圍，而F就是實現此功能的要緊之處，對域非特性元組F的TRSL實現也是描述的關鍵。以C2-C3等級轉換的RBC模塊舉例說明，對于域的非特性元組，狀態S主要使用type定義完成，具體如下。

class

type

RBC∶Nat

/*定義了Nat類別的RBC模塊*/

RBC_state==R1|R2|R3|R4|R5|R6|Rok|Rerror

/*RBC_state類型包含八種狀態值*/

vh∶vehicle，r∶RBC，gr∶GSM-R

/*vh代表車載，r代表RBC，gr代表GSM-R*/

RBC_next(r，gr) ≡

/*函數RBC_next用來決定RBC的下一個狀態*/

case state(r) of

/*判斷RBC在哪一個狀態*/

R1→R1execute-task(r，gr)

/*若RBC在R1狀態時要執行R1內所有事件*/

Rok→(r，gr)，Rerror→(r，gr)

/*如果在成功或錯誤狀態，則不發生變化*/

end

對于C2-C3等級轉換的RBC模塊，域的非特性元組I是指RBC_state類型中的R1狀態，而O可能是順序執行完所有狀態之后的Rok狀態，也可能是出現故障或未完成所有狀態順序執行的Rerror錯誤狀態，而且，整個I到O的操作實現是由F完成的，并且，針對每一個狀態，I、O以及F均有所不同體現，例如，R2狀態的描述如下。

R2execute-task(r，gr) ≡

/*R2狀態執行事件*/

let (news，gr)=RBC_obtain(gr) in

/*通過函數RBC_obtain(gr)獲取消息*/

case news of

/*判斷消息類別*/

data_train(vh，r)→RBC_transmit(Loca_req

(r，vh)，gr) || RBC_transmit(MA_req(r，vh)，gr);

/*如果r收到列車數據消息data_train(vh，r)，則向vh發送位置報告請求參數Loca_req(r，vh)并傳輸MA請求參數信息MA_req(r，vh)*/

wait transfernews_time; state_change(R3)

/*等待端到端傳輸時延后，r遷入R3狀態*/

nil→(r，gr)

/*如果收到nil信息，則不發生動作*/

error→state_change(Rerror)

/*如果收到error消息，轉移進入Rerror狀態*/

end

在設備狀態和狀態間轉移的表述中，使用TRSL中的“||”和“;”操作符實現對系統并發、順序事件的描述，與此同時，利用type、value定義來對列控系統無線網絡QoS指標參數[19]做以說明，具體使用時，采用wait e表達式來表述。例如，車地間連接建立的TRSL表述如下。

type

LinkB_time={t∶Time·5

value

LinkB∶vehicle×RBC×Bool

LinkB∶UnitUin any write Unit

LinkB() ≡ LinkBuild(vh，r); wait LinkB_time

對于域的特性元組T，數字特性使用“∑”、“<”、“+”等各種數學運算符將其表述成axiom形式進行規約，狀態特性采用邏輯符號“^”轉化成Bool類型進行識別，如下規約了C2-C3轉換場景交互正確性要求和部分時間特性約束。

axiom

[correctness_C2-C3]

/*C2-C3級間轉換正確性公理*/

?vh∶vehicle，r∶RBC，gr∶GSM-R·

/*vh代表車載，r代表RBC，gr代表GSM-R*/

vehicle_state(vh)=Vh1∧RBC_state(r)=R1∧

/*定義vh和r的初始狀態*/

vehicle_gain(vh，gr)=nil ∧

RBC_obtain(r，gr)=nil ∧

/*初態時信道中不存在任何信息*/

let (vh',r',gr')=Tra(vh，r，gr) in

/* Tra 是一個狀態遍歷函數*/

vehicle_state(vh')=Vhok∧

RBC_state(r')=Rok∧

/*在遍歷條件下，達到vh、r最終態Vhok和Rok*/

TotleT1-expend (R3，Rok)<=20∧

/*車載和RBC交換數據的時間預估為20s*/

TotleT2-expend(Vh1，Vhok)<=80

/*從GSM-R注冊到完成轉換時的時間不大于80s*/

[realtime_C2-C3]

/*C2-C3級間轉換實時性公理*/

TotleT1-expend(R3，Rok)=

/*車載和RBC交換數據的時間統計*/

TotleT2-expend(Vh1，Vhok)=

/*從GSM-R注冊到完成轉換時的時間統計*/

3.3RBC等級轉換的驗證

在RBC等級轉換場景，選擇了切換正確性和實時性兩個典型指標。切換正確性要求判別以下2個條件：第一，按照流程系統能夠進入成功狀態；第二，遍歷所有實例中系統狀態的路徑。實時性指標不僅要求系統要在確定的時間內做出響應，而且要保證響應的正確性。在該場景中，一旦違反相關時間的約束，不光會影響到行車效率，可能還會造成列車安全事故。

為了實現對RBC等級轉換實時性和正確性的建模驗證，首先需要使用TRSL將系統需求描述成axiom形式，完成系統特性要求的公理描述后，根據RAISE的等價規則、推斷規則以及與分解等推理規則對建立的axiom模型進行推理驗證，整個驗證流程如圖7所示。

在驗證的過程中，首先定義所需的變量、狀態、通道等，其次設定設備狀態和通道的初始值，然后根據條件進行狀態的遍歷和時間的考量，最后判斷結果是否符合要求。為了實現狀態的遷移，使用了函數Tra來進行狀態的遍歷，在Tra中為了獲取下一狀態引入了next函數，函數Tra通過next來獲取下一狀態的同時也使用finished來判斷是否已經達到最后狀態，如果不是函數指向下一遍歷對象狀態繼續執行Tra函數。

結合列車車載模塊和RBC模塊，按照圖7的系統特性驗證流程圖，依靠Tra遍歷函數借助函數next和finished，使用RAISE推理規則中的equivalence rules(等價)、and_split_inf(與分解)、inference rules(推斷)等規則[20]，對C2-C3等級轉換的axiom描述進行推理演繹，具體過程如下。

首先使用規則假設、與分解，將正確性公理分解為式(1)和式(2)

(1)

(2)

當式(1)的切換正確性和式(2)的實時性驗證結果都為true時，才表明系統設備能夠在規定的時間內實現C2到C3的轉換。

對于切換正確性，使用與分解得到以下二式

(3)

(4)

只有vh和r均順利達到成功態時才能說明能夠完成轉換。為了實現狀態的遷移，使用了函數Tra通過next借助函數finished來執行操作遍歷。

首先證明式(3)和式(4)，使用值代入規則將(vh',gr')帶入Tra函數中，從而得到式(5)

Tra(vh',gr')≡let (vh',gr')=next(vh，gr) in"

(5)

else Tra(vh',gr') end

再依據函數next，使用推斷值代入得式(6)

next(vh',gr')≡let(vh',gr')=vehicle_next(vh，gr)

(6)

根據axiom初始化賦值以及推斷規則，等價為執行Vh1execute-task(vh，gr)，再依據推斷規則，等效為執行Vh1狀態內所有事件。操作結束后vh轉入Ve2狀態，接著使用值代入將結果代入式(5)中，依據推斷規則將執行式(7)

if finished(vh',gr') then (vh',gr')

(7)

由于vh目前轉入Ve2狀態，未達到finished函數中定義的結束態，故而可得到式(8)

(8)

由于vh當前狀態已經執行完畢，函數會指向下一遍歷對象狀態，即進入RBC的狀態遍歷。使用值代入規則將(r',gr')代入Tra函數中，得到r的Tra函數定義，再根據next函數，使用推斷、值代入得到r的next函數定義。根據初始化條件，r執行RBC_next函數，使用推斷規則可以等效為執行R1execute-task(r，gr)；由于Ve1狀態執行中輸出了消息callRBC(vh，r)，該消息又作為RBC初始化狀態執行的I存在，故而等價為執行R1狀態內所有事件；操作完畢后轉而進入R2狀態，接著使用值代入將結果代入r的Tra函數中，根據推斷規則將執行finished函數，而且結果為false；由于已完成當前狀態操作，函數會指向下一遍歷對象狀態，后續推理過程與上述類似，不再贅述，最終，可以得到式(9)和式(10)

(9)

(10)

使用值代入規則將上述兩式代入式(1)中，從而得到結果：true ∧ true，該結果說明了C2-C3等級轉換時，vh和r都能遍歷完所有狀態而達到成功態，從而證明了能夠有效地完成C2-C3的轉換。

實時性證明是與交互正確性驗證同時進行的。根據轉換需求的axiom模型，結合vh和r的TRSL表述，使用RAISE推演規則進行推導，最終可得到式(11)和式(12)

(11)

(12)

使用值代入規則將上述兩式代入式(2)中，得到結果：true∧true，再結合axiom描述和式(1)的推理結果，可以得到結果恒為true值，從而證明了C2-C3等級轉換過程滿足系統實時性和交互正確性的需求。

C3-C2的特性驗證推理過程與上述C2-C3的步驟類似，此處不再詳述，最終可以得到執行結果如下

(13)

(14)

(15)

對式(13)和式(14)運用值代入規則得到結果為true值，從而說明車載和RBC借助Tra函數不斷地進行狀態遍歷后能夠進入正確狀態，能夠順利地完成C3-C2的轉換，即滿足切換正確性要求，再結合式(15)，可以表明，列車在線路上運行時能夠完成C3-C2轉換，而且滿足實時性的約束條件。

通過以上分析驗證，證明了TRSL方法能夠全面、精確、有效地對系統行為進行描述，并對系統特性實現驗證，繼而說明了該方法的正確性和通用性，從而為復雜系統的設計、開發和驗證提供新方法和根據。

4　結論

高鐵列控系統呈現出結構分布、響應快速、實時性強等多樣化特性，通過分析形式化驗證方法，采用基于定理證明的TRSL方法對RBC等級轉換進行建模，并實現對系統模型交互正確性和實時性的驗證。本文首先對RBC等級轉換場景進行分析，根據轉換過程中信息的傳遞建立了信息交互圖，再將整個連續轉換過程做以時間上的離散處理得到了狀態遷移圖，然后使用域方法建立了RBC等級轉換的抽象域模型，并采用TRSL對其實現形式化描述，最后將RBC等級轉換的切換正確性和實時性描述成axiom形式，結合RAISE推理準則和系統設備TRSL描述，不斷推理演繹實現對切換正確性和實時性的兩重驗證，結果表明RBC等級轉換滿足系統規范對功能性和實時性的要求，從而說明該方法的有效性、正確性和通用性，為安全苛求系統的設計、開發和驗證提供一種新的途徑和依據。

[1]唐濤.列車運行控制系統[M].北京:中國鐵道出版社，2012:168-178.

[2]趙顯瓊，唐濤.多端日形式化測試自動生成方法在CTCS-3車載系統中的應用[J].鐵道學報，2011，33(7):44-51.

[3]IEC.IEC62425:2007. Railway Applications-Communication， Signaling and Processing Systems-Safety Related Electronic Systems for Signaling[S]. IEC. 2003.

[4]IEC.IEC61508:2005. Functional Safety of Electrical/ Electronic/Programmable Electronic Safety-Related Systems[S]. IEC.2005.

[5]呂繼東.列車運行控制系統分層形式化建模與驗證分析[D].北京:北京交通大學，2011:1-22.

[6]劉金濤，唐濤，趙林.基于UML模型的CTCS-3級列控系統功能安全分析方法[J].鐵道學報，2013，35(10):59-66.

[7]侯剛，周寬久，常軍旺.基于時間STM的軟件形式化建模與驗證方法[J].軟件學報，2015，26(2):223-238.

[8]劉金濤，唐濤，趙林.基于微分動態邏輯的無線閉塞中心交接協議建模與驗證[J].中國鐵道科學，2012，33(5):98-104.

[9]陳怡海，繆淮扣.兩種形式語言:RSL與Z的分析比較[J].計算機應用與軟件，2002，19(4):11-50.

[10]賈若宇，趙保華，屈玉貴，等.CSP和RSL應用于協議形式化描述的研究[J].計算機應用，2003，23 (1):10-12.

[11]李黎.混成系統的描述和設計與Timed RAISE項目[J].計算機科學，2000，27(7):82-84.

[12]The RAISE Method Group.The RAISE Specification Language[M]. UK: Prentice Hall int. 1992:1-249.

[13]Li Li.Towards a denotational semanties of timed RSL using duration caleulus[J]. Journal of Computer Science& Technology， 2001，16(1):64-76.

[14]丁春平，陳永剛.Timed RAISE方法在列控系統等級轉換場景中的應用研究[J].鐵道標準設計，2015，59(8):164-169.

[15]鐵道部科技司.CTCS-3級列控系統標準規范—CTCS-3級列控系統系統功能需求規范(FRS)[M].北京:中國鐵道出版社,2009.

[16]Tianhua Xu， Tao Tang， Chunhai Gao， Baigen Cai. Logic verification of Collision Avoidance System in train control systems[C]∥IEEE. Intelligent Vehicles Symposium 2009. Xi’an. IEEE, 2009:918-923.

[17]王振強.CTCS-3級列控系統等級轉換運營場景智能形式化研究[D].蘭州:蘭州交通大學，2014:1-8.

[18]Kun Wei，Jim Woodcock，Alan Burns.Modelling temporal behavior in complex systems with timebands[A]. In: Mike Hinche， Lorcan Coyle. Conquering Complexity[C]. London: Springer， 2012:277-307.

[19]中國鐵路總公司.CTCS-3級列車運行控制系統[M].北京:中國鐵道出版社,2013.

[20]C.George，S Prehn.The RAISE Justification Handbook[M]. LACOS/CRI/DOC/7/V5.1994.

Research on TRSL-based RBC Level Transition Scene

CHEN Yong-gang， DING Chun-ping

(School of automation and electrical engineering， Lanzhou Jiaotong University， Lanzhou 730070， China)

As a main scene of the Chinese Train Control System， RBC (Radio Block Center) level transition scene， whether it can switch successfully， will directly affect high-speed train operating efficiency and safety. By analyzing the formal verification method， the method of time-based industrial software engineering specification language of theorem proving (Timed Rigorous Approach to Industrial Software Engineering Specification Language，TRSL) is selected. On the basis of the analysis of level transition process， interactive information figure is designed， state transition diagram is constructed， TRSL descriptions of the scene are implemented combined with domain modeling method， and finally the double verification of interaction correctness and real-time capability is fulfilled by means of inference rules and associated system features. The results show the consistence of the scene with system specifications in terms of functionality and instantaneity， and demonstrate the effectiveness， accuracy and versatility of the method， which may provide a new way and basis for the design， development and validation of train control system．

Train control system; RBC level transition; TRSL; Scene interaction correctness

2016-01-19

國家自然科學基金(61164101)

陳永剛(1972—)，男，副教授，主要研究方向：交通信息工程及控制，E-mail：chenyonggang@mail.lzjtu.cn。

1004-2954(2016)08-0122-08

U284.48

ADOI:10.13238/j.issn.1004-2954.2016.08.026