周　翔，武曉春

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

?

基于MSC與UPPAAL的高鐵跨界臨時(shí)限速建模與驗(yàn)證

周翔，武曉春

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

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

臨時(shí)限速服務(wù)器；時(shí)間自動機(jī)；UPPAAL；實(shí)時(shí)性；MSC

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

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

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

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

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

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

2　MSC模型描述

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

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

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

(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)的相關(guān)消息子集。

(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í)數(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消息表示為?！躨表示在時(shí)間軸上實(shí)體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ā)送先于接收的順序關(guān)系，即?m，!m≤io？m;如!ActTSR≤io？ActSucc表示TSRS-A發(fā)送ActTSR消息先于接收到的ActSucc消息；≤MSC表示≤inst和≤io的傳遞包關(guān)系，如!SetTSR≤MSC？ActTSR，!SetTSR≤MSC？ActTSR，!ActTSR≤MSC？ActSucc[9-10]。

2.2跨界臨時(shí)限速命令的擬定和下達(dá)

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

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

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

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

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

2.3跨界臨時(shí)限速命令的取消與刪除

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

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

3.1時(shí)間自動機(jī)與UPPAAL

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

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

表1　BNF語法及其含義

3.2基于時(shí)間自動機(jī)的跨界臨時(shí)限速的模型

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

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

TA=

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

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

表2　模型中的主要位置

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

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

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

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

圖6　性質(zhì)驗(yàn)證

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

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

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

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

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

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

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)).驗(yàn)證不通過，因?yàn)闊o反饋信息無報(bào)警這種情況是不允許發(fā)生的。

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

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

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

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

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).驗(yàn)證通過。

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

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

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

5　結(jié)語

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

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

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

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

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

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

[6]甄力劍.客運(yùn)專線臨時(shí)限速技術(shù)研究與應(yīng)用[D].成都:電子科技大學(xué)，2012.

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

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

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

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

[11]趙榮亮，王長林.高速鐵路CTC分界口臨時(shí)限速系統(tǒng)建模與驗(yàn)證[J].鐵路計(jì)算機(jī)應(yīng)用，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]曹源.高速鐵路列車運(yùn)行控制系統(tǒng)的形式化建模與驗(yàn)證方法研究[D].北京:北京交通大學(xué)，2011.

[14]呂繼東，唐濤，燕飛，等.基于UPPAAL的城市軌道交通CBTC區(qū)域控制子系統(tǒng)建模與驗(yàn)證[J].鐵道學(xué)報(bào)，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

國家自然科學(xué)基金地區(qū)項(xiàng)目(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