CTCS—3級列控系統臨時限速建模與驗證

摘要： 為了滿足臨時限速系統的實時性要求，采用時間自動機理論，對CTCS3級列控系統臨時限速工作流程分別建立了各設備的時間自動機子模型，進而構成臨時限速系統的時間自動機網絡模型，并基于臨時限速系統技術規范的參數對模型進行賦值；采用BNF語法對臨時限速系統待驗證的屬性進行了形式化描述，并應用UPPAAL驗證工具對臨時限速模型的安全性和受限活性進行仿真驗證.驗證結果表明：與現有臨時限速系統的時間參數設置相比，修正后的時間參數設置避免了出現系統死鎖現象；在不影響安全功能屬性和受限活性的基礎上，提高了臨時限速系統的實時性，可在規范規定時間5 s內做出響應.

關鍵詞： CTCS3級列控系統；臨時限速；時間自動機；UPPAAL；實時性

中圖分類號： U283.4文獻標志碼： AModeling and Verification of Temporary Speed Restriction

of CTCS3 Train Control SystemYUAN Lei1，WANG Junfeng1，KANG Renwei1，L Jidong2

（1. State Key Laboratory of Rail Traffic Control and Safety， Beijing Jiaotong University， Beijing 100044， China； 2. National Engineering Research Center of Rail Transportation Operation and Control System， Beijing Jiaotong University， Beijing 100044， China）

Abstract：In order to meet the realtime performance requirement of a temporary speed restriction （TSR） system of Chinese train control system level 3 （CTCS3）， timed automata submodels of each equipment of the train control system were established for the working process of TSR， and a timed automata network model was built through parallel composition of the submodels to valuate the submodels using the parametric configuration of the specification of CTCS3. Then， the properties of the TSR system such as safety and bounded liveness were expressed in BackusNaur form （BNF） and validated through formal verification simulation using the UPPAAL integrated tool. The results show that compared with the parameters defined in the system specifications， the modified time parameters can fix the deadlock problem of the system， and improve the realtime performance of the TSR system on the premise of keeping the system properties such as safety and bounded liveness. The TSR system can respond to inputs within 5 s and meet the system specifications.

Key words：CTCS3 train control system； TSR； timed automata； UPPAAL； realtime performance

臨時限速是指線路規定限速以外具有時效性的限速，包括施工、維修引起的計劃性限速，以及自然災害、設備故障引起的突發性限速等[1].臨時限速是突發的和偶然的，僅在一定的時間范圍內有效[2].因此，臨時限速系統是典型的實時系統，臨時限速命令的擬定、設置、傳輸、接收、執行、確認、取消等，具有嚴格的邏輯順序關系和精確的時間約束特性.臨時限速工作流程依據技術規范而實現，如果技術規范存在缺陷，則會危及行車安全或影響行車效率.對臨時限速工作流程的實時性進行分析研究，以驗證技術規范的正確性具有重要意義.目前，對臨時限速的研究主要集中在介紹臨時限速的應用現狀[1]、分析臨時限速對列車運行的影響[2]等方面.

臨時限速系統具有嚴格的連續時間約束特性.要實現臨時限速功能，涉及多個設備，表現出復雜的交互特性.形式化方法以數學為基礎，是一種定義了硬件系統和軟件系統的規約并對系統進行驗證的語言、技術和工具[3]，可以最大限度地驗證系統的正確性[45].對系統實時性進行建模與驗證的形式化方法主要有：時間自動機（timed automata， TA）[68]、TPN（timed Petri net）[911]、HCSP（hybrid communicating sequential process）[4，12]、DC（duration calculus）[5，13]、Timed RAISE（timed rigorous approach to industrial software engineering）[1014].TPN的模型結構不清晰，不能直觀地描述臨時限速系統的交互特性，且目前的一種研究趨勢是將TPN轉換成TA模型[11]. HCSP可以描述臨時限速系統離散事件的交互行為，但模型的驗證非常困難，還沒有一套完整的HCSP驗證框架[4]. DC不能描述臨時限速的系統結構[4]， Timed RAISE在定理證明過程中，需要更多的人機交互，自動化程度較低，非專業人員使用時有一定困難[4，10，14].時間自動機是為了專門研究實時系統而對自動機理論的擴展，在列控領域已有相關的研究案例[4，6，12].它不僅可以描述臨時限速系統的連續時間特性，還可以描述臨時限速系統的信息交互西南交通大學學報第48卷第4期袁磊等：CTCS3級列控系統臨時限速建模與驗證特性.基于時間自動機的自動驗證工具UPPAAL[8，1518]為驗證提供了便利.綜上，選擇時間自動機理論驗證臨時限速系統的實時性更為合適.

時間自動機通常被定義為一個六元組[18]，為描述時間特性而擴展出關于時鐘約束和時鐘解釋的定義[78]. UPPAAL是基于時間自動機的驗證工具，它為驗證提供了一種BNF語法[18].本文采用時間自動機理論，應用UPPAAL驗證工具對CTCS3級列控系統臨時限速工作流程進行仿真建模，并對臨時限速系統的安全性和受限活性進行驗證，分析驗證技術規范[19]的正確性.1臨時限速系統的結構和功能CTCS3級列控系統臨時限速的設備構成及臨時限速命令傳輸通道如圖1所示[19].

圖1臨時限速命令傳輸示意圖

Fig.1Transmission diagram of temporary speed restriction command

臨時限速服務器分別向列控中心（train control center， TCC）及無線閉塞中心（radio block center， RBC）傳遞臨時限速信息.TCC和RBC分別通過點式的有源應答器和連續式的GSMR（GSM for railway）無線信道將臨時限速命令傳輸至車載設備.在CTCS3級列控系統中，臨時限速的擬定、設置和取消由調度中心（centralized traffic control， CTC）、臨時限速服務器（temporary speed restriction server， TSRS）、RBC和TCC共同完成.CTC負責臨時限速命令的擬定、設置、取消、存儲顯示等功能；TSRS具備全線臨時限速命令的存儲、校驗、撤銷、拆分等功能；RBC、TCC主要實現臨時限速命令的有效性檢查、生成臨時限速信息包、反饋臨時限速命令的執行結果等功能[19].

2臨時限速系統建模2.1安全功能屬性和受限活性要求針對臨時限速工作流程建立時間自動機網絡模型，以驗證工作流程的正確性，從而保證臨時限速系統的安全性和受限活性.臨時限速工作流程分為3部分[19]：擬定臨時限速、設置臨時限速、取消臨時限速.具體流程見文獻[19].系統的安全性用于描述系統不一定發生的事情，指“壞事情永遠都不會發生”[8].系統的受限活性用于說明系統必定發生某些事情，指“好事情終究會發生”[8].作為臨時限速系統建模的驗證目標，提出如下臨時限速系統的安全功能屬性和受限活性要求.

（1） 安全功能屬性要求.屬性a： RBC（TCC）沒有發送執行反饋信息， TSRS也沒有向CTC報警，該現象永遠不會發生.屬性b： CTC能擬定、設置、取消臨時限速命令.屬性c： 各設備正確完成對接收到的臨時限速信息的有效性校驗.屬性d： TSRS先驗證后執行臨時限速命令.屬性e： TSRS向RBC、TCC正確傳輸設置、取消等操作指令.屬性f： RBC、TCC向TSRS正確反饋臨時限速命令的執行結果.

（2） 受限活性要求.RBC收到臨時限速指令后，能在TRBCreaction時間內返回執行結果.若TSRS在TTSRStimeout時間內沒有收到反饋信息，則重發.若超過TTSRStimeout時間則報警.參數TRBCreaction和TTSRStimeout的取值見文獻[19].2.2系統模型分解由圖1可知，臨時限速命令的擬定、設置、取消由CTC、TSRS、RBC、TCC共同完成.文獻[19]中描述的臨時限速工作流程規定了各設備之間信息交互的順序性和實時性.建模的基本思路為：將臨時限速分為擬定、設置、取消3個流程分別建模.建模框圖如圖2所示.

CTC管轄范圍內的RBC和TCC在操作臨時限速時的工作流程基本一樣，只需建立一個RBC（TCC）的模型.因此，建模對象選取為CTC、TSRS、RBC（或TCC），其臨時限速模型分別為一個時間自動機，依次記為ACTC、ATSRS、ARBC_TCC，則臨時限速工作流程的時間自動機模型TA為以上3個時間自動機的積，即

A = ACTCATSRSARBC_TCC.

為了描述臨時限速嚴格的時間約束特性，設置時鐘集合X={T1，T2}.時鐘約束集

Φ（x）=T1≤TRBCreaction，

T2>TRBCtimeout，

T2≤TRBCtimeout，

T2>TRBCreaction，

T2≤TTSRStimeout，

T2>TTSRStimeout.

參數取值見文獻[19].

圖2臨時限速工作流程建模框圖

Fig.2Block diagram for working process of TSR

各成員時間自動機之間的通信通過同步通道實現，設置事件集

Σ1={ΣPlannedTSR，ΣCheckSuccess，ΣCancelTSR，

ΣVerfSuccess，ΣConfExecute，ΣWarning ，…}，

Σ2={ΣTSR，ΣCheckResult，ΣExecuteTSR，ΣCanTSR，

ΣExecuteResult，ΣCancelEXE，ΣExeCanResult， …}.

Σ1實現CTC與TSRS之間的同步信息交互，Σ2實現TSRS與RBC或TCC之間的同步信息交互.

以2.1節中安全功能屬性e、f及受限活性要求為例，說明各模塊之間的關系.

TSRS發送執行TSR命令的事件ExecuteTSR（ΣExecuteTSR∈Σ2），按照時間自動機的定義， ATSRS發生轉換e1（轉換e1～e5均為五元組），并將時鐘T1重置為0開始計時.同時， RBC（TCC）收到事件ExecuteTSR， ARBC_TCC發生轉換e2.

e1=〈SPreExe，ΣExecuteTSR，，{T1}，SWaitResult〉，

e2=〈SSendResult，ΣExecuteTSR，，，SExeTSR〉.

隨著T1時間的流逝，RBC（TCC）在TRBCreaction時間內向TSRS返回執行結果ExecuteResult（ΣExecuteResult∈Σ2）， ARBC_TCC與ATSRS同時發生轉換e3和e4.

e3={SExeTSR，ΣExecuteResult，

T1≤TRBCreaction，，SExeFinish}，

e4=〈SWaitResult，ΣExecuteResult，，，SRecExecResult〉.

令（SPreExe，ν）r1（SWaitesult，ν），（1）

（SSendResult，ν）r2（SSExeTSR，ν），（2）

（SSExeTSR，ν）r3（SSExeFinish，ν），（3）

（SSWaitResult，ν）r4（SSRecExecResult，ν），（4）

式中： ν∈TX，TX表示時鐘解釋的集合.

如果存在執行序列r1和r2使式（1）和（2）成立，那么說明TSRS發出了執行臨時限速的命令，同時，RBC（TCC）也收到了執行臨時限速的命令.

如果存在執行序列r3和r4使式（3）和（4）成立，那么說明RBC（TCC）在T_RBCreaction時間內返回了執行結果，同時，TSRS也收到了反饋結果.

是否存在執行序列r1、r2、r3和r4使式（1）～（4）成立，是下面自動驗證工具UPPAAL的驗證工作.以式（3）為例，依據BNF語法的定義，驗證語句可表示為A<>（（RBC_TCC.SSExeTSR）imply（RBC_TCC.SSExeFinish）and （T1

Fig.3Timed automata model for working process of TSR in CTC圖4RBC、TCC中臨時限速工作流程模型

Fig.4Timed automata model for working process of TSR in RBC and TCC 以上對臨時限速工作流程進行了模塊劃分，并用時間自動機語言規約了各模塊之間的關系，使整個臨時限速工作流程模型的層次更清晰.為了區分臨時限速的擬定、設置、取消模型，規定各設備設置臨時限速流程的位置用F命名，執行臨時限速流程的位置用S命名，取消臨時限速流程的位置用C命名，全局變量用V命名.

模型中，以“！”結尾的標記表示發出此信號時轉換發生；以“？”結尾的標記表示接收到該信號時轉換發生，以此實現各模型中相同的轉換同步發生.標有C的圓圈為堅定位置，表示下一個轉換必須無延遲地離開至少一個堅定位置[8].

圖5TSRS中臨時限速工作流程模型

Fig.5Timed automata model for working process of TSR in TSRS

3模型仿真與驗證驗證系統性質之前，需最大限度地保證建立的模型和真實系統的一致性.本文通過以下兩個方面實現這一需求：

（1） 詳細劃分臨時限速系統的功能.將臨時限速分為擬定、設置、取消3個流程，分別對每個流程建模.

（2） 依據臨時限速系統技術規范，嚴格按照時間自動機的語義和語法規約系統，然后利用UPPAAL工具建模，保證了模型和系統的一致性，為驗證結果的可信性提供了條件.

臨時限速系統的安全功能屬性驗證，可以歸結為時間自動機的可達性分析[18].系統的受限活性由位置的不變式和轉換的約束條件保證.以2.1節提出的安全功能屬性a為例，該安全功能屬性可以表述為：超過時間TTSRStimeout， RBC（TCC）既沒有發送執行臨時限速反饋信息， TSRS也沒有向CTC報警，該現象永遠不會發生，因此，其BNF驗證語句寫為

E（（not p1） and （not p2） and p3），（5）

p1：（RBC_TCC.SExeTSR） imply （RBC_TCC.SExeFinish），

p2：（CTC.SExeTSR）imply（CTC.idle），

p3：T2>TTSRStimeout.

p1表示時間自動機ARBC_TCC從狀態（SExeTSR， ν）可達狀態（SExeFinish， ν），即RBC（TCC）發出了執行臨時限速反饋信息ExecuteResult，not p1表示RBC（TCC）沒有發送執行臨時限速反饋信息.

p2表示時間自動機ACTC從狀態（SExeTSR， ν）可達狀態（idle， ν），即CTC收到了TSRS的報警信息Warning（ΣWarning∈Σ1）， not p2表示TSRS未向CTC報警.

p3表示超過時間TTSRStimeout.

UPPAAL驗證式（5）通不過，表明不存在任何執行序列，使執行序列中每個狀態均滿足表達式

（not p1） and （not p2） and p3，

即RBC（TCC）沒有發送執行反饋信息，同時TSRS也沒有向CTC報警，該現象永遠不會發生.系統的安全性得以驗證.2.1節提出的臨時限速系統的安全功能屬性和受限活性，均可按上述方式驗證.具體驗證內容和驗證結果見表1.由表1可見，除了系統模型死鎖（例如序號1情況）外，系統其它安全功能屬性和受限活性均滿足.在模型仿真過程中發現， TSRS與RBC信息交互時系統出現死鎖.死鎖原因如下： TSRS在TTSRStimeout時間內沒有接收到RBC的任何消息，則判定與RBC通信中斷； RBC在TRBCtimeout時間內沒有接收到TSRS的任何消息，則判定與TSRS通信中斷.

表1模型驗證內容和驗證結果

Tab.1Model verification content and verification results

序號驗證內容驗證語言結果安

全

功

能

屬

性

要

求1系統模型不死鎖Anot deadlock不通過2RBC（TCC）沒有發送執行反饋信息，TSRS也沒有向CTC報警.E（（not（（RBC_TCC.SExeTSR）imply（RBC_TCC.SExeFinish）））and（not（（CTC.SExeTSR）imply（CTC.idle）））and（T2>TTSRStimeout））不通過3CTC應能擬定、設置、取消臨時限速命令.E<>（（（CTC.idle）imply（CTC.FPreTSR））and（（CTC.idle）imply（CTC.SExeSuccess））and（（CTC.idle）imply（CTC. CConfExe）））通過4各設備應對接收到的臨時限速信息進行有效性校驗.E<>（（TSRS.FCheck）or（TSRS.SJudgeResult）or（TSRS.SJudRes）oror（TSRS.CJudResult）or（TSRS.CJudExeRes）or（RBC_TCC.SCheck）or（RBC_TCC.CJudge））通過5TSRS應保證先驗證后執行臨時限速命令.A（（（TSRS.SWaitCheck）imply（TSRS.SWaitResult））or（TSRS.FCheck imply TSRS.SActive））通過6TSRS應向RBC、TCC傳輸設置執行、取消執行等操作指令.E<>（（（（TSRS.SSend）imply（TSRS.SWaitCheck））and（（RBC_TCC.idle）imply（RBC_TCC.SCheck）））or（（（TSRS. CJudResult）imply（TSRS. CJudExeRes））and（（RBC_TCC. CJudge）imply（RBC_TCC. CExe））））通過7RBC、TCC能向TSRS反饋臨時限速命令的執行結果.E<>（（（RBC_TCC.SExeTSR）imply（RBC_TCC.SExeFinish）and（TSRS. SWaitResult）imply（TSRS.SRecExecResult）））通過受

限

活

性

要

求8RBC收到臨時限速指令后，能在TRBCreaction時間內返回執行結果。A<>（（RBC_TCC.SExeTSR）imply（RBC_TCC.SExeFinish）and（T（（TSRS.SWaitResult）imply（TSRS.SPreExe）and（T2>TRBCreaction）and（T2<=TTSRStimeout）and（（RBC_TCC.SExeTSR）imply（RBC_TCC.SSendResult）））通過10若超過TTSRStimeout時間，TSRS仍未收到反饋信息，則報警.A<>（（TSRS.SWaitResult）imply（TSRS.idle）and（T2>TTSRStimeout））通過

根據文獻[19]參數取值為

TTSRStimeout≤5 s，

TRBCtimeout≤3 s.

TSRS和RBC判定與對方通信中斷的時間不一致，導致了系統模型死鎖.這會影響行車效率，但不會危及行車安全，因為超過時間TTSRStimeout后， TSRS認為通信中斷，則向CTC返回操作失敗信息并報警.

將參數TTSRSreaction和TRBCreaction均設置為小于5 s，重新驗證表1中臨時限速系統的屬性，驗證內容和驗證語言不變.驗證結果顯示性質1驗證通過，表明系統模型死鎖消失；性質2～10驗證結果無變化，表明臨時限速系統其它安全功能屬性和受限活性依然滿足，未受這2個參數取值變化的影響.可見，從模型驗證的角度，可以將這2個參數都修正為小于5 s，以消除系統模型死鎖.但該參數的確定，仍需從列控系統的運用需求出發綜合考慮.4結束語提出了一種基于UPPAAL的臨時限速工作流程建模與驗證方法.采用時間自動機理論建立了CTCS3級列控系統臨時限速工作流程的時間自動機網絡模型.利用UPPAAL驗證工具，驗證了臨時限速系統的安全性和受限活性.

本文研究發現RBC和TSRS判斷通信超時中斷的時間參數有待優化，為后續設計提供了參考意見，表明該方法可有效地分析驗證臨時限速系統實時性.

致謝：本文工作得到軌道交通控制與安全國家重點實驗室自主課題重點項目（RCS2011ZZ001）的資助.

參考文獻：[1]郭震. CTCS各級系統中臨時限速技術運用的探討[J]. 科技信息，2011（16）： 111112.

GUO Zhen. Exploration of temporary speed restriction technology application at all levels in CTCS[J]. Science and Technology Information， 2011（16）： 111112.

[2]黃媛媛，董昱，趙宇坤. 臨時限速對列車運行影響的仿真研究[J]. 鐵道通信信號，2011，47（1）： 1315.

HUANG Yuanyuan， DONG Yu， ZHAO Yukun. Simulation study of temporary speed restriction on train operation[J]. Railway Signalling Communication， 2011， 47（1）： 1315.

[3]古天龍. 軟件開發的形式化方法[M]. 北京：高等教育出版社，2005： 424.

[4]呂繼東. 列車運行控制系統分層形式化建模與驗證分析[D]. 北京：北京交通大學，2011.

[5]曹源，唐濤，徐天華，等. 形式化方法在列車運行控制系統中的應用[J]. 交通運輸工程學報，2010，10（1）： 112126.

CAO Yuan， TANG Tao， XU Tianhua， et al. Application of formal methods in train control system[J]. Journal of Traffic and Transportation Engineering， 2010， 10（1）： 112126.

[6]周清雷，姬莉霞. 基于時間自動機的道岔自動控制研究[J]. 控制工程， 2004，11（增刊）： 146149.

ZHOU Qinglei， JI Lixia. On automatic turnout control based on timed automata[J]. Control Engineering of China， 2004， 11（Sup.）： 146149.

[7]ALUR R， DILL D L. A theory of timed automata[J]. Theoretical Computer Science， 1994， 126 ： 183235.

[8]OLDEROG E R， DIERKS H. Realtime systems[M]. London： Cambridge University Press， 2008： 137146.

[9]梁楠，王海峰. 基于SPN的CTCS3級列控系統RBC實時性能分析[J]. 鐵道學報，2011，33（2）： 6771.

LIANG Nan， WANG Haifeng. Realtime performance analysis of RBC system for ctcs lever 3 using stochastic Petri networks[J]. Journal of the China Railway Society， 2011， 33（2）： 6771.

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

[11]吳瓊，邵志清，劉剛. 基于著色時間Petri網的實時系統的形式驗證[J]. 計算機科學，2008，35（7）： 257260.

WU Qiong， SHAO Zhiqing， LIU Gang. Formal verification of realtime system based on colored time Petri net[J]. Computer Science， 2008， 35（7）： 257260.

[12]呂繼東，唐濤. 高速鐵路列控系統運營場景實時性的建模與驗證[J]. 鐵道學報，2011，33（6）： 5461.

L Jidong， TANG Tao. Modeling and verification of time constraints of operation scenarios of highspeed train control system[J]. Journal of the China Railway Society， 2011， 33（6）： 5461.

[13]承向軍，應志鵬，杜鵬. 高速列車ATP控車模式的形式化模型與安全分析[J]. 中國安全科學學報，2008，18（3）： 2832.

CHENG Xiangjun， YING Zhipeng， DU Peng. Formalization model of high speed trains in ATP control and its safety analysis[J]. China Safety Science Journal， 2008， 18（3）： 2832.

[14]曹源，唐濤，羅丹. 列車運行控制系統設計正確性的驗證方法[J]. 西南交通大學學報，2010，45（4）： 574579.

CAO Yuan， TANG Tao， LUO Dan. Method for verifying the correctness of train control system design[J]. Journal of Southwest Jiaotong University， 2010， 45（4）： 574579.

[15]XU Ke， PATTERSSON P， SIERSZECKI K. Verification of COMDESⅡ systems using UPPAAL with model transformation[C]∥The 14th IEEE International Conference on Embedded and RealTime Computing Systems and Applications. Los Alamitos： IEEE Computer Society， 2008： 153160.

[16]HESSEL A， LARSEN K G， MIKUCIONIS M. Testing realtime systems using UPPAAL[J]. Lecture Notes in Computer Science， 2008， 4949： 77117.

[17]BEHRMANN G， LARSEN K G. UPPAALpresent and future[C]∥Proceedings of the 40th IEEE Conference on Decision and Control. New York： IEEE， 2001： 28812886.

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

[19]鐵道部科學技術司，鐵道部運輸局. CTCS3級列控系統標準規范系列：客運專線列控系統臨時限速技術規范[M].北京：中國鐵道出版社，2008： 69，2730.