陳永剛，丁春平

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

?

基于TRSL的RBC等級轉(zhuǎn)換場景研究

陳永剛，丁春平

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

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

列車運行控制系統(tǒng)；RBC等級轉(zhuǎn)換；TRSL；場景切換正確性

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

形式化方法可以精準(zhǔn)地表述系統(tǒng)結(jié)構(gòu)、行為、特征以及時間要求等，用形式化方法描述系統(tǒng)需求規(guī)范要求，可以最大程度地找出其他方法中忽視的錯誤和缺陷，同時還可以運用嚴(yán)格的數(shù)學(xué)邏輯實現(xiàn)對系統(tǒng)特性的驗證分析，來判斷系統(tǒng)特性是否成立[5]。

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

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

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

1　TRSL介紹

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

TRSL依賴數(shù)學(xué)邏輯來表達(dá)系統(tǒng)結(jié)構(gòu)和驗證特性，由于高鐵列控系統(tǒng)結(jié)構(gòu)復(fù)雜、規(guī)模龐大，直接使用形式化方法描述驗證，不僅成本需求高，而且驗證效率也會有一定程度的降低，故而引入域方法實現(xiàn)系統(tǒng)模塊的劃分，整個驗證框架如圖1所示。

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

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

2　RBC等級轉(zhuǎn)換分析

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

2.1構(gòu)建信息交互圖

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

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

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

圖3　C2-C3級RBC等級轉(zhuǎn)換信息交互圖

圖4　C3-C2級RBC等級轉(zhuǎn)換信息交互圖

2.2建立狀態(tài)轉(zhuǎn)移圖

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

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

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

3　形式化建模

3.1建立域模型

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

圖5　RBC等級轉(zhuǎn)換狀態(tài)轉(zhuǎn)移圖

RBC等級轉(zhuǎn)換的實質(zhì)是通過車載和地面間持續(xù)不斷的信息交互傳遞，使設(shè)備的狀態(tài)不斷遷移發(fā)生變化，最終實現(xiàn)等級的轉(zhuǎn)換。將RBC等級轉(zhuǎn)換過程看作是一個域，得到域結(jié)構(gòu)模型如圖6所示。

圖6　RBC等級轉(zhuǎn)換域結(jié)構(gòu)模型

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

3.2域模型到TRSL模型的轉(zhuǎn)化

RBC等級轉(zhuǎn)換域模型描述了系統(tǒng)的抽象靜態(tài)結(jié)構(gòu)，只有匹配動態(tài)行為后才可完成系統(tǒng)完整表述，而且域模型特性T的驗證最終是要使用形式化方法TRSL來實現(xiàn)，因而需要實現(xiàn)域模型到TRSL描述的轉(zhuǎn)化。

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

class

type

RBC∶Nat

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

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

/*RBC_state類型包含八種狀態(tài)值*/

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

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

RBC_next(r，gr) ≡

/*函數(shù)RBC_next用來決定RBC的下一個狀態(tài)*/

case state(r) of

/*判斷RBC在哪一個狀態(tài)*/

R1→R1execute-task(r，gr)

/*若RBC在R1狀態(tài)時要執(zhí)行R1內(nèi)所有事件*/

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

/*如果在成功或錯誤狀態(tài)，則不發(fā)生變化*/

end

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

R2execute-task(r，gr) ≡

/*R2狀態(tài)執(zhí)行事件*/

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

/*通過函數(shù)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收到列車數(shù)據(jù)消息data_train(vh，r)，則向vh發(fā)送位置報告請求參數(shù)Loca_req(r，vh)并傳輸MA請求參數(shù)信息MA_req(r，vh)*/

wait transfernews_time; state_change(R3)

/*等待端到端傳輸時延后，r遷入R3狀態(tài)*/

nil→(r，gr)

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

error→state_change(Rerror)

/*如果收到error消息，轉(zhuǎn)移進入Rerror狀態(tài)*/

end

在設(shè)備狀態(tài)和狀態(tài)間轉(zhuǎn)移的表述中，使用TRSL中的“||”和“;”操作符實現(xiàn)對系統(tǒng)并發(fā)、順序事件的描述，與此同時，利用type、value定義來對列控系統(tǒng)無線網(wǎng)絡(luò)QoS指標(biāo)參數(shù)[19]做以說明，具體使用時，采用wait e表達(dá)式來表述。例如，車地間連接建立的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，數(shù)字特性使用“∑”、“<”、“+”等各種數(shù)學(xué)運算符將其表述成axiom形式進行規(guī)約，狀態(tài)特性采用邏輯符號“^”轉(zhuǎn)化成Bool類型進行識別，如下規(guī)約了C2-C3轉(zhuǎn)換場景交互正確性要求和部分時間特性約束。

axiom

[correctness_C2-C3]

/*C2-C3級間轉(zhuǎn)換正確性公理*/

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

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

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

/*定義vh和r的初始狀態(tài)*/

vehicle_gain(vh，gr)=nil ∧

RBC_obtain(r，gr)=nil ∧

/*初態(tài)時信道中不存在任何信息*/

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

/* Tra 是一個狀態(tài)遍歷函數(shù)*/

vehicle_state(vh')=Vhok∧

RBC_state(r')=Rok∧

/*在遍歷條件下，達(dá)到vh、r最終態(tài)Vhok和Rok*/

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

/*車載和RBC交換數(shù)據(jù)的時間預(yù)估為20s*/

TotleT2-expend(Vh1，Vhok)<=80

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

[realtime_C2-C3]

/*C2-C3級間轉(zhuǎn)換實時性公理*/

TotleT1-expend(R3，Rok)=

/*車載和RBC交換數(shù)據(jù)的時間統(tǒng)計*/

TotleT2-expend(Vh1，Vhok)=

/*從GSM-R注冊到完成轉(zhuǎn)換時的時間統(tǒng)計*/

3.3RBC等級轉(zhuǎn)換的驗證

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

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

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

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

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

(1)

(2)

當(dāng)式(1)的切換正確性和式(2)的實時性驗證結(jié)果都為true時，才表明系統(tǒng)設(shè)備能夠在規(guī)定的時間內(nèi)實現(xiàn)C2到C3的轉(zhuǎn)換。

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

(3)

(4)

只有vh和r均順利達(dá)到成功態(tài)時才能說明能夠完成轉(zhuǎn)換。為了實現(xiàn)狀態(tài)的遷移，使用了函數(shù)Tra通過next借助函數(shù)finished來執(zhí)行操作遍歷。

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

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

(5)

else Tra(vh',gr') end

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

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

(6)

根據(jù)axiom初始化賦值以及推斷規(guī)則，等價為執(zhí)行Vh1execute-task(vh，gr)，再依據(jù)推斷規(guī)則，等效為執(zhí)行Vh1狀態(tài)內(nèi)所有事件。操作結(jié)束后vh轉(zhuǎn)入Ve2狀態(tài)，接著使用值代入將結(jié)果代入式(5)中，依據(jù)推斷規(guī)則將執(zhí)行式(7)

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

(7)

由于vh目前轉(zhuǎn)入Ve2狀態(tài)，未達(dá)到finished函數(shù)中定義的結(jié)束態(tài)，故而可得到式(8)

(8)

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

(9)

(10)

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

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

(11)

(12)

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

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

(13)

(14)

(15)

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

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

4　結(jié)論

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

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

[2]趙顯瓊，唐濤.多端日形式化測試自動生成方法在CTCS-3車載系統(tǒng)中的應(yīng)用[J].鐵道學(xué)報，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]呂繼東.列車運行控制系統(tǒng)分層形式化建模與驗證分析[D].北京:北京交通大學(xué)，2011:1-22.

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

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

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

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

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

[11]李黎.混成系統(tǒng)的描述和設(shè)計與Timed RAISE項目[J].計算機科學(xué)，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方法在列控系統(tǒng)等級轉(zhuǎn)換場景中的應(yīng)用研究[J].鐵道標(biāo)準(zhǔn)設(shè)計，2015，59(8):164-169.

[15]鐵道部科技司.CTCS-3級列控系統(tǒng)標(biāo)準(zhǔn)規(guī)范—CTCS-3級列控系統(tǒng)系統(tǒng)功能需求規(guī)范(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級列控系統(tǒng)等級轉(zhuǎn)換運營場景智能形式化研究[D].蘭州:蘭州交通大學(xué)，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級列車運行控制系統(tǒng)[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

國家自然科學(xué)基金(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