Timed RAISE方法在列控系統(tǒng)等級轉(zhuǎn)換場景中的應(yīng)用研究

丁春平,陳永剛

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

Timed RAISE方法在列控系統(tǒng)等級轉(zhuǎn)換場景中的應(yīng)用研究

丁春平,陳永剛

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

高速鐵路列車運行控制系統(tǒng)是一個復(fù)雜的實時性系統(tǒng),結(jié)合其實際特點,將域方法作為系統(tǒng)描述的切入。通過對模型檢驗和定理證明兩種驗證方法的分析比較,提出使用基于定理證明的時間化工業(yè)軟件工程的嚴(yán)格方法Timed RAISE形式化方法對等級轉(zhuǎn)換(CTCS-2級至CTCS-3級)場景進(jìn)行描述,并對其場景交互一致性和實時性進(jìn)行驗證,結(jié)果表明該場景不會出現(xiàn)場景交互一致性錯誤,也不會違反時間的約束。

高速鐵路； Timed RAISE； CTCS；等級轉(zhuǎn)換場景；實時性；場景交互一致性

高速鐵路是經(jīng)濟(jì)社會發(fā)展的必然趨勢，它具有安全性高、速度快等特點[1]。隨著計算機(jī)、通信、控制技術(shù)等先進(jìn)技術(shù)的廣泛應(yīng)用以及列車速度和密度的不斷提高，對系統(tǒng)的安全性和可靠性要求也越來越高。為了保證列車安全運行、降低事故發(fā)生率，需要高可靠性、高安全性的列車運行控制系統(tǒng)作為保障[2]。根據(jù)中國鐵路列車特性、運行速度、線路條件等運輸需求，將中國列車運行控制系統(tǒng)CTCS(Chinese Train Control System)分為CTCS-0級(簡稱C0)-CTCS-4級(簡稱C4)共5個等級[3]。C3級列車運行控制系統(tǒng)有效提高了列車的運營效率，該系統(tǒng)主要包含14個場景文件：注冊與啟動、注銷、等級轉(zhuǎn)換、RBC切換等[4]。本文對等級轉(zhuǎn)換(C2-C3)場景的條件及轉(zhuǎn)換過程做了詳述，并基于域+Timed RAISE對其進(jìn)行初步描述、驗證和分析。

1 C2-C3等級轉(zhuǎn)換原理

1.1 轉(zhuǎn)換前準(zhǔn)備事項

在等級轉(zhuǎn)換前需要對標(biāo)志牌、轉(zhuǎn)換點和確認(rèn)區(qū)進(jìn)行設(shè)置[5]。其中標(biāo)志牌設(shè)置包含通信連接標(biāo)志牌、等級轉(zhuǎn)換標(biāo)志牌的設(shè)置。轉(zhuǎn)換點設(shè)置包括GSM-R連接點(GRE)、RBC連接點(RE)、轉(zhuǎn)換預(yù)告點(LTA)、轉(zhuǎn)換執(zhí)行點(LTO)、轉(zhuǎn)換取消點的設(shè)置。等級轉(zhuǎn)換確認(rèn)區(qū)為等級轉(zhuǎn)換邊界點前一定距離(列車以最高速度運行至轉(zhuǎn)換點邊界約5 s的時間)和等級轉(zhuǎn)換后列車運行5 s的區(qū)域[6]。圖1所示即為C2-C3級間轉(zhuǎn)換過程中應(yīng)答器布置和確認(rèn)區(qū)設(shè)置。

圖1 C2-C3中應(yīng)答器布置和確認(rèn)區(qū)設(shè)置

1.2 C2-C3級間轉(zhuǎn)換過程

列車由C2轉(zhuǎn)換到C3控車前，需完成車載電臺注冊到GSM-R無線網(wǎng)絡(luò)、ATP與RBC建立通信等信息。如果在C2-C3轉(zhuǎn)換邊界不具備等級轉(zhuǎn)換條件，則列車?yán)^續(xù)按C2控車，直至具備C3控車條件后，列車自動轉(zhuǎn)入C3控車。一個典型的C2-C3控車的流程有以下6步[7-8]。

(1)車載設(shè)備在40 s內(nèi)檢測并注冊到GSM-R網(wǎng)絡(luò)并建立可靠連接。

(2)車載設(shè)備與GSM-R網(wǎng)絡(luò)建立連接后，列車經(jīng)過RBC連接應(yīng)答器組后，發(fā)送建立通信會話命令。系統(tǒng)版本信息通過RBC發(fā)送給車載設(shè)備，由車載設(shè)備檢查該版本信息的兼容性，若不兼容，則停止會話。

(3)由RBC發(fā)送位置報告和MA參數(shù)信息給車載設(shè)備。車載設(shè)備收到信息后，把列車位置信息、當(dāng)前控制等級信息發(fā)送給RBC。RBC收到信息后，發(fā)送配置參數(shù)給車載并給出確認(rèn)信息。

(4)列車通過LTA后，ATP向RBC發(fā)送列車數(shù)據(jù)信息并報告列車位置。RBC計算出MA參數(shù)后，將MA和等級轉(zhuǎn)換命令發(fā)送給車載設(shè)備。

(5)當(dāng)列車接近C2-C3級間轉(zhuǎn)換LTO時，司機(jī)對將要進(jìn)行的轉(zhuǎn)換等級確認(rèn)。

(6)列車頭部經(jīng)過LTO后ATP自動轉(zhuǎn)到C3控車。

2 Timed RAISE

2.1 形式化方法概述

在系統(tǒng)驗證初期，為了發(fā)現(xiàn)大量而又明顯的設(shè)計錯誤，對系統(tǒng)特性進(jìn)行驗證一般使用仿真和測試的方法。然而，這兩種方法并不是萬能的，它們無法檢查系統(tǒng)設(shè)計中存在的精微深奧而又繁瑣的錯誤。對于復(fù)雜系統(tǒng)，如果仿真和測試案例不能被正確地選取，很難對復(fù)雜系統(tǒng)的運行狀態(tài)和執(zhí)行路徑進(jìn)行窮盡的遍歷，從而會給系統(tǒng)安全帶來潛在的危險因素[9]。IEC62279：2002(《鐵路應(yīng)用-通信、信號和處理系統(tǒng)-鐵路控制和防護(hù)系統(tǒng)軟件》)中提出：“在軟件安全度完善等級為4級時，軟件需求規(guī)格說明書定義、軟件設(shè)計和實施、驗證和測試等過程中，強(qiáng)力推薦使用形式化方法進(jìn)行描述和設(shè)計，對于在軟件驗證和測試時，強(qiáng)力推薦的形式化證明技術(shù)[10]?！蓖瑫rIEC61508中也提出了：“在系統(tǒng)的安全完善度等級為4級的時候，強(qiáng)烈推薦利用形式化證明方法對系統(tǒng)進(jìn)行驗證[11]?！?/p>

模型檢驗和定理證明作為形式化驗證方法各有優(yōu)勢和不足[12]。形式化驗證方法模型檢驗的主要對象是有限狀態(tài)系統(tǒng)。驗證流程是：首先對系統(tǒng)進(jìn)行描述，最好選用能夠?qū)ο到y(tǒng)描述詳盡的形式化語言；接著對系統(tǒng)形式化模型進(jìn)行遍歷，選用能夠?qū)崿F(xiàn)對系統(tǒng)運行狀態(tài)和執(zhí)行路徑窮盡遍歷的算法；最后分析判定系統(tǒng)某種特性的要求能否被實現(xiàn)。當(dāng)判定系統(tǒng)某種特性的要求不被滿足時，為了方便定位錯誤的發(fā)生，形式化驗證方法模型檢驗會給出反例[13]。在基于定理證明的形式化方法中，首先定義了一種特殊的數(shù)學(xué)邏輯系統(tǒng)，接著將期望驗證的系統(tǒng)和相關(guān)重要特性用一系列公理和推理規(guī)則組成的數(shù)學(xué)邏輯表示，最后以系統(tǒng)的公理為基礎(chǔ)，使用推理規(guī)則一步一步推導(dǎo)出系統(tǒng)所期望的性質(zhì)[14-15]。

表1所示為常用形式化方法的總結(jié)[16]。

表1 形式化方法比較總結(jié)

注：◆表示能對此性質(zhì)驗證；◆◆表示適合對此性質(zhì)驗證

從表1中可看出：某種單一的方法只適應(yīng)于描述系統(tǒng)的少數(shù)特性，無法全面準(zhǔn)確地描述和驗證復(fù)雜系統(tǒng)。當(dāng)系統(tǒng)復(fù)雜、多任務(wù)并發(fā)運行或多子系統(tǒng)時，模型檢驗方法將會產(chǎn)生狀態(tài)空間爆炸問題，然而，基于定理證明的形式化方法卻與模型檢驗的形式化方法不同。具有無限狀態(tài)空間的復(fù)雜系統(tǒng)可以用定理證明的形式化方法對其分析和驗證，這種形式化驗證方法能夠?qū)δ硞€數(shù)域的特性實現(xiàn)完全驗證主要是由于它不依賴于參數(shù)取值范圍。

模塊性是RAISE方法的一個特點，可以通過模塊來規(guī)范值、變量、類型等各類實體。而且RAISE也具并發(fā)性，易于對進(jìn)程間的相互關(guān)系以及進(jìn)程間的并發(fā)性進(jìn)行研究。RAISE方法吸取了OZ、CSP的精華，但無法描述系統(tǒng)的時間特性。將時間約束條件加入RAISE方法中形成Timed RAISE，因此，Timed RAISE能夠?qū)哂袑崟r性的復(fù)雜系統(tǒng)進(jìn)行比較全面的描述。

2.2 Timed RAISE

Timed RAISE方法，即在RSL語言中引入了一個表示時間的類型和一個描述延遲的等待表達(dá)式。由于RSL語言自身有著結(jié)構(gòu)完善的語法、語義以及相應(yīng)的支持工具，所以這種擴(kuò)充必須是最小化的，即不能破壞RSL語言的原有結(jié)構(gòu)[17]。

(1)Time類型的添加

在RSL語言中擴(kuò)充了如下與時間有關(guān)的描述機(jī)制。

Type

Time //定義時間類型Time

Value

System:Unit→Time //定義函數(shù)System

其中，Time 數(shù)據(jù)類型主要用于說明與時間相關(guān)的變量。它被定為一個非負(fù)實值時，可以作為進(jìn)行連續(xù)計時的系統(tǒng)時鐘。定為一個自然數(shù)時，可作為系統(tǒng)計數(shù)器。表2是對時間表達(dá)式操作符的相關(guān)定義。

表2 操作符定義

+、-操作作用在兩個時間類型的值上返回一個時間類型的值；而×、÷(整除)操作將一個時間類型的值與一個整數(shù)相運算，主要用于實現(xiàn)對時間的翻倍或是減半；此外還有4個比較操作符(﹥、≧、﹤、≦)，其優(yōu)先級順序與RSL中的規(guī)定一致。

在RAISE的擴(kuò)展中，函數(shù)System主要用于獲取系統(tǒng)時間，假設(shè)該函數(shù)的執(zhí)行不消耗任何時間；Time時間類型實質(zhì)上是RSL固有類型Real的一個子類型，所以盡管定義了這樣一個Time時間類型和作用在其上的8種操作，卻不會改變RSL原有的語義結(jié)構(gòu)，這種擴(kuò)充符合最小化的要求。此擴(kuò)充的語法規(guī)范為：

type_expr ::=Unit | Bool | Int | Nat | Real |

Text | Char | Time |…

在對RSL語言進(jìn)行了如上擴(kuò)充后可解決信息傳輸中的等待時間問題和操作執(zhí)行時間問題。前者即超時問題，用當(dāng)前時間值減去開始等待時間值，如若結(jié)果超過某個設(shè)定值，即認(rèn)為出現(xiàn)超時問題，從而執(zhí)行對應(yīng)的超時出錯處理；后者即數(shù)據(jù)準(zhǔn)備和傳輸時間問題，該類問題要求一個操作必須在限定的時間值范圍內(nèi)完成，這一點可以通過比較操作執(zhí)行前后的系統(tǒng)時間值來準(zhǔn)確描述。

(2)wait表達(dá)式的添加

為了保證RSL語言擴(kuò)充后的廣譜性不被弱化，從而引入wait r表達(dá)式。整個wait r表達(dá)式的運算值為Unit，r是一個Time時間類型。運算出r的值之后，wait r表達(dá)式不做任何事情延時r個時間單位。

引入wait r表達(dá)式后，超時機(jī)制描述如下：

Class=

value Operation Unit → Unit

time_lim it Time

axiom

Operation( ) ≡

…… //具體操作

Wait time_lim it

…… //超時處理

end

在RSL語言中引入一個表示時間的類型和一個描述延遲的等待表達(dá)式后就形成Timed RAISE方法，其對應(yīng)語言用TRSL表示。引入wait r表達(dá)式之后，擴(kuò)充后的RSL語言廣譜性就不會被弱化，然而，這種擴(kuò)充可能會給RAISE原有確定語義帶來不確定性。因此，對于引入wait r表達(dá)式的RAISE方法的語法、語義，有必要重新定義和討論，在這里不再詳述。

3 C2-C3的描述驗證

一些指標(biāo)或量化參數(shù)常用來反映列車運行控制系統(tǒng)的性能，而這些參數(shù)基本上存在于某個場景或過程中，本文以等級轉(zhuǎn)換(C2-C3)場景為例，對域的場景交互一致性和實時性進(jìn)行具體的描述驗證。

3.1 域模型建立

C2-C3級間轉(zhuǎn)換場景中的時間約束[4]：

(1)GSM-R無線網(wǎng)絡(luò)注冊時間40 s；

(2)車載與無線閉塞中心的連接時間10 s；

(3)在ATP與RBC建立通信后，RBC與車載設(shè)備間必要信息的傳輸時間預(yù)估為20 s；

(4)進(jìn)行等級轉(zhuǎn)換前司機(jī)的確認(rèn)時間為5 s。

僅為說明該方法的有效性，對該場景進(jìn)行以下簡化：

①在該場景中，僅考慮車載ATP和RBC；

②認(rèn)為所有的延時或人為失誤都不存在，也就是說不需考慮司機(jī)確認(rèn)的時間約束；

③轉(zhuǎn)換中系統(tǒng)的所有設(shè)備都不發(fā)生故障；

④GSM-R中的所有通信過程最終都是可以完成的，對于上述(1)、(2)這兩個時間約束可以通過對GSM-R隨機(jī)時間的定義來滿足；

⑤上述(3)的時間約束在該場景中是一主要的不可忽略的考核指標(biāo)。

根據(jù)域的定義，針對C2-C3轉(zhuǎn)換場景，提出4個基本元素：輸入(I)、輸出(O)、函數(shù)(F)以及特性(T)。如圖2所示，ATP的等級、軌道電路區(qū)間占用等，在域函數(shù)的作用下，實現(xiàn)狀態(tài)的變換和操作，最終實現(xiàn)輸出。根據(jù)前述轉(zhuǎn)換過程，考慮主要時間約束條件，給出C2-C3狀態(tài)轉(zhuǎn)移如圖3所示。

圖2 等級轉(zhuǎn)換(C2-C3)場景域模型

圖3 等級轉(zhuǎn)換(C2-C3)場景狀態(tài)轉(zhuǎn)移

3.2 域的相關(guān)描述

根據(jù)等級轉(zhuǎn)換(C2-C3)域模型以及狀態(tài)轉(zhuǎn)移圖，對其關(guān)鍵進(jìn)行如下描述。

(1)輸入(I)：車載設(shè)備初始狀態(tài)A0，RBC初始狀態(tài)R0，與此同時，初態(tài)時信道中不存在已經(jīng)傳輸?shù)男畔ⅲ珹0到R1轉(zhuǎn)移時間為0。

(2)輸出(O)：車載設(shè)備最終狀態(tài)A3，RBC最終狀態(tài)R2。

(3)函數(shù)(F)：即圖5所示的狀態(tài)轉(zhuǎn)移圖。車載設(shè)備初始狀態(tài)A0、RBC初始狀態(tài)R0，通過域函數(shù)F的作用最終轉(zhuǎn)換為車載設(shè)備最終狀態(tài)A3、RBC最終狀態(tài)R2。

(4)特性(T)：實時性和交互一致性。

對等級轉(zhuǎn)換(C2-C3)場景域模型的RSL描述主要有車載設(shè)備、RBC以及消息集三個模塊的狀態(tài)描述。限于篇幅，僅對車載設(shè)備A0狀態(tài)和交互過程中涉及的消息集為例做以簡單說明。

車載設(shè)備A0狀態(tài)的RSL描述：

Send_CallRBC∶ATP×GNET→ATP×GNET

/*向RBC發(fā)送建立通信會話命令*/

Send_CallRBC(a，ch)≡

/*該式中”≡”表示恒等函數(shù)*/

wait NetworkRegDelay;

/*考慮網(wǎng)絡(luò)注冊時間*/

ATPSend(CallRBC(r));

/*ATP發(fā)送呼叫RBC信息*/

wait ComDelay

/*考慮傳輸延遲時間*/

wait BuildLinkDelay;

/*ATP與RBC建立連接，需等待一定延遲*/ change_state(A1);

/*ATP的下一個狀態(tài)為A1狀態(tài)*/

等級轉(zhuǎn)換(C2-C3)域模型消息集的RSL描述：

Message==

CallRBC(r)|Config(a)|MA(a)|

Pos(a)Pos&MAValue(a)|CallRBCAck(a)|

MAReq(r)|LevelTrain(a)|Level&Mode(a)

|nil|error

/*在切換過程中，涉及到車載配置參數(shù)、位置參數(shù)、MA請求參數(shù)信息、列車等級、列車模式、空包、錯誤包等消息集*/

3.3 驗證

在等級轉(zhuǎn)換 (C2-C3) 場景中，同時對場景實時性和交互一致性問題進(jìn)行驗證。整個驗證過程的簡易流程如圖4所示。

圖4 驗證流程

(1)場景交互一致性axiom模型

axiom

[C2-C3_consistent]

/*C2-C3交互一致性Timed RAISE描述*/

? a∶ATP， r∶RBC， ch∶GNET ?

/*a代表ATP， r代表RBC， ch代表GNET ? */

ATP_state(a)=A0 ^ RBC_state(r)=R0

/* ATP、RBC初始狀態(tài)分別為A0、R0*/

^RBCGet(r， ch)=nil^ATPGet(a，ch)=nil ^ TimePass (A0， R1)=0

/*初態(tài)時信道中不存在已經(jīng)傳輸?shù)男畔?，A0到R1轉(zhuǎn)移時間為0*/

?let (a′， r′,ch′)=run (a， r， ch) in

/*run( )是一個遍歷的函數(shù)*/

ATP_state(a′)=Aok ^

/*在遍歷條件下，達(dá)到ATP最終態(tài)Aok*/

RBC_state(r′)=Rok ^

/*在遍歷條件下，達(dá)到RBC最終態(tài)Rok*/

TimePass(R2， Rok)﹤=20

/*ATP向RBC發(fā)送位置報告的時間為20s*/

end

(2)實時性axiom模型

axiom

[TimeConstraininLevelTrains]

/*C2-C3實時性描述*/

TimePass(R1， Rok)=Time(R1)+Time(A1)+Time(R2)+Time(A3)

/*建立通信會話后，RBC與車載設(shè)備之間進(jìn)行必要信息的傳輸時間*/

在文獻(xiàn)[18]中重點推薦了9種證明方式：Equivalence(等價)、Inference(推演)、Lemma(引理)、Conclusion(結(jié)論)、Assumption(假設(shè))、Side(分支)、Axiom(公理)、Relevance(關(guān)聯(lián))以及Commented(非正式)[18]。在等級轉(zhuǎn)換(C2-C3)特性驗證的過程中，主要使用推斷規(guī)則(inference rules)和等價規(guī)則(equivalence rules)對實時性和場景交互一致性同時進(jìn)行驗證，當(dāng)且僅當(dāng)兩種驗證結(jié)果都為true時，方可認(rèn)為該場景沒有發(fā)生交互一致性的錯誤。通過驗證，結(jié)果表明該場景不會出現(xiàn)交互一致性錯誤，也不會違反時間的約束。

4 結(jié)論

高速鐵路列車運行控制系統(tǒng)是一個復(fù)雜的實時性系統(tǒng)，結(jié)合其實際特點，將域方法作為系統(tǒng)描述的切入。隨之使用Timed RAISE形式化方法對實時性較強(qiáng)的等級轉(zhuǎn)換(C2-C3)場景進(jìn)行描述和驗證，結(jié)果表明列車在等級轉(zhuǎn)換(C2-C3級)場景中，即使無線網(wǎng)絡(luò)GSM-R的隨機(jī)延遲會很大程度地影響場景的實時性，但依然能夠?qū)崿F(xiàn)規(guī)范中等級轉(zhuǎn)換作為(C2-C3級)場景的交互一致性和實時性要求。此外，將域方法和Timed RAISE結(jié)合推廣用于具有混成性、實時性、分布性的列控系統(tǒng)，可以實現(xiàn)對列控系統(tǒng)的整體性能驗證。

[1]李學(xué)偉.高速鐵路概論[M].北京:中國鐵道出版社，2010:10-14.

[2]車玉龍，蘇宏升.基于蒙特卡羅的CTCS-3級列控系統(tǒng)單元重要度分析[J].鐵道標(biāo)準(zhǔn)設(shè)計，2013(8):125-128.

[3]陳令儀.故障注入技術(shù)在CTCS-3級列控系統(tǒng)仿真測試平臺中的應(yīng)用研究[D].北京:北京交通大學(xué)，2011.

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

[5]康仁偉，王俊峰，呂繼東.基于UPPAAL的高鐵列控系統(tǒng)等級轉(zhuǎn)換過程建模與驗證[J].北京交通大學(xué)學(xué)報，2012，36(6):63-68.

[6]鐵道部科技技術(shù)司.科技運[2008]144號CTCS-3級列控系統(tǒng)應(yīng)答器應(yīng)用原則[S].北京：鐵道部科學(xué)技術(shù)司，2008.

[7]程憶佳.基于等級轉(zhuǎn)換場景的CTCS-3級列控數(shù)據(jù)完備性分析[D].北京:北京交通大學(xué)，2011.

[8]康仁偉，王俊峰，呂繼東.基于UPPAAL的高鐵列控系統(tǒng)等級轉(zhuǎn)換過程建模與驗證[J].鐵道標(biāo)準(zhǔn)設(shè)計，2012(6):63-68.

[9]徐田華.概率模型檢驗及其在列車運行控制系統(tǒng)中的應(yīng)用[D].北京：北京交通大學(xué)博士后出站報告，2007.

[10]IEC.IEC62279：2002. Railwayapplications-Communications， signa-

ling and processing systems-Software for railway control and protection systems[S]. IEC.2002.

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

[12]肖健宇，張德運，陳海診，等.模型檢測與定理證明相結(jié)合開發(fā)并驗證高可信嵌入式軟件[J].吉林大學(xué)學(xué)報：工學(xué)版，2005，35(5):531-537.

[13]宋海鋒.基于模型檢驗的RBC子系統(tǒng)測試分析方法研究[D].北京:北京交通大學(xué)，2014.

[14]鄭紅軍，張乃孝.軟件開發(fā)中的形式化方法[J].計算機(jī)科學(xué)，1997，24(6):90-96.

[15]謝雨飛.列控系統(tǒng)需求規(guī)范形式化建模與驗證方法研究[D].北京：北京交通大學(xué)，2012.

[16]曹源，唐濤，徐田華，等.形式化方法在列車運行控制系統(tǒng)中的應(yīng)用[J].交通運輸工程學(xué)報，2010，10(1):112-126.

[17]Xia Yong， Chris George. An operational semantics for timed RAISE[C]∥FM’99-Formal Methods. Springer Berlin/ Heidelberg, 1999：715-730.

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

Application of Timed RAISE Method in Level Conversion Scene of Train Control System

DING Chun-ping, CHEN Yong-gang

(School of Automation and Electrical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China)

The high-speed railway train control system is a complex real-time system. In the light of the actual features of the system, the domain method is employed for system modeling. With the analysis and comparison of model verification and theorem proving, the theorem-proving-based Timed RAISE (Timed Rigorous Approach to Industrial Software Engineering) is recommended to describe level transition scene (CTCS-2 to CTCS-3) and verify the scene interaction consistency and real-time capability. The results show that this scene will not cause errors in scene interactive consistency, nor violate time constraints.

High-speed railway； Timed RAISE； CTCS； Level transformation scene; Real-time capability； Scene interaction consistency

2014-11-17；

2014-12-17

國家自然科學(xué)基金地區(qū)項目(61164101)

丁春平(1989—)，女，碩士研究生，E-mail:dingchunping_1@163.com；陳永剛(1972—)，男，副教授，碩士研究生導(dǎo)師，主要研究方向:交通信息工程及控制。

1004-2954(2015)08-0164-05

U283

A

10.13238/j.issn.1004-2954.2015.08.035