基于MSC與UPPAAL的高鐵跨界臨時限速建模與驗證

周　翔，武曉春

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

?

基于MSC與UPPAAL的高鐵跨界臨時限速建模與驗證

周翔，武曉春

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

臨時限速服務器是高鐵列控系統(tǒng)的重要組成部分，其不僅要校驗CTC下發(fā)的臨時限速命令，還要與相鄰調(diào)度臺臨時限速服務器之間進行頻繁的信息交互，因此對其安全性和實時性要求也更苛刻。為了滿足高鐵列控系統(tǒng)對其運行的要求，采用時間自動機理論和消息順序圖(MSC)相結合的方法，首先建立跨界臨時限速命令的MSC模型和時間自動機子模型，再利用UPPAAL驗證工具對形式化語法BNF描述的時間自動機子模型屬性進行驗證。根據(jù)仿真驗證結果確認了跨界臨時限速信息的安全性和受限活性，為進一步開發(fā)臨時限速服務器功能提供了重要的依據(jù)。

臨時限速服務器；時間自動機；UPPAAL；實時性；MSC

隨著我國高速鐵路的快速發(fā)展，高鐵列控系統(tǒng)對臨時限速服務器的安全性和實時性的要求也越來越高。臨時限速服務器是高鐵列控系統(tǒng)的重要組成部分，其工作流程具有嚴格的時間約束特性和安全特性，是典型的實時系統(tǒng)[1-2]。因此，根據(jù)高速列車的實際運行情況，臨時限速區(qū)段可能設置在CTCS(Chinese Train Control System)等級轉(zhuǎn)換區(qū)，此時，等級轉(zhuǎn)化區(qū)一側(cè)為客運專線CTCS-2/CTCS-3級控制區(qū)域，另一側(cè)為既有提速線控制區(qū)域[3-4]。由于其設備之間信息交互的復雜性，利用半形式化(以數(shù)學為基礎來定義硬件系統(tǒng)和軟件系統(tǒng)的規(guī)約但不對其進行驗證)和形式化方法對跨界臨時限速區(qū)域臨時限速命令的擬定下達校驗進行建模和驗證，有效地發(fā)現(xiàn)系統(tǒng)硬件設計和時間約束缺陷，提高其系統(tǒng)的安全性和受限活性。

半形式化方法以MSC(Message Seque-nce Chart)消息順序圖為基礎，描述臨時限速命令的交互過程；形式化方法以離散型數(shù)學為基礎，運用嚴格的形式化語義對系統(tǒng)特性進行精確描述，其中時間自動機是形式化方法中一種，不僅可用來描述實數(shù)值時鐘約束系統(tǒng)，還可以描述有限控制變量的狀態(tài)轉(zhuǎn)換系統(tǒng)[5]。因此，利用MSC對CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速與各相關設備信息交互流程建立模型將其轉(zhuǎn)化為時間自動機模型，并利用UPPAAl驗證跨界臨時限速的安全性和受限活性。

1　CTCS等級轉(zhuǎn)換區(qū)臨時限速場景分析

在高鐵列控系統(tǒng)中，臨時限速服務器不僅對臨時限速命令進行校驗和存儲，而且還要跟其他相關信號設備進行交互。如：CTC(Centralized Traffic Control，調(diào)度中心)負責擬定、執(zhí)行、取消等命令的下達，TSRS(Temporary Speed Restriction Server，臨時限速服務器)完成校驗、分發(fā)和綜合，并將結果反饋給CTC，TCC(Train Control Center，列控中心)、RBC(Radio Block Center，無線閉塞中心)分別通過應答器、GSM-R(Global System for Mobile Communication-Railway)將TSRS下發(fā)的TSR(Temporary Speed Restriction，臨時限速命令)發(fā)送到車載設備執(zhí)行[6-7]。臨時限速在CTCS等級轉(zhuǎn)換區(qū)的場景如圖1所示。

圖1　CTCS等級轉(zhuǎn)換區(qū)臨時限速場景

臨時限速命令的擬定遵循“以線路正方向為限速起點”的歸屬原則，限速-2在兩側(cè)TSRS數(shù)據(jù)覆蓋范圍之內(nèi)。因此，TSRS-A與TCC-B要實現(xiàn)TSR切換控制權同步，這樣臨時限速命令正式生成。本論文主要是針對CTCS等級轉(zhuǎn)換區(qū)的跨界臨時限速命令的擬定下達、取消和刪除過程進行建模[8]，從而驗證跨界臨時限速命令切換的安全性和時效性。

2　MSC模型描述

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

消息順序圖(MSC)是一種直觀可視的半形式化圖形描述語言，用來描述不同組件之間交互機制。MSC的描述功能能夠滿足許多復雜領域的應用，因此，利用MSC來描述等級轉(zhuǎn)換區(qū)跨界臨時限速TSR切換的過程，建立技術規(guī)范中模型的信息交互和狀態(tài)轉(zhuǎn)移(靜態(tài))過程，為后面的模型搭建提供清楚的圖形描述，從而達到驗證的目的。

定義1：MSC是一個五元組∑=(I，M，f，t，{≤i}i∈I)。其中，I是有限實體集，M是有限消息集，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)可以用來描述等級轉(zhuǎn)換區(qū)跨界臨時限速命令交互模型，其定義如下。

(1)I={ICTC-A，ITSRS-A，ITCC-B，ICTC-B}，分別表示仿真客專側(cè)CTC系統(tǒng)，客專側(cè)TSRS系統(tǒng)，既有線側(cè)TCC系統(tǒng)，既有線側(cè)CTC系統(tǒng)。

(2)M={MCTC-A，MTSRS-A，MTCC-B，MCTC-B}，分別表示仿真客專側(cè)CTC系統(tǒng)，客專側(cè)TSRS系統(tǒng)，既有線側(cè)TCC系統(tǒng)，既有線側(cè)CTC系統(tǒng)的相關消息子集。

(3)≤inst=Ui∈I。

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

(5)≤MSC=(≤inst∪≤io)+。

其中：MCTC-A={SetTSR，ActivateTSR，DisToTCC，ActTSR}，MTSRS-A={SaveTSR，ActFail，CancTSR，NoticeCase，ActTSR，JudCommand，ExeTSR，DisToTCC-B，Protocal(TSRSToCTC)}，MTCC-B={ActSucc，NoticeCase，ExeTSR，ExeSucc}，MCTC-B={NoticeCase，SetTSR，Protocal(CTCToTSRS)}，f和t表示將消息集M映射到實數(shù)集I的函數(shù)，如f(SetTSR)=ICTC-A，t(SetTSR)=ITSRS-A。!m用來表示發(fā)送m事件，？m用來表示接收m事件，如：消息SetTSR從組件CTC-A發(fā)送至組件TSRS-A表示為;組件TSRS-A接收組件CTC-A發(fā)送的SetTSR消息表示為。≤i表示在時間軸上實體i發(fā)生變化的局部順序，如：ActTSR和ActSucc，!ActTSR≤TSRS-A!ActTSR表示TSRS-A向TCC-B發(fā)送ActTSR消息，？ActSucc≤TSRS-A？ActSucc表示TSRS-A接收TCC-B的ActSucc消息?！躨o表示消息的發(fā)送先于接收的順序關系，即?m，!m≤io？m;如!ActTSR≤io？ActSucc表示TSRS-A發(fā)送ActTSR消息先于接收到的ActSucc消息；≤MSC表示≤inst和≤io的傳遞包關系，如!SetTSR≤MSC？ActTSR，!SetTSR≤MSC？ActTSR，!ActTSR≤MSC？ActSucc[9-10]。

2.2跨界臨時限速命令的擬定和下達

如圖1中限速-2由CTC-A負責擬定a-c段，CTC/TDCS-B負責擬定c-b段。若左側(cè)調(diào)度臺CTC-A下發(fā)SetTSR消息至TSRS-A，由TSRS-A對下發(fā)命令進行校驗，此時TSRS-A向CTC-A反饋校驗結果需要在4個通信周期完成(一個通信周期為2s)，若CTC-A在2s內(nèi)沒有收到反饋校驗結果則判斷為一次等待超時，若CTC-A向TSRS-A重發(fā)消息且連續(xù)4次等待超時則判斷CTC-A與TSRS-A之間通信中斷。當校驗成功時回執(zhí)SaveTSR消息至CTC-A，其校驗MSC模型流程如圖2所示。CTC-A根據(jù)反饋回的SaveTSR，向激活后的TSRS-A發(fā)送ActTSR消息。TSRS-A根據(jù)命令參數(shù)信息將臨時限速命令下發(fā)至TCC-A，同時發(fā)送至右側(cè)區(qū)域TCC-B進行驗證、執(zhí)行。此時TSRS-A要求TCC-A，TCC-B要在3個通信周期(一個通信周期為1s)內(nèi)反饋接受信息，如果沒有接收到反饋信息則判斷一次等待超時，如果連續(xù)3次判斷為等待超時則TSRS-A判斷為通信中斷。同時要求TCC-A、TCC-B將驗證、執(zhí)行的有效的目標參數(shù)結果反饋給TSRS-A。TSRS-A對目標驗證結果進行綜合判定，若驗證成功向CTC-A發(fā)送ActSucc消息，若驗證失敗向CTC-A返回ActFail消息。當驗證目標信息成功時，CTC-A向TSRS-A發(fā)送ExeTSR消息，由TCC-A和TCC-B執(zhí)行臨時限速命令，并將執(zhí)行成功的ExeSucc消息反饋給TSRS-A。

圖2　客專側(cè)臨時限速命令的校驗MSC模型

若由右側(cè)的CTC/TDCS-B下發(fā)的SetTSR消息發(fā)送至TCC-B，左側(cè)TSRS-A通過CTC協(xié)議轉(zhuǎn)換Protocal(CTCToTSRS)接收TCC-B下發(fā)的SetTSR消息由其進行可執(zhí)行性校驗(校驗流程圖如圖3所示)，此時既有線側(cè)同客專側(cè)通信周期相同。

圖3　既有線側(cè)臨時限速命令的校驗MSC模型

若校驗成功，發(fā)送ActSucc消息至本側(cè)的TCC-A，并由TCC-B發(fā)送ExeTSR消息至CTC-A執(zhí)行臨時限速命令；若校驗失敗，TSRS-A將ActFail消息發(fā)送至右側(cè)調(diào)度臺CTC/TDCS-B，并將CancTSR消息發(fā)送至TCC-B。反饋兩側(cè)執(zhí)行信息由TSRS-A綜合校驗，其結果發(fā)送至左側(cè)調(diào)度臺CTC-A顯示。

2.3跨界臨時限速命令的取消與刪除

客運專線調(diào)度臺CTC-A由原擬定方取消臨時限速命令擬定的限速命令；而既有提速線調(diào)度臺CTC/TDCS-B需要通過電話、傳真通知客運專線調(diào)度臺確認，只有得到確認后，才能由CTC/TDCS-B下達取消命令[11]。

3　系統(tǒng)建模仿真

3.1時間自動機與UPPAAL

時間自動機理論由R.Alur和Dill于1994年提出，時間自動機是一種基于時間周期、時間約束和時間解釋的形式化建模方法。UPPAAL驗證工具由Aalborg大學和Uppsala大學于1995年共同開發(fā)，其通過模擬控制有限個控制結構和數(shù)值時鐘并采用整型變量來驗證系統(tǒng)的安全性和受限活性[12-13]。

UPPAAL用戶界面包括三個部分：系統(tǒng)編輯器(system editor)、模擬器(simulator)和驗證器(verifier)。其中system editor用于創(chuàng)建和編輯要分析的系統(tǒng)；simulator用來檢查所建系統(tǒng)模型是否正確；verifier通過快速搜索系統(tǒng)模型的狀態(tài)空間來檢查時鐘約束條件和限制性質(zhì)。UPPAAL驗證工具應用的BNF語法[14-15]。Prop::=E<>p∣E[]p∣A<>p∣A[]p∣p→q，這種語法含義如表1所示。

表1　BNF語法及其含義

3.2基于時間自動機的跨界臨時限速的模型

2.1節(jié)和2.2節(jié)已利用消息順序圖(MSC)對跨界臨時限速命令在設備之間的交互流程已做了詳細的闡述，且根據(jù)MSC描述的流程用UPPAAL建模仿真工具分別對CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速信息交互的4個活動對象進行建模，即CTC-A、TSRS-A、TCC-B、CTC-B。構造出每個時間自動機模型，分別為TACTC-A、TATSRS-A、TATCC-B、TACTC-B，如圖4所示。

設CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速的時間自動機模型為

TA=

S、S0、A、X、I、E分別表示時間自動機建模的過程狀態(tài)、初始狀態(tài)、觸發(fā)事件、時間參數(shù)、整數(shù)變量、狀態(tài)轉(zhuǎn)移路徑。其中，過程狀態(tài)S={idle，P_preTSR，S_exeFail，S_exeTSR，…};初始狀態(tài)S0=idle;觸發(fā)事件A={cancelTSR，TSRFail，warning，planTSR，…};時間參數(shù)X={T0，T1，T2，t，T_TCCreaction，T_TSRStimeout}，其中T0表示臨時限速命令激活提示時間，T1、T2用來表示TSRS與TCC和CTC之間的通信時間，T_TCCreaction表示TCC接收和反饋TSRS發(fā)送信息的等待時間，T_TSRStimeout表示接收反饋信息超時;整數(shù)變量I={confirmFlag，verifFlag，checkFlag，exeFlag};狀態(tài)轉(zhuǎn)移路徑E={idle，comfirmFlag，P_preTSR，confirmFlag，idle，…}。其中“P_”，“E_”，“S_”開頭分別表示限速命令的擬定、下達、設置的過程。

如圖4所示，跨界臨時限速時間自動機網(wǎng)絡模型。其中，“!”表示發(fā)出信息交互，“？”表示接受信息交互。標有C的圓圈為堅定位置，表示在沒有時間延遲的情況下立即轉(zhuǎn)換離開約束位置，在該位置進行操作具有原子性，使用它則可以明顯減少系統(tǒng)狀態(tài)空間，并且可以對多個同步通信進行編碼。圖中模型中的主要位置如表2所示。

表2　模型中的主要位置

圖4　CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速的時間自動機模型

4　系統(tǒng)模型的驗證

圖5　跨界臨時限速工作狀態(tài)流程時序

在UPPAAL模擬器中建立好CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速的時間自動機網(wǎng)絡模型，其工作流程時序如圖5所示；同時在模擬器中對跨界臨時限速命令的擬定下達、取消與刪除等信息的交互進行模擬校驗；最后在UPPAAL驗證器中，應用BNF語法對跨界臨時限速的時間自動機模型進行驗證從而滿足其安全性和受限活性的要求，如圖6所示。

圖6　性質(zhì)驗證

4.1系統(tǒng)安全性要求

(1)TSRS-A分發(fā)跨界臨時限速命令進行校驗，E<>(TSRS_a.idle)imply(TSRS_a.E_waitCheck);同時請求鄰站TCC-B校驗，E<>(TCC_b.idle)imply(TCC_b.S_check).驗證通過。

(2)TSRS-A對執(zhí)行跨界臨時限速命令進行驗證，E<>(TSRS_a.idle)imply(TSRS_a.S_verif);同時請求鄰站TCC-B進行執(zhí)行校驗，E<>(TCC_b.S_checkSucc)imply(TCC_b.S_verif).驗證通過。

(3)TCC-B應向TSRS-A反饋分發(fā)校驗結果，E<>(TCC_b.S_check)imply(TCC_b.S_sendCheckRes);TSRS-A對結果進行校驗，E<>(TSRS_a.E_waitCheck)imply(TSRS_a.S_checkRes)).驗證通過。

(4)TCC-B應向TSRS-A反饋執(zhí)行驗證結果，E<>((TCC_b.S_verif)imply(TCC_b.S_sendVerifRes);TSRS-A對執(zhí)行結果進行驗證，E<>(TSRS_a.S_waitVerif)imply(TSRS_a.S_verifRes).驗證通過。

(5)TCC-B既沒有發(fā)送執(zhí)行反饋信息，TSRS-A也沒有向CTC-B報警。

E[]((not((TCC_b.S_exeTSR)imply(TCC_b.S_exeFinish)))and(not((CTC_b.S_exeTSR)imply(CTC_b.idle)))and(T2>T_TSRStimeout)).驗證不通過，因為無反饋信息無報警這種情況是不允許發(fā)生的。

4.2系統(tǒng)受限活性要求

(1)TCC-B收到臨時限速命令后，其驗證結果要求在1s反饋回TSRS-A，由TSRS-A對TCC-B反饋的驗證結果進行判定。

A<>(TCC_b.S_exeTSR)imply(TCC_b.S_exeFinish)and(T1<=1).驗證通過。

(2)TSRS-A對限速信息進行有效性校驗，并在2 s內(nèi)向CTC-A行調(diào)臺反饋校驗結果。若校驗成功，臨時限速操作終端需每隔10 min向CTC-A提示臨時限速命令的激活。

A<>((TSRS_a.P_checkValidity)imply(TSRS_a.P_checkSucc)or(TSRS_a.P_checkValidity)imply(TSRS_a.P_checkFail)and(T2<2)and(CTC_a.S_judgeCheckRes)imply(CTC_a.S_waitConfirm)and(T0=600).驗證通過。

(3)TSRS-A在超出T_TSRStimeout時間未收到反饋信息，則報警。

A<>((TSRS_a.S_waitRes)imply(TSRS_a.idle)and(T2>T_TSRStimeout)).驗證通過。

以上每條性質(zhì)都逐一進行了驗證，通過分析說明該系統(tǒng)滿足實際中對CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速安全性和受限活性的要求。

5　結語

本文采用消息順序圖(MSC)和時間自動機這種形式化的方法對跨界臨時限速進行建模，應用MSC建立起整個跨界臨時限速信息交互系統(tǒng)的模型，詳細闡述模型中信息交互和狀態(tài)轉(zhuǎn)移過程，并根據(jù)MSC描述的此過程同時建立時間自動機網(wǎng)絡模型，且應用UPPAAL進行模型驗證。成功地驗證了CTCS等級轉(zhuǎn)換區(qū)跨界臨時限速的安全性和受限活性，保證了系統(tǒng)的平穩(wěn)運行，并為系統(tǒng)進一步開發(fā)提供重要的依據(jù)。

[1]吳永剛，陸慧娟.基于時間自動機的實時系統(tǒng)建模及驗證[J].計算機時代，2011，6(1):2-3.

[2]郭震.CTCS各級系統(tǒng)中臨時限速技術運用的探討[J].科技信息，2011(16):111-112.

[3]姜明華.列控系統(tǒng)級間轉(zhuǎn)換點臨時限速區(qū)段設置探討[J].鐵道通信信號，2013(4):32-33.

[4]劉傳會，張廣全.一種基于時間自動機網(wǎng)絡的實時系統(tǒng)形式化驗證方法[J].蘇州大學學報，2008，24(1):35-40.

[5]中華人民共和國鐵道部.科技運[2010]137號.客運專線列控系統(tǒng)臨時限速技術規(guī)范(V2.0)[S].北京：中華人民共和國鐵道部，2010.

[6]甄力劍.客運專線臨時限速技術研究與應用[D].成都:電子科技大學，2012.

[7]袁磊，王俊峰.CTCS-3級列控系統(tǒng)臨時限速建模與驗證[J].西南交通大學學報，2013，48(4):701-712.

[8]康仁偉.基于時間自動機的CTCS-3級列控系統(tǒng)建模方法與驗證研究[D].北京:北京交通大學，2013：40-53.

[9]萬勇兵，徐中偉，梅萌.CTCS-3級列控系統(tǒng)臨時限速服務器建模與形式化驗證[J].系統(tǒng)仿真學報，2013，25(1):132-138.

[10]胡雪蓮，陶彩霞.基于MSC與UPPAAL的列控系統(tǒng)等級轉(zhuǎn)換場景形式化驗證[J].鐵道標準設計，2015(2):122-127.

[11]趙榮亮，王長林.高速鐵路CTC分界口臨時限速系統(tǒng)建模與驗證[J].鐵路計算機應用，2014，23(7):43-47.

[12]Larsen K G，Mikucionis M，Nielsen B.Online Testing of Real-time System Using UPPAAL，F(xiàn)ormal Approaches to Software Testing-4th International Workshop[J].Lecture Notes in Computer Science:(S0302-9743)，2005,3395:79-94.

[13]曹源.高速鐵路列車運行控制系統(tǒng)的形式化建模與驗證方法研究[D].北京:北京交通大學，2011.

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

[15]Hessel A，Larsen K G，Mikucionis M.Testing real-time systems using UPPAAL[J].Lecture Notes in Computer Science, 2008,4949:77-117.

Modeling and Verification of Cross-border Temporary Speed Restriction for High Speed Railway Based on MSC and UPPAAL

ZHOU Xiang，WU Xiao-chun

(College of Automation &Electrical Engineering，Lanzhou Jiaotong University，Lanzhou 730070，China)

Temporary Speed Restriction Server (TSRS) is an important part of the High Speed Railway Train Control System，it not only checks the temporary speed restriction orders issued by CTC，but also exchanges information frequently with the temporary speed restriction server of the adjacent dispatching station，and the requirements for its security and real-time performance are rigorous.In order to meet the requirement of the high speed railway train control system，a combination of timed automata theory with Message Sequence Chart (MSC) is employed to establish firstly the MSC model of Cross-border Temporary Speed Restriction and timed automata submodel，and then the verification tool of UPPAAL is used to verify the properties of the Cross-border Temporary Speed Restriction System described by BNF syntax.According to the simulation verification results，the security and restricted activity of the Cross-border Temporary Speed Restriction Information are confirmed，which provides an important basis for further development of the Temporary Speed Restriction Server.

Temporary Speed Restriction Server; Timed automata; UPPAAL; Real-time; MSC

2016-03-15；

2016-04-13

國家自然科學基金地區(qū)項目(61164010)

周翔(1989—)，男，碩士研究生，E-mail：826791444@qq.com。

1004-2954(2016)10-0126-06

U284.48+2

A

10.13238/j.issn.1004-2954.2016.10.028