丁春平,陳永剛

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

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

丁春平,陳永剛

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

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

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

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

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

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

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

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

1.2 C2-C3級(jí)間轉(zhuǎn)換過(guò)程

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

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

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

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

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

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

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

2 Timed RAISE

2.1 形式化方法概述

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

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

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

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

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

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

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

2.2 Timed RAISE

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

(1)Time類型的添加

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

Type

Time //定義時(shí)間類型Time

Value

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

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

表2 操作符定義

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

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

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

Text | Char | Time |…

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

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

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

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

Class=

value Operation Unit → Unit

time_lim it Time

axiom

Operation( ) ≡

…… //具體操作

Wait time_lim it

…… //超時(shí)處理

end

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

3 C2-C3的描述驗(yàn)證

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

3.1 域模型建立

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

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

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

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

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

僅為說(shuō)明該方法的有效性，對(duì)該場(chǎng)景進(jìn)行以下簡(jiǎn)化：

①在該場(chǎng)景中，僅考慮車載ATP和RBC；

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

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

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

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

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

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

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

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

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

(1)輸入(I)：車載設(shè)備初始狀態(tài)A0，RBC初始狀態(tài)R0，與此同時(shí)，初態(tài)時(shí)信道中不存在已經(jīng)傳輸?shù)男畔ⅲ珹0到R1轉(zhuǎn)移時(shí)間為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，通過(guò)域函數(shù)F的作用最終轉(zhuǎn)換為車載設(shè)備最終狀態(tài)A3、RBC最終狀態(tài)R2。

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

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

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

Send_CallRBC∶ATP×GNET→ATP×GNET

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

Send_CallRBC(a，ch)≡

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

wait NetworkRegDelay;

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

ATPSend(CallRBC(r));

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

wait ComDelay

/*考慮傳輸延遲時(shí)間*/

wait BuildLinkDelay;

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

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

等級(jí)轉(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

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

3.3 驗(yàn)證

在等級(jí)轉(zhuǎn)換 (C2-C3) 場(chǎng)景中，同時(shí)對(duì)場(chǎng)景實(shí)時(shí)性和交互一致性問(wèn)題進(jìn)行驗(yàn)證。整個(gè)驗(yàn)證過(guò)程的簡(jiǎn)易流程如圖4所示。

圖4 驗(yàn)證流程

(1)場(chǎng)景交互一致性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)時(shí)信道中不存在已經(jīng)傳輸?shù)男畔?，A0到R1轉(zhuǎn)移時(shí)間為0*/

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

/*run( )是一個(gè)遍歷的函數(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ā)送位置報(bào)告的時(shí)間為20s*/

end

(2)實(shí)時(shí)性axiom模型

axiom

[TimeConstraininLevelTrains]

/*C2-C3實(shí)時(shí)性描述*/

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

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

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

4 結(jié)論

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

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

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

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

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

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

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

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

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

[9]徐田華.概率模型檢驗(yàn)及其在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[D].北京：北京交通大學(xué)博士后出站報(bào)告，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]肖健宇，張德運(yùn)，陳海診，等.模型檢測(cè)與定理證明相結(jié)合開發(fā)并驗(yàn)證高可信嵌入式軟件[J].吉林大學(xué)學(xué)報(bào)：工學(xué)版，2005，35(5):531-537.

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

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

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

[16]曹源，唐濤，徐田華，等.形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J].交通運(yùn)輸工程學(xué)報(bào)，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

國(guó)家自然科學(xué)基金地區(qū)項(xiàng)目(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