基于UML與UPPAAL的高鐵列控臨時限速切換場景建模與驗(yàn)證

摘要：為提高高速鐵路列控臨時限速命令在臨時限速服務(wù)器（temporary speed restriction server，TSRS）與無線閉塞中心（radio block center， RBC）跨界重疊區(qū)域信息傳遞過程的時效性和安全性，建立TSRS切換與RBC切換跨界重疊區(qū)域限速流程的數(shù)學(xué)模型，根據(jù)中國列車運(yùn)行控制系統(tǒng)（Chinese train control system，CTCS）CTCS-2/CTCS-3高鐵列控系統(tǒng)間臨時限速命令交互的特點(diǎn)，采用統(tǒng)一建模語言（unified modeling language，UML）與時間自動機(jī)模型理論相結(jié)合的方法，采用形式化驗(yàn)證工具UPPAAL尋找臨時限速命令在跨界重疊區(qū)域信息傳遞的不足和漏洞。研究結(jié)果表明：列控臨時限速是高鐵安全運(yùn)行的重要組成部分，其與高鐵列控高鐵調(diào)度集中（centralized traffic control，CTC）、RBC、列控中心（train control center，TCC）等相關(guān)子系統(tǒng)有頻繁的信息交互，不同子系統(tǒng)間信息傳遞過程不同，Timer（時間控制器）、Resend（重發(fā)控制器）、TSRS和RBC時間自動機(jī)數(shù)學(xué)模型驗(yàn)證結(jié)果為TSRS切換與RBC切換信息在跨界重疊區(qū)域的傳遞時間小于3 s，且時間自動機(jī)模型信息通道無鎖死情況，大大提高高鐵列車運(yùn)行的時效性和安全性。

關(guān)鍵詞：臨時限速；時間自動機(jī)；UML；UPPAAL；高鐵列控

中圖分類號：U284.48文獻(xiàn)標(biāo)志碼：A文章編號：1672-0032（2024）03-0031-08

引用格式：周翔.基于UML與UPPAAL的高鐵列控臨時限速切換場景建模與驗(yàn)證［J］.山東交通學(xué)院學(xué)報，2024，32（3）：31-38.

ZHOU Xiang. Modeling and verification of high-speed railway train control temporary speed limit switching scenarios based on UML and UPPAAL［J］.Journal of Shandong Jiaotong University，2024，32（3）：31-38.

0 引言

截至2023年底，我國高速鐵路運(yùn)營里程已達(dá)4.5萬 km^[1]。高速鐵路的飛速發(fā)展對運(yùn)營安全性和時效性也提出更高要求。高鐵列控系統(tǒng)是保障高鐵安全運(yùn)行的核心，其中二級臨時限速系統(tǒng)又是重中之重^[2]。在傳遞臨時限速命令時，須嚴(yán)格遵守中國國家鐵路集團(tuán)有限公司下發(fā)的技術(shù)規(guī)范要求，如文獻(xiàn)[3]等。但實(shí)際運(yùn)行中信息在跨界重疊區(qū)域傳遞時又存在特殊性，研究跨界重疊區(qū)域信息傳遞對提升高鐵列車運(yùn)行的時效性和安全性具有重要意義^[4-5]。

康仁偉^[6]提出基于時間自動機(jī)的列控系統(tǒng)建模與驗(yàn)證方法，以中國列車運(yùn)行控制系統(tǒng)（Chinese train control system，CTCS）CTCS-3級臨時限速和等級轉(zhuǎn)換運(yùn)營場景為例，說明該建模與驗(yàn)證方法的有效性；趙榮亮^[7]采用時間自動機(jī)理論對臨時限速系統(tǒng)進(jìn)行建模，并結(jié)合高鐵調(diào)度集中（centralized traffic control，CTC）系統(tǒng)調(diào)度臺分界口、CTCS等級轉(zhuǎn)換，建立各自的時間自動模型，采用工具UPPAAL對模型進(jìn)行時序邏輯的仿真，得到系統(tǒng)工作流程的仿真時序圖，驗(yàn)證各模型的功能；安越^[8]采用統(tǒng)一建模語言（unified modeling language，UML）和時間自動機(jī)相結(jié)合，對無線閉塞中心（radio block center，RBC）進(jìn)行建模驗(yàn)證，保證RBC控車的實(shí)時性和安全性；朱偉等^[9]總結(jié)RBC出行車許可異常縮短和無線通信超時故障，提出有效提高CTCS-3級列控系統(tǒng)運(yùn)用質(zhì)量的建議。高鐵列控臨時限速的研究目前還停留在無跨界信息的常規(guī)區(qū)段，較少涉及2個不同系統(tǒng)在交叉重疊區(qū)域臨時限速信息傳遞的復(fù)雜性，研究手段單一。

本文采用UML和UPPAAL相結(jié)合的辦法，對高鐵列控子系統(tǒng)信息交互時重疊區(qū)域臨時限速信息的交互過程進(jìn)行建模，并采用消息順序圖（message sequence charts，MSC）、UML時序圖和時間自動機(jī)模型相互轉(zhuǎn)換方式進(jìn)行逐層分析，驗(yàn)證列控系統(tǒng)臨時限速服務(wù)器（temporary speed restriction server，TSRS）和RBC信息交互重疊區(qū)域的時效性和安全性。

1 TSRS切換與RBC切換重疊區(qū)域限速流程臨時限速場景分析

高鐵列控系統(tǒng)臨時限速命令的交互過程具有階段性和區(qū)域性，不同的子系統(tǒng)間信息傳遞過程不同，在跨界重疊區(qū)域的信息傳遞過程更復(fù)雜。相鄰區(qū)段的列控系統(tǒng)均會產(chǎn)生信息傳遞的重疊區(qū)域，重疊區(qū)域不同子系統(tǒng)間也會產(chǎn)生信息交互。本文以列控系統(tǒng)跨界區(qū)域A、B兩側(cè)作為重疊區(qū)域，建立臨時限速信息在重疊區(qū)域的數(shù)學(xué)模型，分析系統(tǒng)的安全性和時效性^[10-12]。

高鐵列控系統(tǒng)與子系統(tǒng)信息交互的穿插重疊區(qū)域是關(guān)系高鐵安全運(yùn)行的特殊場景，跨界信息的交互處于不同的列控設(shè)備控制區(qū)段，交互過程復(fù)雜，需通過A、B兩側(cè)不同的設(shè)備間互聯(lián)互通完成信息的安全傳遞，其復(fù)雜性和不同的時效性易導(dǎo)致重疊區(qū)域的信息產(chǎn)生錯亂，影響高鐵的安全運(yùn)行，進(jìn)路信息和列車數(shù)據(jù)未得到有效傳輸。需建立UML和時間自動機(jī)模型，對信息交互過程進(jìn)行建模驗(yàn)證，分析模型的安全性和時效性^[13-14]。臨時限速在重疊區(qū)域的信息交互過程如圖1所示。

2 UML模型

UML模型表達(dá)內(nèi)容全面、詳細(xì)、簡單、多樣，但不具有廣泛性，對需要形式化驗(yàn)證的模型不具有驗(yàn)證作用。從3個步驟分析具體模型：1）繪制MSC消息順序圖；2）從MSC轉(zhuǎn)換為UML時序圖；3）由UML時序圖轉(zhuǎn)換為時間自動機(jī)模型圖，將最終轉(zhuǎn)換圖形由UPPAAL形式化驗(yàn)證工具輸入巴科斯范式（Backus-Naur form，BNF）驗(yàn)證語句進(jìn)行驗(yàn)證。本文主要研究重疊區(qū)域切換場景下的臨時限速信息交互，采用MSC構(gòu)建可視化時間信息交互模型，以此為依據(jù)同步構(gòu)建UML模型和時間自動機(jī)模型^[15-17]。

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

定義1：MSC是多個實(shí)體間進(jìn)行形式化語言描述，并采用二維圖形概括消息交互通信實(shí)例的圖形化語言，構(gòu)建關(guān)于區(qū)域關(guān)系的描述。形式化語言詞組包括lt;area1gt; contains lt;area2gt;、lt;area1gt; is followed by lt;area2gt;、lt;area1gt; is associated with lt;area2gt;、lt;area1gt; is attached to lt;area2gt;、lt;area1gt; above lt;area2gt;、{lt;gt;}set。lt;area1gt; contains lt;area2gt;表示區(qū)域1包含區(qū)域2，通常用于描述嵌套或包含關(guān)系；lt;area1gt; is followed by lt;area2gt;表示區(qū)域1緊隨在區(qū)域2后，通常用于描述順序關(guān)系；lt;area1gt; is associated with lt;area2gt;表示區(qū)域1與區(qū)域2相關(guān)聯(lián)，可能指二者間存在某種關(guān)聯(lián)或聯(lián)系；lt;area1gt; is attached to lt;area2gt;表示區(qū)域1附加在區(qū)域2上，描述二者間的連接或附屬關(guān)系，區(qū)域2必須為1個或1組圖形符號，構(gòu)成消息傳遞路徑，如圖2所示；lt;area1gt; above lt;area2gt;表示區(qū)域1在區(qū)域2的上方并相連，如圖3所示，通常用于描述空間位置關(guān)系；{lt;gt;}set表示1個集合，通常用于收集或組織具有某種共同特征或?qū)傩缘脑亍?/p>

消息域中的消息在實(shí)例與環(huán)境間進(jìn)行交換，即消息入（message in）消息出（message out）^[18]，如圖4所示。

定義2：：：=定義符。左邊為非終結(jié)符，右部為終結(jié)符；lt; gt;括號內(nèi)的符號為非終結(jié)符，需進(jìn)一步定義。

MSC的主體包括參與者、消息、時間順序和交互關(guān)系，通過對象沿生命線的交互展現(xiàn)對象間的通信和消息觸發(fā)關(guān)系，強(qiáng)調(diào)消息傳遞的時間順序和交互細(xì)節(jié)。MSC的解釋主體為^[19-21]：

lt;msc body areagt;：：={lt;instance layergt;lt;text layergt;lt;gate def layergt;lt;event layergt;lt;connector layergt;}set，

其中，臨時限速M(fèi)SC主體為：

lt;SetTSRS areagt;：：={lt;Protocal（RBCToTSRS） layergt;lt;Protocal（TSRSToRBC） layergt;lt;ActTSRS layergt;

lt;ExeTSRS layergt;lt;NoticeCase layergt;}set。

臨時限速命令的交互MSC模型如圖5所示。

Resend—重發(fā)控制器；Timer—時間控制器；ActTSRS—激活臨時限速服務(wù)器命令；SetTSRS—設(shè)置臨時限速服務(wù)器命令；ActFail—激活失??；Protocal（RBCToTSRS）—無線閉塞中心與臨時限速服務(wù)器的協(xié)議；CancTSRS—取消臨時限速服務(wù)器命令；ActSucc—激活成功；ExeTSRS—執(zhí)行臨時限速服務(wù)器命令；Protocal（TSRSToRBC）—臨時限速服務(wù)器與無線閉塞中心的協(xié)議；NoticeCase—預(yù)告信息。

2.2 基于UML時序圖的建模

在UML時序圖中分為橫軸、縱軸和生命線，分別表示時間進(jìn)行線、各對象的狀態(tài)和系統(tǒng)運(yùn)行的主要元素，系統(tǒng)運(yùn)行對象的工作狀態(tài)呈階梯狀態(tài)^[22]。在UML時序圖中不同信息的交互對象由帶實(shí)心箭頭的生命線相互連接，表示從一種狀態(tài)轉(zhuǎn)移到另一種狀態(tài)。這種對象狀態(tài)的遷移需具體量化的時間變量表達(dá)，持續(xù)的時間變量為t。根據(jù)2.1節(jié)中MSC中交互的狀態(tài)信息，建立TSRS切換與RBC切換重疊區(qū)域限速流程的UML時序圖。TSRS切換與RBC切換重疊區(qū)域限速流程中各信息交互對象的狀態(tài)如表1所示^[23]。

采用MSC直觀表述4個對象的信息交互流程，采用UML時序圖表示時間信息交互過程。主要事件和發(fā)生對象的表述方式為：timeout-T==0表示與TSRS建立的信息通信未超時；timeout-R==0表示與RBC建立信息通信未超時；PressResend==1表示臨時限速信息和無線閉塞中心信息交互的可循環(huán)性，防止死循環(huán)；PressTimer==1表示時間不會鎖止，時間狀態(tài)正循環(huán)。設(shè)置時間約束條件分別為：ConnTSRS（與臨時限速服務(wù)器建立聯(lián)系）時間狀態(tài)為10 s，ConnRBC（與無線閉塞中心建立聯(lián)系）時間狀態(tài)為5 s，PressResend（運(yùn)行重發(fā)控制器）循環(huán)時間為1 s，PressTimer（運(yùn)行時間控制器）防鎖止時間循環(huán)為2 s^[24-26]。根據(jù)以上信息建立TSRS切換與RBC切換重疊區(qū)域限速流程的UML時序圖模型，如圖6所示。

2.3 UML時序圖向時間自動機(jī)模型的轉(zhuǎn)換

時序圖中的生命線對應(yīng)時間自動機(jī)模型中的temple，表示1個對象或子系統(tǒng)；時序圖中的狀態(tài)state對應(yīng)時間自動機(jī)模型中的位置location，時間自動機(jī)的初始狀態(tài)idle替換UML時序圖中的初始狀態(tài)start，時序圖中的消息message對應(yīng)時間自動機(jī)模型中的通道channel，時間線timeline對應(yīng)時鐘clock，事件event對應(yīng)監(jiān)管guard，根據(jù)對應(yīng)關(guān)系，在建立的時間自動機(jī)位置模型圖中添加消息通道、時間約束和事件監(jiān)管的信息。

2.4 基于時間自動機(jī)的系統(tǒng)建模

UPPAAL是用于驗(yàn)證時間自動機(jī)模型正確性的工具，它支持系統(tǒng)的建模、模擬和形式化特性驗(yàn)證，能避免狀態(tài)空間爆炸問題，保證系統(tǒng)的正確性和安全性。采用形式化驗(yàn)證語言BNF驗(yàn)證UPPAAL，語法及其含義為Prop：：= Elt;gt;p|E[]p|Alt;gt;p|A[]p|p→q^[27]。

建立TSRS與RBC切換重疊區(qū)域時間自動機(jī)模型，根據(jù)2.1節(jié)和2.2節(jié)中MSC消息順序圖和UML時序圖中對信息的交互流程和時間事件的發(fā)生順序，對重疊區(qū)域信息的交互流程，即Resend、Timer、TSRS和RBC等4個建模對象，進(jìn)行建模，建立TA_Resend、TA_Timer、TA_TSRS、TA_RBC等4個時間自動機(jī)模型，如圖7所示。

設(shè)TSRS與RBC切換重疊區(qū)域時間自動機(jī)模型為：

T_A=lt;S，S⁰，A，X，I，Egt;，

式中：S、S⁰、A、X、I、E分別為時間自動機(jī)建模的過程狀態(tài)、初始狀態(tài)、觸發(fā)事件、時間參數(shù)、整數(shù)變量、狀態(tài)轉(zhuǎn)移路徑。

以T_A，RBC時間自動機(jī)為例說明，過程狀態(tài)S={idle，P_CheckMSG1，P_BuildConnect}，初始狀態(tài)S⁰=idle；觸發(fā)事件A={MSG？，MSGconfirm！}，時間參數(shù)X={T₁，T_rbc，T_RBCtimeout}，整數(shù)變量I={MSG？，MSGconfirm！}，狀態(tài)轉(zhuǎn)移路徑E={idle，P_CheckMSG4，P_Control，P_TransferMA，idle}，其中，“P_”“E_”開頭分別表示限速命令的擬定、下達(dá)過程。

由圖7可知：Resend可在保障信息交互循環(huán)時防止信息循環(huán)鎖死，Timer是保障在無時間延遲的情況下防止時間信息鎖死，二者在保證無時間信息鎖死的情況下進(jìn)行RBC和TSRS時間自動機(jī)模型信息傳遞的閉循環(huán)。

RBC切換時間自動機(jī)模型中，Trbcgt;RBCtimeout時，說明信息傳遞失敗，移交命令超時，根據(jù)操作者要求，可重新下達(dá)命令，從Idle重新發(fā)送。由圖7c）可知：有3個時間遷移變量端分別為E_TSRSabSendToRBCab、E_TSRSabSendToTSRSba、E_TSRSabSendToRBCba，為臨時限速服務(wù)器和無線閉塞中心的A、B兩側(cè)分別進(jìn)行通信信息的交叉?zhèn)鬟f。圖7設(shè)3個時間約束，Ttsrslt;=T_TSRStimeoutamp;amp;T0lt;=1表示TSRSab和RBCab的信息交互時間不超過1 s，Ttsrslt;=T_TSRStimeoutamp;amp;T1lt;=3表示TSRSab和TSRSba的信息交互時間不超過3 s，Ttsrslt;=T_TSRStimeoutamp;amp;T2lt;=3表示TSRSab和RBCba的信息交互時間不超過3 s。

TSRS與RBC切換重疊區(qū)域的主要位置為：Resend（重發(fā)控制器）、Timer（時間控制器）、E_Handover （移交限速命令）、E_TransferMA（傳遞移動授權(quán)信息）、E_Send（發(fā)送信息）、E_Receive（接收信息）、P_BuildConnect（建立通信鏈接）、P_Start（開始傳遞信息）、P_CheckMSG1（檢查1通信通道）、P_Control（控制傳遞信息）。

TSRS與RBC切換重疊區(qū)域的主要通信通道為：HandoverOrder（移交命令）、SendConfirm（發(fā)送確認(rèn)消息）、transferMA（傳遞移動授權(quán)信息）、TCCSend TCC（發(fā)送信息）、TCCInfoReq TCC（信息需求）、RBCback RBC（返回信息）、RBCInfoOK RBC（信息返回正確）、MSGconfirm（信息通道確認(rèn)）、Open（開放重發(fā)命令）、Circle（時間循環(huán)命令）。

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

將UPPAAL驗(yàn)證器導(dǎo)入已構(gòu)建的時間自動機(jī)模型，同時應(yīng)用語法BNF驗(yàn)證TSRS與RBC切換重疊區(qū)域時間自動機(jī)模型滿足安全性和受限活性的要求。

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

1）系統(tǒng)沒有死鎖。A[]not deadlock，驗(yàn)證通過。

2）RBC建立通信協(xié)議，完成RBC通信信息的傳遞。

Elt;gt;（（RBC.P_BuildConnect）and（RBC.P_Start）and（RBC.P_Control）and（RBC.P_Handover）），驗(yàn)證通過。

3）TSRS和RBC切換信息移交正常完成。

Elt;gt;（（RBCa.Idle）imply（RBCa.P_Handover）and（RBCb.Idle）imply（RBCb.P_Handover）and（TSRSa.Idle）imply（TSRSa.E_TSRSaSendToRBCb）and（TSRSa.Idle）imply（TSRSb.E_TSRSbSendToRBCa）），驗(yàn)證通過。

4）在列車非減速狀態(tài)下RBC切換信息正常移交。

Elt;gt;（（RBC.newspeedgt;=RBC.oldspeed）imply（RBC.P_Handover）），驗(yàn)證通過。

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

1）TSRS和RBC在A、B兩側(cè)1 s內(nèi)完成通信信息的移交。

A[]（（TSRSab.ControlRBCab）imply（TSRSab.E_TSRSabSendToRBCab）and（T0lt;=1）），驗(yàn)證通過。

2）TSRS_A和TSRS_B在3 s內(nèi)完成臨時限速命令的切換。

A[]（（TSRSa.ControlTSRSb）imply（TSRSab.E_TSRSabSendToTSRSba）and（T1lt;=3）），驗(yàn)證通過。

3）TSRS_A和RBC_B，TSRS_B和RBC_A在3 s內(nèi)進(jìn)行臨時限速命令的雙向傳遞，同時在A、B兩側(cè)對無線閉塞中心的信息傳遞做出必要的時間限制。

A[]（（TSRSab.ControlRBCba）imply（TSRSabE_TSRSabSendToRBCba）and（T2lt;=3）），驗(yàn)證通過。

通過驗(yàn)證分析可知：跨界重疊區(qū)域的時間自動機(jī)模型通過UPPAAL驗(yàn)證工具的狀態(tài)驗(yàn)證，滿足安全性和時效性應(yīng)用，達(dá)到客運(yùn)專線列控系統(tǒng)臨時限速技術(shù)規(guī)范要求。驗(yàn)證語句在驗(yàn)證中正常通過，形成模擬器狀態(tài)圖。

4 結(jié)束語

本文采用MSC和UML建立TSRS與RBC切換重疊區(qū)域的基礎(chǔ)時間約束模型，為方便自動機(jī)模型的轉(zhuǎn)換，在MSC和UML的建模過程中描述時間約束條件和狀態(tài)轉(zhuǎn)移過程。采用時間自動機(jī)方法建立TSRS與RBC切換重疊區(qū)域時間自動機(jī)模型，采用形式化驗(yàn)證工具UPPAAL進(jìn)行模型驗(yàn)證。結(jié)果表明TSRS與RBC切換重疊區(qū)域信息在具體時間限制內(nèi)可順利完成信息交互，說明其具有安全性和時效性，保證高鐵列控系統(tǒng)在TSRS和RBC切換情況下的安全運(yùn)行。

后續(xù)的研究中可進(jìn)一步論證2個相鄰區(qū)段TSRS和TSRS重疊區(qū)域信息交互的復(fù)雜性，為鐵路通信信號研究提供技術(shù)支撐。

參考文獻(xiàn)：

[1] 新京報. 我國高鐵達(dá)到4.5萬公里[N/OL].（2024-01-09）[2024-06-30].http：//www.xinhuanet.com/fortune/20240109/7e9f592edefe48d8b9a0a67fab44da2b/c.html.

[2] 宋莉， 劉伯鴻. 基于UPPAAL的列控系統(tǒng)臨時限速建模與驗(yàn)證[J].鐵路計(jì)算機(jī)應(yīng)用， 2020， 29（5）： 12-16.

[3] 中國國家鐵路集團(tuán)有限公司，中國鐵道科學(xué)研究院集團(tuán)有限公司通信信號研究所.列控中心接口規(guī)范 第7部分：列控中心與臨時限速服務(wù)器接口：Q/CR 864.7—2021[S].北京：中國鐵道出版社，2021.

[4] 馮婷婷. 基于 UML 活動圖模型測試用例生成的研究[D].衡陽：南華大學(xué)，2020.

[5] 宋菲. 基于時間自動機(jī)的 RBC 控車場景建模與驗(yàn)證[D].成都：西南交通大學(xué)， 2017.

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

[7] 趙榮亮.列控系統(tǒng)TSRS形式化建模分析與驗(yàn)證[D].成都：西南交通大學(xué)，2014.

[8] 安越.基于UML和TA的RBC系統(tǒng)形式化建模與分析[D].蘭州：蘭州交通大學(xué)，2016.

[9] 朱偉，馮飛.RBC典型問題原因分析及處置[J].鐵道通信信號，2022，58（10）：35-39.

[10] 施汀瑞. 基于時間自動機(jī)的 RBC 切換的建模分析與實(shí)現(xiàn)[D].北京：北京交通大學(xué)， 2019.

[11] 彭麗維，宋鵬飛，江雪瑩，等.基于模型的聯(lián)鎖軟件測試用例生成方法[J].鐵路通信信號工程技術(shù)，2022，19（11）：32-36.

[12] 鐵道部.客運(yùn)專線 CTCS-2 級列控系統(tǒng)列控中心技術(shù)規(guī)范：科技運(yùn)[2007]158號[S/OL].（2023-06-20）[2018-11-11].https：//www.doc88.com/p-7778434233848.html.

[13] 李耀， 張曉霞， 郭進(jìn). 鐵路信號系統(tǒng)軟件測試建模方法[J].西南交通大學(xué)學(xué)報， 2022， 57（2）：392-400.

[14] 于瀟. CBTC 聯(lián)鎖系統(tǒng)的形式化建模與驗(yàn)證方法研究[D].北京：中國鐵道科學(xué)研究院， 2017.

[15] 張廣泉. 形式化方法導(dǎo)論[M].2版.北京：清華大學(xué)出版社， 2023.

[16] 賀偉. 基于時間自動機(jī)的行車許可的建模與驗(yàn)證[D].成都：西南交通大學(xué)， 2017.

[17] 王觀寧. 基于 UPPAAL 的聯(lián)鎖進(jìn)路控制流程建模與驗(yàn)證[D].北京：北京交通大學(xué)， 2009.

[18] 張鵬基. 基于時間自動機(jī)的 ZC 子系統(tǒng)建模與驗(yàn)證[D].北京：北京交通大學(xué)， 2017.

[19] 張志斌，張耀回.空口監(jiān)測在 CTCS-3 級列控系統(tǒng)無線超時分析中的應(yīng)用研究[J].鐵道通信信號，2022，58（10）：71-75.

[20] 劉艷平，李海浩.基于序列圖和狀態(tài)圖的軟件測試用例生成方法[J].電子設(shè)計(jì)工程，2019，27（24）：167-170.

[21] 盧佩玲，郝韜，徐強(qiáng).高鐵聯(lián)絡(luò)線不利條件下CTCS3CTCS2 等級轉(zhuǎn)換方案研究[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2022，66（12）：137-142.

[22] 王建. 基于隨機(jī) Petri 網(wǎng)的高鐵列控系統(tǒng) C2/C3 等級轉(zhuǎn)換過程建模及仿真[D].成都：西南交通大學(xué)， 2015.

[23] 袁磊，王俊峰，康仁偉，等.CTCS-3級列控系統(tǒng)臨時限速建模與驗(yàn)證[J].西南交通大學(xué)學(xué)報，2013，48（4）：708-714.

[24] 周翔，武曉春.基于MSC與UPPAAL的高鐵跨界臨時限速建模與驗(yàn)證[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2016，60（10）：126-131.

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

[26] 李勝，王維.普速鐵路CTC中心站集中控制技術(shù)的研究與應(yīng)用[J]．鐵路通信信號，2021，57（12）：12-15.

[27] HORSTE M Z， SCHNIEDER E. Modeling train control system with petri nets-a functional reference-architecture[C]//Proceedings of the IEEE International Conference on System， Man and Cybernetics. [S.l.]：IEEE， 2000：884471.

Modeling and verification of high-speed railway train control temporary

speed limit switching scenarios based on UML and UPPAAL

ZHOU Xiang

Binzhou Jiaotong Bureau， Binzhou 256600， China

Abstract：To improve the timeliness and safety of the information transmission process in the cross-border overlapping area between the temporary speed restriction server （TSRS） and the radio block center （RBC） for high-speed rail train control temporary speed restriction commands， a mathematical model of the TSRS switch and RBC switch cross-border overlapping area speed restriction process is established. Based on the characteristics of temporary speed restriction command interaction between the Chinese Train Control System （CTCS） CTCS-2/CTCS-3 high-speed rail train control systems， a combined approach of unified modeling language （UML） and Timed Automata model theory is adopted. The formal verification tool UPPAAL is used to identify deficiencies and vulnerabilities in the information transmission of temporary speed restriction commands in the cross-border overlapping area. The research results indicate that train control temporary speed restriction is an important component for the safe operation of high-speed rail. There is frequent information interaction between temporary speed restriction， centralized traffic control （CTC）， RBC， train control center （TCC）， and other related subsystems. The information transmission processes between different subsystems vary. The verification results of the Timer， Resend， TSRS， and RBC Timed Automata mathematical models show that the transmission time of TSRS switch and RBC switch information in the cross-border overlapping area is less than 3 s， and the information channel of the Timed Automata model does not lead to deadlock situations， significantly improving the timeliness and safety of high-speed rail train operation.

Keywords：temporary speed limit; timed automata; UML; UPPAAL; high-speed railway train control

（責(zé)任編輯：王惠）