基于MSC與UPPAAL的列控系統(tǒng)等級轉(zhuǎn)換場景形式化驗證

胡雪蓮,陶彩霞

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

?

基于MSC與UPPAAL的列控系統(tǒng)等級轉(zhuǎn)換場景形式化驗證

胡雪蓮,陶彩霞

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

摘要：等級轉(zhuǎn)換是C3級列控系統(tǒng)的重要場景,是列控系統(tǒng)兼容性的集中體現(xiàn),轉(zhuǎn)換的成功與否直接關系到列車的運行安全和行車效率。因此,有必要對設計規(guī)范中所描述的轉(zhuǎn)換過程進行形式化建模和驗證,以保障系統(tǒng)的安全性和實時性。為保證設計規(guī)范與所建模型的一致性,采取消息順序圖(MSC)與時間自動機相結(jié)合的方式,建立等級轉(zhuǎn)換場景中C2級向C3級轉(zhuǎn)換過程的MSC模型,并將其轉(zhuǎn)換為時間自動機模型。應用UPPAAL對模型的安全性和受限活性進行仿真驗證,結(jié)果表明設計規(guī)范中所描述的轉(zhuǎn)換過程是安全可靠的,可以滿足C3級列控系統(tǒng)的兼容性和安全性要求。

關鍵詞：CTCS；等級轉(zhuǎn)換； MSC；時間自動機； UPPAAL；建模

1概述

中國列車運行控制系統(tǒng)(CTCS)按照不同的功能和設備配置分為5個應用等級，即CTCS-0至CTCS-4級(以下簡稱C0級～C4級)[1]，其中C3級是基于GSM-R無線通信并采用軌道電路等方式檢查列車占用的控制系統(tǒng)，它可以疊加在C2級列控系統(tǒng)上，實現(xiàn)上下線運行，即同時能夠在C2和C3區(qū)段的線路運行，列車在運行過程中需要進行等級轉(zhuǎn)換[2]。

C2級列控系統(tǒng)適用于時速200～250 km的列車，C3級列控系統(tǒng)適用于時速300～350 km的列車[3]，二者在傳輸方式、控制原理、設備構(gòu)成等方面存在很大差異[4]，等級轉(zhuǎn)換的成功與否直接關系到列車的行車效率和運行安全。因而，對C3級列控系統(tǒng)標準規(guī)范[5]所描述的等級轉(zhuǎn)換場景進行建模，驗證系統(tǒng)的安全性和功能屬性，對輔助系統(tǒng)開發(fā)十分必要。由于自然語言的模糊性和二義性，直接對其描述的等級轉(zhuǎn)換場景建立形式化模型，必然會對系統(tǒng)描述和模型的一致性產(chǎn)生影響。將半形式化方法與形式化方法相結(jié)合，以等級轉(zhuǎn)換場景中較為復雜的C2級向C3級的轉(zhuǎn)換過程為例，先建立MSC模型，描述系統(tǒng)的消息交互行為，然后將其轉(zhuǎn)換為時間自動機模型，并利用UPPAAL驗證工具對系統(tǒng)的安全性和受限活性進行驗證。

2等級轉(zhuǎn)換過程描述

當列車從C2線路進入C3線路時，為了提高運行效率，列控系統(tǒng)需從C2級轉(zhuǎn)換至C3級。等級邊界應答器及司機確認區(qū)設置如圖1所示，轉(zhuǎn)換過程主要分為以下3步。

圖1　等級邊界應答器及司機確認區(qū)設置

(1)建立通信：GSM-R為唯一網(wǎng)絡時，列車自動連接到GSM-R網(wǎng)絡，當GSM-R網(wǎng)絡與其他網(wǎng)絡并存時，列車通過GSM-R網(wǎng)絡連接應答器組(GRL)注冊到GSM-R網(wǎng)絡，車載設備與GSM-R網(wǎng)絡建立連接后，通過RBC連接應答器組(RL)建立與RBC的通信會話。

(2)數(shù)據(jù)交換：車載設備和RBC建立無線通信連接后，RBC向列車發(fā)送請求參數(shù)信息，列車通過轉(zhuǎn)換預告應答器組(YG)后，向RBC發(fā)送準確的列車進路位置及當前等級和模式信息，RBC根據(jù)以上信息及C3級控制區(qū)域聯(lián)鎖進路條件，向列車發(fā)送行車許可及等級轉(zhuǎn)換命令。

(3)執(zhí)行轉(zhuǎn)換：列車具備等級轉(zhuǎn)換條件后，根據(jù)RBC傳送的等級轉(zhuǎn)換命令，車載設備請求司機確認即將執(zhí)行的等級轉(zhuǎn)換，司機應在規(guī)定時間確認轉(zhuǎn)換，列車根據(jù)轉(zhuǎn)換執(zhí)行應答器組(ZX)發(fā)送的信息，自動由C2級列控系統(tǒng)轉(zhuǎn)換到C3級列控系統(tǒng)控車。

當列車已經(jīng)與RBC建立了通信連接后，進入了不通往C3線路的分支進路，需要更改等級轉(zhuǎn)換計劃，分為以下兩種情況：

(1)列車經(jīng)過RBC連接應答器組(RL)后進入不通往C3級線路的分支進路，在此線路上應設置命令列車關閉通信會話的應答器組(RT)；

(2)列車經(jīng)過轉(zhuǎn)換預告應答器組(YG)后，受線路條件限制，需進入C2級線路支路進路，在此線路上需設置等級轉(zhuǎn)換終止應答器組(LTT)，列車前端經(jīng)過該點后取消原轉(zhuǎn)換命令，列車繼續(xù)維持C2級列控系統(tǒng)工作[5，6]。

3等級轉(zhuǎn)換過程建模

3.1基于MSC的系統(tǒng)建模

MSC是一種用來直觀描述并行系統(tǒng)設計要求的建模工具，它用簡潔的圖形化語言描述系統(tǒng)中各部件的信息交互過程[7]，其強大的描述功能在很多領域得到廣泛的應用[8，9]。因此利用MSC建立等級轉(zhuǎn)換過程的MSC模型圖，可以有效地保證所建模型與相關技術(shù)規(guī)范的一致性，從而達到驗證系統(tǒng)技術(shù)規(guī)范的目的。

定義1：MSC是一個五元組MSC=(I，M，f，t，{≤i}i∈I)。其中，I是有限實體集；M是有限消息集；f和t是兩個函數(shù)集，f∈M→I表示消息接收，t∈M→I表示消息發(fā)送；?i∈I，≤i={？m|m∈M,,t(m)=i}∪{!m|m∈M,,f(m)=i}，即M中消息接收與消息發(fā)送的傳遞閉包。

定義2：假定一個五元組MSC=(I，M，f，t，{≤i}i∈I)可以用來描述C2級向C3級轉(zhuǎn)換時的信息交互，對其定義如下。

(1)I={IDriver，IRBC，ITrain，IBalise}，IDriver，IRBC，ITrain，IBalise分別表示司機，RBC系統(tǒng)，車載系統(tǒng)和應答器系統(tǒng)。

(2)M={MDriver，MRBC，MTrainMBalise}，MDriver，MRBC，MTrain，MBalise分別表示與仿真司機系統(tǒng)，RBC系統(tǒng)，車載系統(tǒng)和應答器系統(tǒng)相關的消息子集，其中MDriver={RequestConf，Confirm，DelayConfirm};MRBC={ConnectRBC，ConfirmCon，CancelCon，Parameter，Level，Config，Confirm，Route，MA，Location};MTrain={SetGSM_R，SetRBC，ConnectRBC，ConfirmCon，Cancel，CancelCon，Parameter，Level，Config，Confirm，Notice，Route，MA，Termination，RequestConf，ConfirmR，Execution，DelayConfirm，Location};MBalise={SetGSM_R，SetRBC，Cancel，Notice，Termination，Execution}。

(3)≤inst=∪i∈I。

(4)≤io={(!m，？m)|m∈M}。

f和t是表示將消息集M映射到實體集I的函數(shù)，如f(SetGSM_R)=IBalise，t(SetGSM_R)=ITrain，用!m和？m分別表示發(fā)送和接收消息m的事件。≤i表示在實體i的時間軸(縱軸)上發(fā)生的事件的局部順序，對于沒有絕對先后順序的消息，MSC允許用共區(qū)(coregion)來表示。如在C2級向C3級轉(zhuǎn)換過程中，車載設備接收來自司機確認轉(zhuǎn)換的消息，ConfirmR或DelayConfirm，!ConfirmR≤Driver! DelayConfirm表示Driver系統(tǒng)發(fā)送消息ConfirmR和DelayConfirm沒有絕對先后順序?！躨o表示消息的發(fā)送先于接收的因果關系，即?m，!m≤io？m;如!ConnectRBC≤io？ConfirmCon表示Train發(fā)送ConnectRBC消息先于接收到的ConfirmCon消息。

根據(jù)3.1節(jié)的定義2，對第二節(jié)所描述的C2級向C3級轉(zhuǎn)換過程進行建模。假設轉(zhuǎn)換執(zhí)行過程中產(chǎn)生的事件都按正常消息流程實現(xiàn)，利用MSC異步連接方式(在執(zhí)行后一個進程的任何事件之前，必須先完成它在前一個進程中的所有事件)構(gòu)件事件的因果關系，建立C2級向C3級轉(zhuǎn)換過程的MSC模型，完整的轉(zhuǎn)換過程如圖2所示，轉(zhuǎn)換包括建立連接，數(shù)據(jù)交換和執(zhí)行轉(zhuǎn)換3個過程。圖3和圖4表示在兩種更改計劃的情況下，列車取消轉(zhuǎn)換計劃的消息順序圖。

圖2　C2/C3等級轉(zhuǎn)換過程消息順序模型

3.2MSC模型描述

C2級向C3級轉(zhuǎn)換過程中信息交互的對象有：司機(Driver)、RBC、車載設備(Train)和應答器(Balise)。

(1)建立通信：進入轉(zhuǎn)換區(qū)之前，當GSM-R與其他網(wǎng)絡并存時，由應答器組GRE向列車發(fā)送SetGSM_R消息，以連接GSM_R網(wǎng)絡，列車連接成功后，接收設置在轉(zhuǎn)換區(qū)入口處的RBC連接應答器組RE的消息SetRBC，列車根據(jù)收到的SetRBC消息，向RBC發(fā)送連接RBC的請求消息ConnectRBC，RBC向車載發(fā)送確認消息ConfirmCon，呼叫RBC成功，建立通信過程完成。

此后列車若經(jīng)過RT應答器組，更改轉(zhuǎn)換計劃，此過程的MSC模型圖如圖3所示：列車接收到RT應答器組發(fā)來取消通信的消息Cancel，列車向RBC發(fā)送消息CancelCon斷開通信，列車繼續(xù)以C2系統(tǒng)運行。

圖3　列車經(jīng)過RT應答器組的消息順序

(2)數(shù)據(jù)交換：列車與RBC建立通信成功后，RBC向車載發(fā)送位置報告參數(shù)消息Parameter，列車向RBC發(fā)送當前等級及模式信息消息Level，RBC向列車發(fā)送配置參數(shù)消息Config，列車向RBC發(fā)送確認收到配置參數(shù)的消息Confirm，列車前端經(jīng)過等級轉(zhuǎn)換預告應答器組LTA時，接收到提醒列車即將進行轉(zhuǎn)換和準確的列車位置信息消息Notice，列車再將準確的進路信息消息Route發(fā)送給RBC，RBC根據(jù)以上消息計算行車許可MA，并將其發(fā)送給列車，數(shù)據(jù)交換過程完成。

此后列車若經(jīng)過LTT應答器組，終止轉(zhuǎn)換計劃，此過程的MSC模型圖如圖4所示：列車接收到LTT應答器組發(fā)來終止轉(zhuǎn)換的消息Termination，列車向RBC發(fā)送消息CancelCon斷開通信，列車繼續(xù)以C2系統(tǒng)運行。

圖4　列車經(jīng)過LTT應答器組的消息順序

(3)執(zhí)行轉(zhuǎn)換：列車與RBC數(shù)據(jù)交換完成后，列車運行接近C2級向C3級轉(zhuǎn)換邊界一定距離時(列車需走行5s時間)，車載設備將請求司機確認即將進行的等級轉(zhuǎn)換，發(fā)送消息RequestConf，司機進行確認，向車載設備發(fā)送消息ConfirmR，列車前端進入C3級區(qū)域并自動轉(zhuǎn)為C3級系統(tǒng)工作后5 s內(nèi)允許司機繼續(xù)進行確認，此時確認，司機向車載設備發(fā)送消息DelayConfirm。等級轉(zhuǎn)換邊界設置轉(zhuǎn)換執(zhí)行應答器組LTO，列車前端經(jīng)過該應答器組時，收到執(zhí)行轉(zhuǎn)換的消息Execution，本務端的車載設備執(zhí)行C2級向C3級的控車轉(zhuǎn)換。列車完成C2級向C3級的等級轉(zhuǎn)換。車載設備將其位置信息Location發(fā)送給RBC，執(zhí)行轉(zhuǎn)換過程完成。

4模型的仿真與驗證

4.1驗證工具UPPAAL簡介

時間自動機是為了專門研究實時系統(tǒng)而對自動機理論的擴展，在列控領域已有相關的研究案例[10，11]。UPPAAL是時間自動機模型的自動驗證工具，為實時系統(tǒng)的驗證提供建模、仿真和驗證環(huán)境，適用于可以被描述為非確定并行過程的積的系統(tǒng)。其用戶界面包括系統(tǒng)編輯器，模擬器和驗證器，分別用于系統(tǒng)模型的創(chuàng)建、檢查和驗證[12，13]。

4.2C2級向C3級轉(zhuǎn)換過程模型

等級轉(zhuǎn)換過程的MSC模型直觀描述了消息事件的進程，但無法對其模型進行有效的分析和驗證，在UPPAAL的編輯器中，將MSC模型轉(zhuǎn)換成時間自動機模型，然后對其進行形式化驗證。

圖5　C2向C3轉(zhuǎn)換過程中車載設備的模型

圖6　C2級向C3級轉(zhuǎn)換過程中RBC的模型

圖7　C2級向C3級轉(zhuǎn)換過程中應答器的模型

圖8　C2級向C3級轉(zhuǎn)換過程中司機的模型

MSC模型中有4個實體：ITrain，IRBC，IBalise，IDriver，按照時間自動機嚴格的語法和語義，結(jié)合文獻[3]，定義時間自動機的位置、事件、時鐘約束等，建立相應的時間自動機模型，依次記做TATrain、TARBC、TABalise、TADriver。C2級向C3級轉(zhuǎn)換過程是這四個時間自動機的積，即TA=TATrain||TARBC||TABalise||TADriver。所建立的C2級向C3級轉(zhuǎn)換的時間自動機網(wǎng)絡模型如圖5～圖8所示。所建立的時間自動機模型完全對照文獻[5]中對C2級向C3級轉(zhuǎn)換過程的描述，消息的命名與內(nèi)容與所建MSC模型相一致，確保時間自動機模型與C3級列控系統(tǒng)設計規(guī)范相符。以“!”結(jié)尾的消息表示發(fā)出此信號時轉(zhuǎn)換發(fā)生，以“？”結(jié)尾的消息表示接收到該信號時轉(zhuǎn)換發(fā)生，以此實現(xiàn)各模型中相同的轉(zhuǎn)換同步發(fā)生。T1～T6表示系統(tǒng)的時鐘約束，k，f，n，y，x，z，b，v，m1，m2為系統(tǒng)的標志位，用于限定消息的接收與發(fā)送。

4.3模型的仿真與驗證

UPPAAL模擬器中可以觀察各實體之間消息的交互情況，在驗證前發(fā)現(xiàn)系統(tǒng)運行的錯誤從而對模型進行修正，通過不斷的模擬和修正，完善系統(tǒng)模型。繼而在驗證器中，通過對BNF語句的檢驗，驗證系統(tǒng)的功能屬性。UPPAAL為模型的驗證提供了一種BNF語法[14]。Prop∷=A[]p|E<>p|E[]p|A<>p|p→q，其中E<>p表示屬性p可能滿足，E<>p為真，當且僅當在轉(zhuǎn)換系統(tǒng)中存在一個序列s0→s1→…→sn，使得s0是開始狀態(tài)，sn代表p。A[]p表示屬性p是不變的，等價于notE<>notp。E[]p表示屬性p是永遠可能的，E[]p為真，當且僅當在系統(tǒng)中存在一個序列s0→s1→…→si→…，使得p在所有狀態(tài)si中有效，并且這個序列無窮或者在狀態(tài)(ln，vn)終止，對所有的d:(ln，vn+d)滿足p和Inv(ln)或者從(ln，vn)出發(fā)沒有轉(zhuǎn)換。A<>p表示屬性p最終滿足。p→q表示屬性p滿足導致屬性q也滿足，等價于A[](p imply A<>q)。

根據(jù)CTCS-3級列控系統(tǒng)總體技術(shù)方案中對等級轉(zhuǎn)換過程的功能性和實時性的相關要求，列出系統(tǒng)需要滿足的要求和性質(zhì)，然后將每一條性質(zhì)用BNF語句表達出來，對BNF語句逐一進行驗證，語句后面的小圓圈在驗證通過時顯示綠色，如圖9所示，驗證不通過時顯示紅色，以此來表明此條性質(zhì)在所建模型中是否可達的。具體驗證內(nèi)容和驗證結(jié)果如下所述。

圖9　模型驗證結(jié)果示意

(1)對系統(tǒng)功能性要求的驗證

①系統(tǒng)模型不死鎖：A[] not deadlock，驗證通過；

②設備均正常的情況下，能實現(xiàn)C2級向C3級的轉(zhuǎn)換：E<>(Train.idleimply Train.gotoC3)，驗證通過；

③更改計劃后，系統(tǒng)能繼續(xù)以C2級運行：E<>((Train.C2) or(Train.c2))，驗證通過。

(2)對系統(tǒng)受限活性的驗證：

①連接RBC時間不大于10 s：A<>((Train.BuildConn imply Train.ConnYES) and (T2<=10))，驗證通過；

②車載設備和RBC交換數(shù)據(jù)的時間為15～20 s：A<>((Train.PreConvert implyT3>=15) and (Train.PreConvert implyT3<=20))，驗證通過；

③司機確認時間不大于10 s：A<>(Train.PreConvert imply Train.C3 and(T5<=10))，驗證通過；

④從開始與RBC連接到完全具備轉(zhuǎn)換C3級系統(tǒng)條件，列車至少需要走行40 s的時間：A[](Train.WaitConf implyT2>=40)，驗證通過；

⑤從轉(zhuǎn)換預告點到轉(zhuǎn)換執(zhí)行點，列車至少需要走行20 s的時間：A[](Train.gotoC3 implyT4>=20)，驗證通過；

⑥從建立GSM-R無線注冊到C3級轉(zhuǎn)換完成時間為80 s：A<>((Train.ConnGSM_R imply Train.Goto C3) and (T1<=80))，驗證通過。

對以上每條性質(zhì)逐一檢驗，得出的結(jié)果是每條性質(zhì)都是可達的，說明系統(tǒng)可以滿足這些性能和要求，繼而說明根據(jù)文獻[5]所建立的MSC模型和時間自動機模型經(jīng)過檢驗是安全可靠的。

5結(jié)語

本文采取MSC和時間自動機理論相結(jié)合的方法，對C3級列控系統(tǒng)中C2級向C3級轉(zhuǎn)換的場景進行形式化建模與驗證。MSC理論的優(yōu)點是易于理解和直觀表達，因此，建立等級轉(zhuǎn)換的MSC模型，將其轉(zhuǎn)化為擁有驗證工具UPPAAL的時間自動機模型，確保了模型與系統(tǒng)規(guī)范的一致性，并對系統(tǒng)的功能性和受限活性進行了模擬仿真，驗證了C3級列控系統(tǒng)對等級轉(zhuǎn)換的設計要求，為系統(tǒng)下一步的設計和開發(fā)提供了依據(jù)。結(jié)果表明此種建模方法可行，可將其應用于系統(tǒng)規(guī)范中其他場景的進行形式化建模與驗證。

參考文獻：

[1]佟立本.高速鐵路概論[M].4版.北京:中國鐵道出版社，2012：159-206.

[2]劉琦.高速鐵路開行160 km/h普速列車信號系統(tǒng)適應性研究與應用[J].鐵道標準設計，2013(10):129-132.

[3]王俊峰，汪希時.CTCS-3列車控制系統(tǒng)數(shù)據(jù)融合方法研究[J].鐵道學報，2012，34(9):70-74.

[4]王艷平.既有鐵路車站站改信號過渡特殊處理[J]. 鐵道標準設計，2013(4):123-126.

[5]張曙光.CTCS-3級列控系統(tǒng)總體技術(shù)方案[M].北京:中國鐵道出版社，2008：14-25.

[6]鐵道部運輸局.運基信號[2011]170號CTCS-2/CTCS-3級列控系統(tǒng)等級轉(zhuǎn)換應用原則[S].北京：鐵道部運輸局，2011.

[7]Alur R，Etessami k，Yannakakis M.Inference of Message Sequence Charts[J].IEEE Transaction on Software Engineering(S0098-5589)， 2003，29(7):623-633.

[8]Roychoudhury A.Embedded Systems and Software Validation[M]. Singapore：Elsevier Pte Ltd.Press，2009.

[9]石雙元，張浩.基于消息順序圖和Petri網(wǎng)的供應鏈工作流模型設計[J].管理學報，2007，4(6):756-766.

[10]呂繼東，唐濤，燕飛等.基于UPPAAL的城市軌道交通CBTC區(qū)域控制子系統(tǒng)建模與驗證[J].鐵道學報，2009，32(3):59-64.

[11]彭大天，步兵.基于UPPAAL的FAO系統(tǒng)典型運營場景建模與驗證[J].鐵道學報，2013，35(6):65-71.

[12]Sultan F，F(xiàn)arley J U， Lehman D R. A meta analysis of applications of diffusion models[J]. Journal of Marketing Research(S0022-2437)， 1990，37(12):70-77.

[13]Erdo P，Renyi A.On the evolution of random graphs[J]. Bulletin of the International Statistical Institute(S1539-3755)， 1961，38(4):343-347.

[14]孫全勇.時間自動機及其應用研究[D].哈爾濱:哈爾濱工程大學，2007.

Formal Verification of Level Transition Process in Train Control System Based On MSC and UPPAALHu Xue-lian, Tao Cai-xia

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

Abstract：Level transition is one of the most important scenarios in CTCS-3 control system and the very reflection of its compatibility. The successful transition is directly related to train operation safety and transportation efficiency. Therefore, in order to guarantee the security and real-time performance of the system, it is necessary to formally build and verify a model of transition process described in the design specification. To ensure the consistency between of the design specification, the message sequence configure (MSC) is combined with timed automata, the MSC model is established for C2 to C3 transition process in level transition scenario and is transformed to timed automata model. Then the security and restricted activity of the model are simulated and verified by applying UPPAAL validation tool. The results show that the transition process described in the design specification is safe and reliable to meet the requirements of compatibility and security in CTCS-3 system.

Key words：CTCS; Level transition; MSC; Timed automata; UPPAAL; Modeling

中圖分類號：U285.21

文獻標識碼：A

DOI:10.13238/j.issn.1004-2954.2015.02.030

文章編號：1004-2954(2015)02-0122-06

作者簡介：胡雪蓮(1988—)，女，碩士研究生，E-mail：tjhuxuelian@163.com。

收稿日期：2014-05-14； 修回日期：2014-06-11