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

周　翔，武曉春

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

?

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

周翔，武曉春

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

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

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

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

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

1　CTCS等級轉換區臨時限速場景分析

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

圖1　CTCS等級轉換區臨時限速場景

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

2　MSC模型描述

2.1基于MSC的系統建模

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

定義1：MSC是一個五元組∑=(I，M，f，t，{≤i}i∈I)。其中，I是有限實體集，M是有限消息集，f∈M→I、t∈M→I分別表示消息接收和消息發送，對?i∈I，≤i={？m∣m∈M，t(m)=i}∪{!m∣m∈M，f(m)=i}，即M中消息接收與消息發送的傳遞閉包。

定義2：假定一個五元組MSC=(I，M，f，t，{≤i}i∈I)可以用來描述等級轉換區跨界臨時限速命令交互模型，其定義如下。

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

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

(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映射到實數集I的函數，如f(SetTSR)=ICTC-A，t(SetTSR)=ITSRS-A。!m用來表示發送m事件，？m用來表示接收m事件，如：消息SetTSR從組件CTC-A發送至組件TSRS-A表示為;組件TSRS-A接收組件CTC-A發送的SetTSR消息表示為。≤i表示在時間軸上實體i發生變化的局部順序，如：ActTSR和ActSucc，!ActTSR≤TSRS-A!ActTSR表示TSRS-A向TCC-B發送ActTSR消息，？ActSucc≤TSRS-A？ActSucc表示TSRS-A接收TCC-B的ActSucc消息。≤io表示消息的發送先于接收的順序關系，即?m，!m≤io？m;如!ActTSR≤io？ActSucc表示TSRS-A發送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段。若左側調度臺CTC-A下發SetTSR消息至TSRS-A，由TSRS-A對下發命令進行校驗，此時TSRS-A向CTC-A反饋校驗結果需要在4個通信周期完成(一個通信周期為2s)，若CTC-A在2s內沒有收到反饋校驗結果則判斷為一次等待超時，若CTC-A向TSRS-A重發消息且連續4次等待超時則判斷CTC-A與TSRS-A之間通信中斷。當校驗成功時回執SaveTSR消息至CTC-A，其校驗MSC模型流程如圖2所示。CTC-A根據反饋回的SaveTSR，向激活后的TSRS-A發送ActTSR消息。TSRS-A根據命令參數信息將臨時限速命令下發至TCC-A，同時發送至右側區域TCC-B進行驗證、執行。此時TSRS-A要求TCC-A，TCC-B要在3個通信周期(一個通信周期為1s)內反饋接受信息，如果沒有接收到反饋信息則判斷一次等待超時，如果連續3次判斷為等待超時則TSRS-A判斷為通信中斷。同時要求TCC-A、TCC-B將驗證、執行的有效的目標參數結果反饋給TSRS-A。TSRS-A對目標驗證結果進行綜合判定，若驗證成功向CTC-A發送ActSucc消息，若驗證失敗向CTC-A返回ActFail消息。當驗證目標信息成功時，CTC-A向TSRS-A發送ExeTSR消息，由TCC-A和TCC-B執行臨時限速命令，并將執行成功的ExeSucc消息反饋給TSRS-A。

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

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

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

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

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

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

3　系統建模仿真

3.1時間自動機與UPPAAL

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

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

表1　BNF語法及其含義

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

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

設CTCS等級轉換區跨界臨時限速的時間自動機模型為

TA=

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

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

表2　模型中的主要位置

圖4　CTCS等級轉換區跨界臨時限速的時間自動機模型

4　系統模型的驗證

圖5　跨界臨時限速工作狀態流程時序

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

圖6　性質驗證

4.1系統安全性要求

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

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

(3)TCC-B應向TSRS-A反饋分發校驗結果，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反饋執行驗證結果，E<>((TCC_b.S_verif)imply(TCC_b.S_sendVerifRes);TSRS-A對執行結果進行驗證，E<>(TSRS_a.S_waitVerif)imply(TSRS_a.S_verifRes).驗證通過。

(5)TCC-B既沒有發送執行反饋信息，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)).驗證不通過，因為無反饋信息無報警這種情況是不允許發生的。

4.2系統受限活性要求

(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內向CTC-A行調臺反饋校驗結果。若校驗成功，臨時限速操作終端需每隔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)).驗證通過。

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

5　結語

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[14]呂繼東，唐濤，燕飛，等.基于UPPAAL的城市軌道交通CBTC區域控制子系統建模與驗證[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

國家自然科學基金地區項目(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