徐世澤，肖　蒙

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

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

徐世澤，肖蒙

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

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

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

引言

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

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

1Timed RAISE形式化方法

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

使用RSL標準語言進行建模與驗證的框架圖如圖1所示。

圖1　建模與驗證框架

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

2RBC切換過程

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

(1)列車通過切換預告應答器組后，車載向RBC1發(fā)送列車位置報告，RBC1接到報告后向車載發(fā)送切換命令，同時向RBC2發(fā)送移交列車預告信息和進路請求信息。

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

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

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

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

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

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

3.1域模型的建立

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

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

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

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

3.2RSL模型的建立

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

1) 列車子模型

根據(jù)切換協(xié)議以及狀態(tài)轉(zhuǎn)移圖，建立列車的RSL模型Train，在Train模型中描述了列車發(fā)送位置報告，與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是錯誤的狀態(tài)。t，r1，r2，g1，g2分別表示列車，RBC1，RBC2和兩個車載電臺。Train_def表示列車在不同狀態(tài)時要執(zhí)行的動作。在狀態(tài)T1中，Train_send表示列車發(fā)送位置報告Loc_mes，change_state表示列車的狀態(tài)遷移進入了狀態(tài)T2。在狀態(tài)T2中，列車根據(jù)收到的消息Train_get判斷下一步的動作，若收到切換命令RBC_com，那么列車向RBC2發(fā)送呼叫消息RBC_call，若收到空消息nil則不動作，若收到錯誤消息error則進入錯誤狀態(tài)Terror。列車其他狀態(tài)的模型與T1，T2相似，只是發(fā)送接受的消息不同，以T1，T2為例進行說明，其他不再表述。

(2)RBC子模型

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

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分別表示兩個RBC的狀態(tài)，狀態(tài)的定義和設備的定義與列車子模型中的相同，在狀態(tài)R11中，RBC1若收到列車的位置報告Loc_mes，則向列車發(fā)送切換命令RBC_com，同時向RBC2發(fā)送進路請求信息Route_req，若收到空消息則不動作，若收到錯誤消息error則進入錯誤狀態(tài)R1error，正確執(zhí)行動作后進入狀態(tài)R12。RBC1與RBC2的其他狀態(tài)模型與R11相似，以R11為例進行說明，其他不再表述。

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

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

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時間，Build_delay表示連接建立的網(wǎng)絡延時，Reg_delay表示網(wǎng)絡注冊的延時時間，TTI_delay表示傳輸干擾帶來的網(wǎng)絡延時，時間都是以s為單位。

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

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

(1)正確性驗證

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

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表示對整個系統(tǒng)狀態(tài)進行遍歷，Train_state(t’)=Tok ∧ RBC1_state(r1’)=R1ok ∧ RBC2_state(r2’)=R2ok表示列車，RBC1和RBC2最終進入了正確的狀態(tài)，同時也是最終要驗證的目標。

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

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

(1)

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

(2)實時性驗證

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

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)絡注冊等所需要的時間，Time_totle≤ 44.8是最終要驗證的目標。

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

(2)

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

(3)文獻比較分析

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

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

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

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

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

4結(jié)論

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

參考文獻：

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

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

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

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

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

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

[7]顧翔，邱建林，邵浩然.基于RSL的協(xié)議形式化描述與驗證方法[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]章珍珍.高速磁浮運控系統(tǒng)運行場景的RSL建模與驗證[D].北京:北京交通大學，2013.

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

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

[12]呂繼東，唐濤.高速鐵路列控系統(tǒng)運營場景實時性的建模與驗證[J].鐵道學報，2011，33(6):54-61.

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

[14]楊柳倩.基于UML和有色Petri網(wǎng)的RBC切換建模與分析[D].蘭州:蘭州交通大學，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

中圖分類號：TP301.2

文獻標識碼：A

DOI:10.13238/j.issn.1004-2954.2015.06.031

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

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

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