基于Timed RAISE的高速列車RBC切換協(xié)議形式化建模及驗(yàn)證

徐世澤，肖　蒙

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

基于Timed RAISE的高速列車RBC切換協(xié)議形式化建模及驗(yàn)證

徐世澤，肖蒙

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

摘要：在CTCS-3(Chinese Train Control System Level 3)級(jí)列控系統(tǒng)中，RBC(Radio Block Center)切換是影響列車安全高效運(yùn)行的重要環(huán)節(jié)，現(xiàn)階段對(duì)RBC切換協(xié)議進(jìn)行驗(yàn)證分析所使用的形式化方法還存在狀態(tài)爆炸或描述性質(zhì)單一等問題?；赥imed RAISE的形式化方法，結(jié)合域的模型，在對(duì)RBC切換流程分析的基礎(chǔ)上，構(gòu)建狀態(tài)轉(zhuǎn)移圖，得到切換協(xié)議的形式化模型，使用等價(jià)和推斷的推理規(guī)則對(duì)模型的正確性和實(shí)時(shí)性進(jìn)行推理驗(yàn)證，得到的結(jié)果表明，RBC切換協(xié)議滿足規(guī)范標(biāo)準(zhǔn)對(duì)正確性與實(shí)時(shí)性的要求，將驗(yàn)證結(jié)果與其他文獻(xiàn)的結(jié)論進(jìn)行比較分析，說明該方法具有通用性，對(duì)于推廣其在列控系統(tǒng)場(chǎng)景驗(yàn)證中的應(yīng)用有一定的實(shí)際意義。

關(guān)鍵詞：列控系統(tǒng)；形式化方法；RBC切換協(xié)議；正確性與實(shí)時(shí)性

引言

中國列車控制系統(tǒng)(Chinese Train Control System， CTCS)是我國鐵路當(dāng)中控制列車安全運(yùn)行，提高列車行車效率的重要裝備。無線閉塞中心(Radio Block Center， RBC)作為CTCS-3級(jí)列控系統(tǒng)的重要組成部分，其安全性、可靠性直接影響列車的安全運(yùn)行。列控系統(tǒng)是一種復(fù)雜的安全苛求系統(tǒng)，無論是在標(biāo)準(zhǔn)和規(guī)范的制定過程當(dāng)中，或是在系統(tǒng)的開發(fā)和設(shè)計(jì)階段，都不可避免地會(huì)存在著一些系統(tǒng)的漏洞或安全隱患，在歐洲鐵路行業(yè)規(guī)范標(biāo)準(zhǔn)IEC61508-1中明確指出，對(duì)于高安全部件(安全完善度等級(jí)SIL4級(jí))，強(qiáng)烈推薦使用形式化方法進(jìn)行建模和驗(yàn)證[1]。因此，使用形式化方法對(duì)RBC切換協(xié)議進(jìn)行建模與驗(yàn)證是十分必要的。

文獻(xiàn)[2]采用時(shí)間自動(dòng)機(jī)理論對(duì)RBC的子系統(tǒng)進(jìn)行了形式化的描述，建立了相應(yīng)的網(wǎng)絡(luò)模型，運(yùn)用UPPAAL驗(yàn)證工具有效地證明了RBC子系統(tǒng)的安全性和受限活性，并對(duì)RBC切換的時(shí)間進(jìn)行了優(yōu)化。文獻(xiàn)[3]結(jié)合UML和微分動(dòng)態(tài)邏輯從列車混成性的角度對(duì)ETCS-2中的RBC交接場(chǎng)景進(jìn)行建模，最后驗(yàn)證了其正確性并且得到了列車運(yùn)行狀況和RBC離散控制時(shí)間共同影響RBC交接效率的結(jié)論。文獻(xiàn)[4]提出了一種基于列車主體性的RBC切換模型，由列車作為主體計(jì)算生成移動(dòng)授權(quán)，同時(shí)運(yùn)用Petri網(wǎng)對(duì)模型進(jìn)行了形式化建模與驗(yàn)證，最后結(jié)論表明，新的模型增強(qiáng)了列車運(yùn)行的安全性，提高了行車效率。文獻(xiàn)[5]使用UML結(jié)合可達(dá)集計(jì)算的形式化方法，對(duì)CTCS-3級(jí)列控系統(tǒng)的RBC交接場(chǎng)景進(jìn)行了建模和功能安全分析，分析的結(jié)果表明了UML與可達(dá)集計(jì)算相結(jié)合的方法適用于CTCS-3級(jí)列控系統(tǒng)的功能安全分析。上述文獻(xiàn)對(duì)于列控系統(tǒng)中形式化方法的應(yīng)用研究起到了積極的推動(dòng)作用，但是仍存在以下的問題：(1)現(xiàn)階段所使用的形式化驗(yàn)證方法較大部分都基于模型檢驗(yàn)，當(dāng)系統(tǒng)結(jié)構(gòu)較為復(fù)雜，多任務(wù)并發(fā)運(yùn)行時(shí)，系統(tǒng)狀態(tài)空間會(huì)出現(xiàn)指數(shù)級(jí)增長，導(dǎo)致狀態(tài)爆炸的問題；(2)列控系統(tǒng)由于其復(fù)雜的結(jié)構(gòu)，包含了實(shí)時(shí)性、并發(fā)性、混成性和反應(yīng)性等多種特性，目前所使用的基于定理證明的形式化方法都只針對(duì)了列控系統(tǒng)中的某一種特性，很難全面地描述和驗(yàn)證系統(tǒng)的全部特性。 在列控系統(tǒng)的結(jié)構(gòu)愈加復(fù)雜的情況下，對(duì)單一性質(zhì)的驗(yàn)證已不再適用，對(duì)高速鐵路列控系統(tǒng)全面有效的驗(yàn)證更能提高效率[6]。本文采用了Timed RAISE的形式化方法，對(duì)CTCS-3級(jí)列控系統(tǒng)規(guī)范中的RBC切換協(xié)議進(jìn)行建模，對(duì)系統(tǒng)模型的正確性和實(shí)時(shí)性進(jìn)行驗(yàn)證，將驗(yàn)證分析的結(jié)果與其他文獻(xiàn)的結(jié)論相比較，說明該方法的有效性。

1Timed RAISE形式化方法

Timed RAISE形式化方法包括了其規(guī)范語言RSL(RAISE Specification Language)和相應(yīng)的開發(fā)工具集。在RSL中有3個(gè)主要的要素：type、value和axiom。type定義了所有數(shù)據(jù)的類型，value定義了函數(shù)以及常量的值，axiom定義了value的屬性或者約束的規(guī)則，一般在axiom中，對(duì)所要驗(yàn)證的特性進(jìn)行描述[7，8]。通過對(duì)以上3個(gè)部分靈活的運(yùn)用和構(gòu)建，可以實(shí)現(xiàn)模塊化的建模方式以及對(duì)系統(tǒng)進(jìn)程化的描述，實(shí)現(xiàn)了對(duì)列控系統(tǒng)混成性、并發(fā)性和反應(yīng)性的支持。在RSL的不斷研究過程中，又加入了時(shí)間因子Time，對(duì)系統(tǒng)的實(shí)時(shí)性能夠很好地描述。Timed RAISE是基于定理證明的方法，使用數(shù)學(xué)邏輯來表示被驗(yàn)證的系統(tǒng)和所要驗(yàn)證的特性，可以用數(shù)學(xué)符號(hào)來描述具有無限狀態(tài)空間的系統(tǒng)[9]。因此，使用Timed RAISE形式化方法能夠更加全面深入的對(duì)列控系統(tǒng)進(jìn)行建模和驗(yàn)證。

使用RSL標(biāo)準(zhǔn)語言進(jìn)行建模與驗(yàn)證的框架圖如圖1所示。

圖1　建模與驗(yàn)證框架

首先，對(duì)系統(tǒng)需求規(guī)范進(jìn)行抽象，得到系統(tǒng)的域模型，使用RSL語言對(duì)系統(tǒng)域模型進(jìn)行描述，得到了由邏輯表達(dá)式、命題、定理等構(gòu)成的形式化模型。其次，使用RSL語言描述所要驗(yàn)證的系統(tǒng)性質(zhì)，將其表示為公理、定理的形式。最后在驗(yàn)證時(shí)，使用推理規(guī)則對(duì)命題、定理等進(jìn)行推理演繹，直至推導(dǎo)出最后的結(jié)果，判斷其是否滿足性質(zhì)的要求。

2RBC切換過程

列車在運(yùn)行過程當(dāng)中從當(dāng)前所處的RBC控制區(qū)域(移交RBC或RBC1)進(jìn)入了下一個(gè)RBC控制區(qū)域(接受RBC或RBC2)，列車的控制權(quán)限要進(jìn)行交接，這個(gè)過程就是RBC切換。RBC切換的過程可以分為雙電臺(tái)工作的情況和單電臺(tái)工作的情況，采用雙電臺(tái)工作時(shí)RBC切換的過程作為研究的重點(diǎn)，切換步驟如下[10]。

(1)列車通過切換預(yù)告應(yīng)答器組后，車載向RBC1發(fā)送列車位置報(bào)告，RBC1接到報(bào)告后向車載發(fā)送切換命令，同時(shí)向RBC2發(fā)送移交列車預(yù)告信息和進(jìn)路請(qǐng)求信息。

(2)當(dāng)RBC2接到進(jìn)路請(qǐng)求信息后，向RBC1發(fā)送進(jìn)路信息，RBC1根據(jù)得到的信息向車載發(fā)送延伸至RBC2區(qū)域的行車許可。

(3)車載根據(jù)RBC1提供的電話號(hào)碼，使用電臺(tái)2呼叫RBC2，呼叫成功則建立會(huì)話。

(4)當(dāng)列車最大安全前端越過邊界后，車載向RBC1和RBC2發(fā)送位置報(bào)告。之后，車載拒絕接受RBC1除終止會(huì)話信息之外的信息。同時(shí)，RBC2收到列車位置報(bào)告后向RBC1發(fā)送接管列車信息。

(5)當(dāng)列車最小安全末端越過邊界后，車載向RBC1和RBC2發(fā)送位置報(bào)告。RBC1接到位置報(bào)告后向車載發(fā)送切斷通信命令，車載接到切斷通信命令后，切斷與RBC1的通信連接。

(6)車載通過電臺(tái)2與RBC2保持通信會(huì)話并接受行車許可，監(jiān)控列車安全運(yùn)行，完成了RBC1到RBC2的切換。

3RBC切換協(xié)議的建模與驗(yàn)證

3.1域模型的建立

為了降低建模的難度，方便RSL語言進(jìn)行描述，首先建立系統(tǒng)的域模型。域是一類有著相同的性質(zhì)和功能的模型合集，可以將整個(gè)RBC切換的流程看作一個(gè)域，域模型的基本結(jié)構(gòu)如圖2所示。在域模型中，包括了3個(gè)基本的要素，輸入、輸出和函數(shù)，圖2中IN表示域的輸入，包括了列車和RBC的狀態(tài)，參數(shù)等，F(xiàn)(I)表示域函數(shù)，其中I表示域的輸入，即IN，O表示輸出，即OUT，這些輸入在域函數(shù)F的作用下，不斷發(fā)生改變，直至域的輸出OUT。列車和RBC之間不斷地進(jìn)行信息交互使得狀態(tài)發(fā)生變化，函數(shù)F表示了列車和RBC的狀態(tài)不斷遷移變化的過程。列車運(yùn)行以及RBC正常工作的過程都是在時(shí)間上連續(xù)的，以列車與RBC通信時(shí)信息的傳遞為分界，可以將整個(gè)連續(xù)的過程轉(zhuǎn)化為在時(shí)間上離散的過程，得到RBC切換協(xié)議的狀態(tài)轉(zhuǎn)移圖，如圖3所示。

圖3中RBC1為移交RBC，RBC2為接收RBC，豎線是時(shí)間的順序，方框中內(nèi)容是執(zhí)行的事件，圖中清晰地描述了2個(gè)相鄰的RBC在移交列車時(shí)，系統(tǒng)狀態(tài)的遷移變化過程。

圖2　域模型結(jié)構(gòu)

圖3　狀態(tài)轉(zhuǎn)移

3.2RSL模型的建立

根據(jù)圖3中RBC切換場(chǎng)景的狀態(tài)轉(zhuǎn)移過程以及需求標(biāo)準(zhǔn)對(duì)網(wǎng)絡(luò)傳輸?shù)难訒r(shí)要求[11]，建立RBC切換協(xié)議的RSL模型。為了方便建模，對(duì)圖3中的每一個(gè)狀態(tài)進(jìn)行了編號(hào)，R11表示RBC1的第一個(gè)狀態(tài)，T1表示列車的第一個(gè)狀態(tài)，R21表示RBC2的第一個(gè)狀態(tài)，其他與之類似。RSL模型由列車子模型Train、RBC1子模型、RBC2子模型和網(wǎng)絡(luò)傳輸子模型Delay組成，模型的描述具體如下。

1) 列車子模型

根據(jù)切換協(xié)議以及狀態(tài)轉(zhuǎn)移圖，建立列車的RSL模型Train，在Train模型中描述了列車發(fā)送位置報(bào)告，與RBC2建立通信等工作過程，具體的模型如下。

class

type

Train，

Train_state==T1| T2| T3| T4| T5| Tok| Terror

value

t：Train， r1，r2：RBC， g1，g2：NET

Train_def： Train×NET×NET→Train×NET×NET

Train_def(t，g1，g2)≡case state(t) of

T1→T1_work(t，g1)， T2→T2_work(t，g1，g2)

Tok→ (t，g1，g2)， Terror→ (t，g1，g2)

end

//T1state//

T1_work: Train×NET →Train×NET

T1_work(t，g1)≡Train_send(Loc_mes(t，r1)，g1);

change_state(T2)

//T2state//

T2_work: Train×NET ×NET→Train×NET×NET

T2_work(t，g1，g2)≡

let (mes，g1)=Train_get(g1) in case mes of

RBC_com(r1，t)→Train_send(RBC_call(t，r2)，g2);

change_state(T3)

nil→(t，g1，g2)， error→change_state(Terror)

end end

Train的模型中，Train_state表示列車的狀態(tài)，Tok是列車完成切換后的成功狀態(tài)，Terror是錯(cuò)誤的狀態(tài)。t，r1，r2，g1，g2分別表示列車，RBC1，RBC2和兩個(gè)車載電臺(tái)。Train_def表示列車在不同狀態(tài)時(shí)要執(zhí)行的動(dòng)作。在狀態(tài)T1中，Train_send表示列車發(fā)送位置報(bào)告Loc_mes，change_state表示列車的狀態(tài)遷移進(jìn)入了狀態(tài)T2。在狀態(tài)T2中，列車根據(jù)收到的消息Train_get判斷下一步的動(dòng)作，若收到切換命令RBC_com，那么列車向RBC2發(fā)送呼叫消息RBC_call，若收到空消息nil則不動(dòng)作，若收到錯(cuò)誤消息error則進(jìn)入錯(cuò)誤狀態(tài)Terror。列車其他狀態(tài)的模型與T1，T2相似，只是發(fā)送接受的消息不同，以T1，T2為例進(jìn)行說明，其他不再表述。

(2)RBC子模型

根據(jù)切換協(xié)議和狀態(tài)轉(zhuǎn)移圖，建立RBC的RSL模型，因?yàn)镽BC1和RBC2是同一類型設(shè)備，將兩者放在同一模塊中建模。RBC模型描述了RBC發(fā)送切換命令、進(jìn)路請(qǐng)求信息和行車許可等工作過程，具體模型如下。

class

type

RBC，

RBC1_state==R11| R12| R13| R14|

R15| R1ok| R1error

RBC2_state==R21| R22| R23| R24|

R25| R2ok| R2error

value

t: Train， r1，r2: RBC， g1，g2: NET

RBC1_def:RBC×NET →RBC×NET

RBC2_def:RBC×NET →RBC×NET

RBC1_def(r1，g1)≡case state(r1) of

R11→R11_work(r1，g1)， R1ok→ (r1，g1)，

R1error→ (r1，g1)

end

RBC2_def(r2，g2)≡case state(r2) of

R21→R21_work(r2，g2)， R2Fok→ (r2， g2)，

R2error→ (r2，g2)

end

//R11state//

R11_work: RBC×NET →RBC×NET

R11_work(r1，g1) ≡

let (mes，g1)=RBC1_get(g1) in case mes of

Loc_mes(t，r1) →RBC1_send(RBC_com(r1，t)) ||

RBC1_send_RBC2(Route_req(r1，r2));

change_state(R12)

nil→(r1，g1)， error→change_state(R1error)

end end

RBC的模型中，RBC1_state和RBC2_state分別表示兩個(gè)RBC的狀態(tài)，狀態(tài)的定義和設(shè)備的定義與列車子模型中的相同，在狀態(tài)R11中，RBC1若收到列車的位置報(bào)告Loc_mes，則向列車發(fā)送切換命令RBC_com，同時(shí)向RBC2發(fā)送進(jìn)路請(qǐng)求信息Route_req，若收到空消息則不動(dòng)作，若收到錯(cuò)誤消息error則進(jìn)入錯(cuò)誤狀態(tài)R1error，正確執(zhí)行動(dòng)作后進(jìn)入狀態(tài)R12。RBC1與RBC2的其他狀態(tài)模型與R11相似，以R11為例進(jìn)行說明，其他不再表述。

(3)網(wǎng)絡(luò)傳輸子模型

根據(jù)文獻(xiàn)[11]中對(duì)網(wǎng)絡(luò)傳輸時(shí)延的要求，建立網(wǎng)絡(luò)傳輸?shù)腞SL模型Delay。為了方便建模，將越區(qū)切換、鏈路中斷、突發(fā)降質(zhì)等因素造成的通信故障都簡化為信息傳輸?shù)难訒r(shí)，具體的模型如下。

type

Time，

Mes_delay={t：Time · 0.5

Build_delay={t：Time · 5

Reg_delay={t：Time · 15

TTI_delay={t：Time · 0

在Delay模型中，Mes_delay表示端到端信息傳輸?shù)难訒r(shí)時(shí)間，Build_delay表示連接建立的網(wǎng)絡(luò)延時(shí)，Reg_delay表示網(wǎng)絡(luò)注冊(cè)的延時(shí)時(shí)間，TTI_delay表示傳輸干擾帶來的網(wǎng)絡(luò)延時(shí)，時(shí)間都是以s為單位。

3.3RBC切換協(xié)議的驗(yàn)證

為了保證列車運(yùn)行的安全與效率，對(duì)RBC切換協(xié)議的要求是：在一定的時(shí)間內(nèi)，列車能夠安全可靠地完成RBC切換，并且不影響列車的行車效率。因此，對(duì)RBC切換協(xié)議的正確性和實(shí)時(shí)性進(jìn)行了驗(yàn)證。

(1)正確性驗(yàn)證

由域模型的分析可以得到，在圖3的狀態(tài)轉(zhuǎn)移圖中，T1，R11和R21三個(gè)初始狀態(tài)就是域模型的輸入，而T5，R15和R25三個(gè)最終狀態(tài)是域模型的輸出。列車安全可靠完成RBC切換的充分必要條件是：從域模型的輸入開始，經(jīng)過狀態(tài)的變遷，最終列車，RBC1和RBC2到達(dá)了域模型的輸出，即T5，R15和R25三個(gè)最終狀態(tài)，若在過程中，發(fā)生了系統(tǒng)死鎖，信息交互錯(cuò)誤，系統(tǒng)都會(huì)進(jìn)入錯(cuò)誤狀態(tài)，無法完成RBC切換。根據(jù)切換正確性的分析，運(yùn)用RSL語言對(duì)所驗(yàn)證性質(zhì)進(jìn)行描述，使用推理規(guī)則對(duì)正確性進(jìn)行驗(yàn)證，具體描述如下。

axiom

[Handover_correct]

? t∶Train， r1，r2∶RBC， g1，g2∶NET ·

Train_state(t)=T1 ∧ RBC1_state(r1)=R11 ∧

RBC2_state(r2)=R21 ∧ Train_get(t，g1，g2)=nil ∧

RBC1_get(r1，g1)=nil ∧ RBC2_get(r2，g2)=nil

? let (t’，r1’，r2’，g1’，g2’)=erg(t，r1，r2，g1，g2) in

Train_state(t’)=Tok ∧ RBC1_state(r1’)=R1ok ∧

RBC2_state(r2’)=R2ok

end

在正確性的RSL描述[Handover_correct]中，erg表示對(duì)整個(gè)系統(tǒng)狀態(tài)進(jìn)行遍歷，Train_state(t’)=Tok ∧ RBC1_state(r1’)=R1ok ∧ RBC2_state(r2’)=R2ok表示列車，RBC1和RBC2最終進(jìn)入了正確的狀態(tài)，同時(shí)也是最終要驗(yàn)證的目標(biāo)。

使用推理規(guī)則中的等價(jià)規(guī)則(equivalence rules)和推斷規(guī)則(inference rules)，結(jié)合列車子模型和RBC子模型，對(duì)正確性的RSL描述進(jìn)行推理演繹，經(jīng)過整理最終得到了下面的表達(dá)式。

Train_state(t’)=Tok∧RBC1_state(r1’)=R1ok∧

(1)

式(1)表明列車，RBC1和RBC2經(jīng)過狀態(tài)遷移最終進(jìn)入了正確的狀態(tài)，即列車能夠安全可靠的完成RBC的切換。結(jié)果說明了RBC切換協(xié)議滿足系統(tǒng)對(duì)于切換正確性的要求。

(2)實(shí)時(shí)性驗(yàn)證

文獻(xiàn)[11]中規(guī)定，列車注冊(cè)下一RBC分區(qū)的時(shí)間必須在 40s內(nèi)完成。假設(shè)列車以300km/h的速度運(yùn)行，且列車長度為400m，則從列車前端通過切換點(diǎn)，到列車末端通過切換點(diǎn)共需要4.8s時(shí)間，則總共RBC切換的時(shí)間為44.8s，當(dāng)RBC切換時(shí)間大于44.8s，則會(huì)影響列車的行車效率。運(yùn)用RSL語言對(duì)RBC切換的實(shí)時(shí)性要求進(jìn)行描述，使用推理規(guī)則對(duì)實(shí)時(shí)性進(jìn)行驗(yàn)證，具體描述如下。

axiom

[Handover_time]

Time_totle=Time_pass(T1)+Time_pass(R11)+

Time_pass(T2)+Time_pass(R22)+Time_pass(T4)

?Time_totle≤ 44.8

其中，Time_pass表示在狀態(tài)內(nèi)的信息交互，網(wǎng)絡(luò)注冊(cè)等所需要的時(shí)間，Time_totle≤ 44.8是最終要驗(yàn)證的目標(biāo)。

與驗(yàn)證RBC切換正確性的過程相同，使用推理規(guī)則，結(jié)合列車子模型和RBC子模型對(duì)實(shí)時(shí)性的RSL描述進(jìn)行推理演繹，最終得到下面的表達(dá)式。

(2)

式(2)表明，在正常的網(wǎng)絡(luò)狀況下，RBC切換的時(shí)間小于44.8 s，即列車能夠在要求的時(shí)間內(nèi)完成切換，說明了RBC切換協(xié)議滿足系統(tǒng)對(duì)于實(shí)時(shí)性的要求。

(3)文獻(xiàn)比較分析

對(duì)于RBC切換正確性的驗(yàn)證，文獻(xiàn)[12，13]分別采用了通信順序進(jìn)程和Petri網(wǎng)兩種形式化方法對(duì)RBC切換過程進(jìn)行了驗(yàn)證，采用的切換協(xié)議與本文相同，最后驗(yàn)證的結(jié)果都表明切換協(xié)議的正確性滿足系統(tǒng)的要求，這與本文的研究結(jié)果一致。

在不同網(wǎng)絡(luò)質(zhì)量的情況下，對(duì)RBC切換過程的實(shí)時(shí)性進(jìn)行驗(yàn)證，驗(yàn)證的結(jié)果與文獻(xiàn)[14]相比較，如表1所示。

表1　驗(yàn)證結(jié)果比較

表1中，“實(shí)時(shí)性驗(yàn)證”是本文得到的驗(yàn)證結(jié)果，結(jié)果顯示，在網(wǎng)絡(luò)質(zhì)量為60%、70%和80%時(shí)，切換過程不滿足實(shí)時(shí)性的要求，由于RSL模型是由數(shù)學(xué)邏輯表達(dá)式構(gòu)成的，所以得到的結(jié)果為布爾值?！扒袚Q時(shí)間”是文獻(xiàn)[14]中，經(jīng)過仿真運(yùn)行得到的RBC切換時(shí)間的數(shù)據(jù)，在網(wǎng)絡(luò)質(zhì)量為60%、70%和80%時(shí)，切換的時(shí)間分別為55.1、52.8 s和45.8 s，都大于44.8 s，不符合實(shí)時(shí)性的要求，這與本文研究結(jié)果一致。當(dāng)網(wǎng)絡(luò)質(zhì)量為90%和100%時(shí)，兩者的驗(yàn)證結(jié)果同樣相同。

通過以上的比較分析，證明了Timed RAISE方法能夠全面有效地對(duì)系統(tǒng)協(xié)議進(jìn)行建模與驗(yàn)證，說明了該方法適合于CTCS-3級(jí)列控系統(tǒng)場(chǎng)景的形式化建模與驗(yàn)證分析。

4結(jié)論

在現(xiàn)階段針對(duì)鐵路列控系統(tǒng)進(jìn)行形式化驗(yàn)證的方法中，還存在著狀態(tài)爆炸和描述性質(zhì)單一等問題，這大大制約了形式化方法的應(yīng)用范圍，基于定理證明的Timed RAISE方法不會(huì)產(chǎn)生狀態(tài)爆炸的問題，同時(shí)能夠更加全面的驗(yàn)證整個(gè)系統(tǒng)。本文首先分析了RBC切換協(xié)議的整個(gè)過程，為了降低建模難度，使用了域的方法對(duì)切換協(xié)議進(jìn)行了抽象建模，得到了相應(yīng)的域模型，然后使用RSL標(biāo)準(zhǔn)語言對(duì)域模型進(jìn)行描述，建立了切換協(xié)議的形式化模型，最后對(duì)切換協(xié)議的正確性和實(shí)時(shí)性進(jìn)行了形式化描述，并使用相關(guān)的推理規(guī)則進(jìn)行推理演繹，得到了驗(yàn)證的結(jié)果，結(jié)果表明RBC切換協(xié)議滿足相關(guān)的安全性和實(shí)時(shí)性的要求。將驗(yàn)證結(jié)果與其他文獻(xiàn)的結(jié)論進(jìn)行比較分析，說明了該方法的有效性，對(duì)于推廣其在列控領(lǐng)域場(chǎng)景驗(yàn)證中的應(yīng)用有一定的實(shí)際意義。

參考文獻(xiàn)：

[1]BOWEN J P. Formal Methods in Safety-Critical Standards[C]∥Software Engineering Standards Symposium. Brighton: IEEE Computer Society Press， 1993:168-177.

[2]呂繼東，唐濤，賈昊.客運(yùn)專線CTCS-3級(jí)列控系統(tǒng)無線閉塞中心的建模與驗(yàn)證[J].鐵道學(xué)報(bào)，2010，32(6):34-42.

[3]劉金濤，唐濤，趙林，等.基于微分動(dòng)態(tài)邏輯的無線閉塞中心交接協(xié)議建模與驗(yàn)證[J].中國鐵道科學(xué)，2012，33(5):98-104.

[4]潘登，梅萌，鄭應(yīng)平.基于列車主體性的RBC越區(qū)切換模型[J].交通運(yùn)輸系統(tǒng)工程與信息，2013，13(4):134-141.

[5]劉金濤，唐濤，趙林，等.基于UML模型的CTCS-3級(jí)列控系統(tǒng)功能安全分析方法[J].鐵道學(xué)報(bào)，2013，35(10):59-66.

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

[7]顧翔，邱建林，邵浩然.基于RSL的協(xié)議形式化描述與驗(yàn)證方法[J].計(jì)算機(jī)工程，2009，35(23):41-43.

[8]Xiang Gu， Jianlin Qiu. Describing Protocol Elements and Protocols with RSL[C]//Advances in Information Technology and Industry Applications. Berlin: Springer， 2012：741-748.

[9]章珍珍.高速磁浮運(yùn)控系統(tǒng)運(yùn)行場(chǎng)景的RSL建模與驗(yàn)證[D].北京:北京交通大學(xué)，2013.

[10]李偉.基于有色Petri網(wǎng)的無線閉塞中心子系統(tǒng)切換建模與驗(yàn)證[D].北京:北京交通大學(xué)，2009.

[11]鐵道部.科技運(yùn)[2008]168號(hào)CTCS-3級(jí)列控系統(tǒng)GSM-R網(wǎng)絡(luò)需求規(guī)范(v1.0)[S].北京:中國鐵道出版社，2008.

[12]呂繼東，唐濤.高速鐵路列控系統(tǒng)運(yùn)營場(chǎng)景實(shí)時(shí)性的建模與驗(yàn)證[J].鐵道學(xué)報(bào)，2011，33(6):54-61.

[13]張友兵，唐濤.基于有色petri網(wǎng)的CTCS-3級(jí)列控系統(tǒng)RBC切換的建模與形式化分析[J].鐵道學(xué)報(bào)，2012，34 (7):49-55.

[14]楊柳倩.基于UML和有色Petri網(wǎng)的RBC切換建模與分析[D].蘭州:蘭州交通大學(xué)，2012.

The Formal Modeling and Verification of RBC HandoverProtocol for High-speed Train Based on Timed RAISE

XU Shi-ze， XIAO Meng

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

Abstract：In the CTCS-3-based train control system， the Radio Block Center (RBC) handover is an important part closely related to train safety and efficiency. The formal methods used for verifying and analyzing train control system tend to have some problems such as state explosion and singularity of description. Based on the analysis of RBC handover， the Domain method merging with Timed RAISE formal is applied to construct state transition diagram and obtain the formal model of handover protocol， and the inference rules are used to verify the correctness and real time of handover protocol. The result shows that the protocol satisfies the requirements for correctness and real time. The verification results are compared with other literatures and proved to be suitable for scene verification in train control system.

Key words：Train control system; Formal method; RBC handover protocol; Correctness and real time

中圖分類號(hào)：TP301.2

文獻(xiàn)標(biāo)識(shí)碼：A

DOI:10.13238/j.issn.1004-2954.2015.06.031

文章編號(hào)：1004-2954(2015)06-0138-05

作者簡介：徐世澤(1989—)，男，碩士研究生，E-mail：348510010@qq.com。

收稿日期：2014-12-15； 修回日期：2014-01-12