CTCS-3級列控車載設備的形式化建模與驗證

何濤 韓敬佳

doi：10.11835/j.issn.1000.582X.2023.09.012

收稿日期：2020-06-09

基金項目：國家自然科學基金資助項目（U2268206）。

Supported by National Natural Science Foundation of China（U2268206）.

作者簡介：何濤（1977—），男，教授，碩導，主要從事軌道交通測試研究方向研究。

通信作者：韓敬佳（1994—），女，碩士，主要從事列控系統建模分析方向研究，（E-mail）1558155326@qq.com。

摘要：CTCS-3級列控系統安全苛求性較高，而列控車載設備是CTCS-3級列控系統的主體，主要功能是對列車進行操縱和控制，保證列車安全運行的關鍵。通過分析CTCS-3級列控車載設備之間的信息交互以及車載安全計算機中工作模式的轉換規則，采用有色Petri網（CPN）建立車載設備的信息交互模型以及工作模式轉換模型，使用ASK-CTL分支時序邏輯公式驗證了模型的死標識、死鎖以及分析工作模式下的系統行為等特性，驗證構建的CPN模型符合系統規范要求的流程及規則，可為相關安全苛求系統的設計提供一定參考。

關鍵詞：列控系統；車載設備；模式轉換；有色Petri網

中圖分類號：TP391；U284 ?????????文獻標志碼：A ?????文章編號：1000-582X（2023）09-120-10

Formal modeling and verification of CTCS-3 train control on-board equipment

HE Tao^a，b， HAN Jingjia^a

（a. School of Automation and Electrical Engineering; b. Gansu Research Center of Automation Engineering Technology for Industry &Transportation， Lanzhou JiaoTong University， Lanzhou 730070， P. R. China）

Abstract： The CTCS-3 train control system is subject to stringent safety requirements， with the train control on-board equipment serving as its core. This equipment plays a vital role in operating and controlling the train， ensuring the overall safety of train operation. In this study， the information interaction between CTCS-3 train control on-board devices and the work mode conversion rules in the on-boar safety computer was analyzed. To establish a comprehensive model， colored Petri nets （CPN） were used， enabling the construction of an information interaction model and work mode transformation model for the on-board equipment. To validate the models effectiveness， the ASK-CTL branching sequence logic formula was used to verify its performance concerning dead identification， deadlock and transferability under various working modes. The results show that the CPN model conforms to the system specification requirements， adhering to the expected process and rules. This research provides valuable ingishgts and serves as a reference for the design of the relevant security demanding systems.

Keywords： train control system; on-board equipment; mode conversion; colored Petri net

近年來，中國對于時速超過250 km/h的鐵路采用的是CTCS-3級列車運行控制系統（以下簡稱C3級列控系統）^[1]，車載設備是C3級列控系統的重要組成部分，其安全性、可靠性直接影響列車運行安全。因此對列控車載設備進行建模，驗證車載設備系統功能及轉換流程滿足相關系統需求規范，對保證列車運行安全，改進系統需求規范具有重要意義。

目前，國內外對Petri網的運用以及對列控系統的建模與仿真做了許多研究，德國學者Hardi^[2]以現有的ERTMS/ETCS規范為基礎，采用著色Petri網（CPN）構建了形式化模型。應用一種集成的面向事件和數據的方法，顯示系統在自己的Petri網層次上的不同方面。中國學者采用UML建模方法^[3]，對CTCS-3級列控車載設備進行分析與建模，依據系統模型提出車載設備測試案例和測試序列設計。UML是一種半形式化建模方法，不能對構建的模型進行驗證，具有一定局限性，給系統的驗證和分析帶來困難。另外還有時間自動機建模方法^[4]可對CTCS-3級列控車載設備中的車載安全計算機VC和無線閉塞中心RBC進行建模，驗證車載設備的系統特性。時間自動機是形式化建模方法，適合描述反應式系統，對于復雜系統，構造時間自動機模型的工作量比較大，不適合描述具有并發狀態的系統。?C3級列控車載設備是對安全性要求較高的復雜系統。僅僅依靠傳統建模語言無法完全描述出CTCS-3級列控車載設備模式轉換的多樣性，因此，需要一種能夠描述復雜系統的建模語言對模式轉換進行分層建模，能夠更好表現系統的功能及結構。對比目前現有UML以及時間自動機等建模方法，Petri網有直觀的圖形表示，又可以引入數學方法對建立的模型進行驗證與分析^[5]。用有色Petri網CPN（colored petri net）建立模型完成后可以直接用工具CPNTools進行驗證和分析，對于C3級列控系統這種復雜系統，可以對其進行分層描述來簡化模型結構，減小系統驗證復雜度。因此，選用有色Petri網更加適用于列控系統的建模，解決系統空間爆炸問題，更加適用于復雜系統的建模。

1車載設備功能需求分析

CTCS-3級列控系統的主要功能有保障行車安全、保證運輸效率、保證乘客舒適度等^[6]。C3級列控系統主要由2部分組成：一部分是提供監控列車所需要的線路允許速度、行車許可等基礎數據的地面設備；另一部分是根據相關設備傳送上來的地面信息監控列車運行速度、運行條件的車載設備。

C3級列控車載設備是C3級列控系統的核心設備，采用故障-安全設計，車載設備主要構成有：主控單元車載安全計算機（VC）、?GSM-R無線通信、軌道電路信息讀取器（STM）、應答器信息接收單元（BTM）、列車接口單元（TIU）、人機界面（DMI）、等^[7]。C3級列控車載設備構成如圖1所示，其主要功能包括：

1）?向RBC發送列車運行所需動態信息，處理來自車載的調車請求。

2）?處理來自RBC的緊急停車消息，根據情況對列車實行控制命令。

3）?接收無線閉塞中心RBC發送來的正常行車許可MA、列車位置報告等。

4）?根據接收到的應答器信息，計算行車曲線及列車位置校正。

5）?接收軌道電路傳送的線路參數信息。

6）?實時測量列車運行速度和行走距離并計算目標距離模式控制曲線。

7）?RBC/RBC的交接。

8）?DMI的管理、司法數據的記錄功能。

車載安全計算機VC是C3級列控車載系統的控制核心，主要完成車載設備工作模式的判斷及轉換，根據從其他模塊獲取的信息，必要時對列車實施制動，以保證車載系統對列車安全防護功能的具體實現和操作。因此，選用車載安全計算機中工作模式轉換作為車載設備安全計算機的主要狀態。

2CPN模型的構建

2.1建模研究思路

根據有色Petri網建模語言的建模流程，將對車載設備的建模思想總體分為3部分：一是系統功能分析，根據系統規范了解車載設備間信息交互和車載設備中工作模式轉換條件；二是根據系統功能構建CPN模型；三是根據系統屬性對構建的模型進行驗證。CTCS-3級列控車載設備形式化建模與驗證的總體框架圖如圖2所示。

具體建模流程如下：

1）?根據《CTCS-3級列控系統需求規范（SRS）》^[8]中的要求，采用有色Petri網對CTCS-3級列控系統車載設備各部分之間的信息交互以及車載安全計算機中工作模式轉換進行建模。

2）?基于有色Petri網構建出車載設備以及模式轉換的CPN模型，其中對系統模型采用分層（2層）的構建規則，根據系統需求規范中的模式轉換條件，將車載安全計算機設為替代變遷，它的子頁模型為各模式之間的轉換。

3）?在CPN Tools工具中引入分支時序邏輯ASK-CTL公式對構建的CPN模型進行形式化驗證，分析模型是否滿足《CTCS-3級列控系統需求規范（SRS）》要求的車載設備信息交互功能以及模型是否符合車載設備模式轉換流程，若不滿足，則重新采用有色Petri網對車載設備進行建模。

4）?在模型驗證結果正確的基礎上，分析系統的屬性是否滿足車載設備信息交互功能以及是否符合模式轉換流程。

2.2有色Petri網建模方法

有色Petri網是一種形式化的建模語言，與其他建模語言相比有色Petri網構建的CPN模型更加直觀形象，還能對復雜系統進行分層建模來描述系統的功能和行為，大大簡化系統模型的復雜度。CPN作為一種圖形化的表達形式，主要由庫所（P用圓表示，代表系統的狀態）、變遷（T用矩形表示，代表系統狀態的改變或動作的執行）、托肯（token代表數據類型）、有向弧（A用箭頭表示，代表托肯的流動方向）組成。

ASK-CTL模型檢驗用于驗證建模語言有色Petri網描述的系統模型與設計的系統性質是否一致。將系統需要驗證的性質用ASK-CTL公式進行描述與驗證，如果系統模型符合描述的驗證語言則返回結果“true”，如果不滿足則返回“false”，以便根據驗證結果對設計進行修改^[9]。

基于ASK-CTL公式的模型驗證算法如圖3所示。

在CPN Tools中對系統模型進行檢測時常用的函數是eval_node（），函數的格式是：val eval_node（VALUE self， NODE* node），其中self是ASK-CTL庫中自帶的查詢函數^[10]，例如自循環終端的檢測常用OutNodes（）函數，當返回結果為“There is No loop Terminal！”時，表示系統模型不存在自循環；死鎖的檢測常用InvalidTerminal（）函數，當返回結果為“No Deadlock Markings！”時，表示系統模型不存在死鎖。

2.3構建車載設備CPN模型

C3級列控車載設備是對安全性要求較高的復雜系統。僅僅依靠傳統的建模語言無法完全描述出CTCS-3級列控車載設備模式轉換的多樣性，因此，需要一種能夠描述復雜系統的建模語言對模式轉換進行分層建模，能夠更好表現出系統功能及結構。

C3級列控車載設備中的核心設備是車載安全計算機，保證車載系統對列車安全防護功能的具體實現和操作^[11]。車載安全計算機主要實現車載設備工作模式的判斷及轉換，實現列車基本運營場景；RBC收到來自車載的行車許可MA請求和列車位置報告（train position）后，根據相關信息計算生成行車許可MA，并將臨時限速信息、線路信息等通過GSM-R發送給安全計算機用以生成速度控制曲線；考慮司機對列車運行狀態的影響，司機的主要狀態是確認安全計算機傳來的信息，必要時對列車實施人工制動；列車的主要狀態是向安全計算機提供列車速度及位置信息后接收安全計算機發送的對列車控制要求以及制動命令；應答器主要是用于列車定位，應答器發送的線路參數、臨時限速等信息主要是為了滿足C3級列控系統后備模式C2級列控系統的控制，但RBC切換、級間轉換等信息是利用地面應答器發送的。根據系統需求規范中提出的車載設備和司機相關職責構建出車載設備之間信息交互CPN模型如圖4所示。

CPN模型以車載安全計算機為中心，車載設備主要變遷設為RBC、司機、列車、應答器，將其與車載安全計算機的信息交互設為CPN模型的系統狀態即庫所，根據車載設備的功能可知庫所的主要狀態如表1所示。

車載設備的工作過程由工作模式不斷轉換來實現，因此將模式轉換作為安全計算機的主要狀態進行建模。CTCS-3級列控車載設備主要包括待機模式（SB）、完全監控模式（FS）、調車模式（SH）、目視行車模式（OS）、引導模式（CO）、休眠模式（SL）、冒進防護模式（TR）、冒進后防護模式（PT）、隔離模式（IS）9種工作模式^[12]。系統需求規范中規定了各工作模式轉換之間的轉換條件。車載設備工作模式轉換實例如表2所示。

CTCS-3級列控系統需求規范的模式轉換部分定義了列控車載設備的工作模式、與模式有關的功能以及各模式之間的轉換條件^[13?14]。主要工作模式對應的車載設備職責：

1）?待機模式SB是一種默認模式，司機不能對其進行選擇，車載設備啟動，自檢和測試通過后自動進入待機模式；

2）?當車載設備接收到來自RBC的行車許可MA，列車數據和線路數據都具備后，車載設備轉入完全監控模式FS，根據動態曲線監控列車運行，并向司機顯示列車速度；

3）?調車模式SH用于列車進行調車作業時，由司機選擇調車，車載設備應向RBC申請授權并在進入調車模式后與RBC斷開連接；

4）?當地面設備故障，車載設備顯示禁止但列車需要繼續運行時，由司機選擇轉入目視行車模式OS，從RBC接收請求，列車每運行一定距離需司機確認一次；

5）?引導模式CO用于開放引導信號，接收RBC的請求后司機應在此模式下檢查軌道占用；

6）?休眠模式SL用于非本務端車載設備，如果開啟（異常操作），應轉入待機模式SB；

7）?當車載設備停用，隔離車載設備的制動功能后，列控車載設備處于隔離模式IS，應向司機指示車載設備已被隔離；

8）?當車載設備輸出緊急制動命令時進入冒進防護模式TR，應要求司機確認，列車實施緊急制動；

9）?冒進后防護模式PT時車載設備應緩解緊急制動，司機選擇啟動，向RBC發送MA請求。

C3級列控車載設備工作模式轉換的CPN模型如圖5所示。工作模式的轉換是車載安全計算機的主要狀態，因此在模型中將工作模式設為庫所，模式間轉換條件設為替代變遷，用標號pntn表示，p表示模式轉換的優先等級，數字越小優先；t表示模式轉換條件，在文獻[8]《CTCS-3級列控系統需求規范（SRS）》有明確規范。在CPNTools工具的Declarations下定義聲明MODE為9種工作模式轉換，WRIECOMM設為變量“true”。安全計算機初始工作模式為SB，因此SB的初始標識為1′（6，true）。根據系統需求規范中模式轉換條件以及模式轉換中車載設備職責，構建模式間轉換條件的CPN子頁模型，如圖6為SB轉SH模式的CPN子頁模型，由圖5可知，SB轉SH變遷狀態為p4t6，表示優先級為4級，轉換條件為6（司機請求調車模式后，從RBC接收到“允許調車”信息）和（列車停車），模型中庫所集P={SB，Driver Shunt Request，RBC Received，On-board Received，SH}，庫所集T={Train Stop Info，Send MSG To RBC，Send Shunt Permission Info，p4_t6}，如圖6所示。若在工作模式下轉換成功，則驗證結果顯示“true”，否則顯示“false”。

3CPN模型的驗證與分析

3.1CPN模型的驗證

有色Petri網建模語言對模型的驗證是用ASK-CTL分支時序邏輯公式描述系統的性質，通過對系統模型進行系統邏輯性的驗證分析，例如系統的自循環終端特性、死鎖特性等來證明系統模型是否可執行，從而得出構建的CPN模型是否滿足系統規范要求的規則以及各組件之間的交互是否符合規范流程。根據對系統需求規范中系統屬性分析，對構建的車載設備CPN功能模型以及模式轉換CPN模型進行了自循環終端檢測、死鎖和活鎖檢測驗證。驗證結果如下：

對所建車載設備CPN模型進行自循環終端檢測是為了驗證系統中死標識的合理性，對模型執行ASK-CTL公式，由圖7可知驗證結果為“There is no loop terminal！”。

對車載設備CPN模型進行死鎖分析，執行ASK-CTL公式，由圖8可知驗證結果為“No Deadlock Markings！”。

活鎖的檢查是根據狀態空間報告中OG和SCCG節點和弧的數量相同，即同構的，則系統不存在活鎖。部分狀態空間報告如圖9所示。

采用ASK-CTL公式對模型進行自循環驗證和死鎖分析等，是為了驗證模型的邏輯特性，只有系統死標識合理，無死鎖及活鎖等特性，模型才是安全可執行的。另外，還可通過CPNTools工具對模型進行功能行為特性的檢查：如驗證系統的活性、可達性、有界性、轉移性和公平性等^[15]。例如針對圖6系統工作狀態下進行模式轉換規則驗證，車載設備初始工作模式始終為待機SB模式，驗證系統是否存在某條路徑，使待機模式SB轉入調車模式SH，驗證執行結果“true”，表示系統模型之間可轉移。

3.2模型驗證結果分析

根據模型驗證結果分析系統的屬性，只有系統模型中不存在死鎖、活鎖等屬性，才能驗證系統功能屬性的正確性^[16]。

1） 車載設備自循環終端

自循環終端檢測是為了驗證系統死標識的合理性，由圖7的驗證結果“There is no loop terminal！”?可知CPN模型中不存在自循環終端，驗證了系統模型中死標識是合理的，系統模型正確。說明構建的CPN模型滿足《CTCS-3級列控系統需求規范（SRS）》要求的車載設備信息交互流程。

2） 模式轉換無死鎖

無死鎖是指系統不會永遠停留在一個狀態。根據圖8ASK-CTL描述的系統性質驗證結果?“No Deadlock Markings！”，可知系統在模式轉換過程中無死鎖，系統模型正確。

3） 模式轉換無活鎖

檢查系統活鎖的目的是為了發現系統中存在的死循環。由圖9可知，“State Space”中節點數和弧與“Scc Graph”中節點數和弧的數量相同，即同構，說明系統中不存在活鎖，系統模型正確。

系統模型既無死鎖也無活鎖，系統功能屬性正確，說明構建的CPN模型滿足《CTCS-3級列控系統需求規范（SRS）》要求的模式轉換功能。

4） 工作狀態下系統的行為特性

轉移性是指模型中一個模式與另一個模式之間存在遷移關系，即系統可經過轉移從一個模式轉換到另一個模式，建模驗證返回的執行結果為true，表示系統從SB狀態可以經過轉換步驟遷移到SH狀態，由此可知構建的模式轉換CPN模型符合系統規范要求的CTCS-3級列控車載設備模式轉換條件。

4結??語

由于CTCS-3級列控車載設備是一個安全苛求性較高的復雜系統，而有色Petri網建模方法能夠對模型進行分層建模，適用于復雜系統建模。研究主要分析了列控車載設備功能設計時涉及到的安全問題，對CTCS-3 級列控系統車載設備之間的功能信息交互以及車載設備中安全計算機主要狀態工作模式轉換的各模式之間轉換路徑和模式之間具體轉換流程進行了CPN建模，并在驗證工具CPN Tools中使用時序邏輯公式ASK-CTL對所建模型系統功能性質進行描述，根據驗證結果分析得到系統功能模型與相關系統需求規范的一致性。此外，提出的有色Petri網建模方法也適用于其他安全性要求較高的復雜系統建模驗證研究。該建模驗證方法能夠對系統進行圖形化描述，對復雜系統還可以進行分層建模，大大減少系統空間爆炸的概率。形式化的建模方法能夠使建模工具對系統模型進行驗證確保系統設計規則的正確性和安全性，減少復雜系統設計規則的不可靠性，對安全苛求性要求較高的復雜系統的設計具有一定的參考意義。

參考文獻

［1］??張曙光. CTCS-3級列控系統總體技術方案[M]. 北京： 中國鐵道出版社， 2008： 26-37.

Zhang S G. Overall technical scheme of CTCS-3 train control system[M]. Beijing： China Railway Publishing House， 2008： 26-37.（in Chinese）

［2］??Hardi Hr， Michael M. Modelling functionality of ?train control system using petri nets[C]//Fm-rail-bok Workshop. Madrid： DLR， 2013：1-6.

［3］??何文鋒. 基于UML的CTCS-3級列控車載設備建模、仿真和測試研究[D]. 北京： 北京交通大學， 2009.

He W F. Research on modeling， simulation and testing of CTCS-3 train control vehicle equipment based on UML[D].Beijing： Beijing Jiaotong University， 2009. （in Chinese）

［4］??曹加云. 基于時間自動機的CTCS-3級列控車載設備建模與驗證[D]. 成都： 西南交通大學， 2010.

Cao J Y. Modeling and verification of CTCS-3 train control vehicle equipment based on time automata[D].Chengdu： Southwest Jiaotong University， 2010. （in Chinese）

［5］??牟小玲， 丁曉明， 張望. 基于Petri網的測試用例生成研究進展[J]. 重慶交通大學學報（自然科學版）， 2012， 31（1）： 163-167.

Mu X L， Ding X M， Zhang W. Research progress in test case generation based on petri nets[J]. Journal of Chongqing Jiaotong University （Natural Science）， 2012， 31（1）： 163-167.（in Chinese）

［6］??中國鐵路總公司. CTCS-3級列車運行控制系統[M]. 北京： 中國鐵道出版社， 2013.

China Railway Corporation. CTCS-3 train operation control system [M]. Beijing： China Railway Publishing House， 2013.

［7］??Wang R， Zheng W， Liang C， et al. An integrated hazard identification method based on the hierarchical Colored Petri Net[J]. Safety Science， 2016， 88： 166-179.

［8］??鐵道部科技司. CTCS-3級列控系統標準規范-CTCS-3級列控系統系統需求規范（SRS）（第一冊）[S]. 北京： 中國鐵道出版社， 2009.

Department of Science and Technology.Ministry of railways standard specification for CTCS-3 class train control system （SRS） （volume 1） [S]. Beijing： China Railway Publishing House， 2009.（in Chinese）

［9］??馬國富， 劉文良， 周建勇， 等. 基于ASK-CTL的有色Petri網模型檢驗算法研究[J]. 計算機應用與軟件， 2015， 32（10）： 302-305， 333.

Ma G F， Liu W L， Zhou J Y， et al. Study on coloured petri net model checking based on ask-ctl[J]. Computer Applications and Software， 2015， 32（10）： 302-305， 333.（in Chinese）

［10］??趙曉宇， 楊志杰， 呂旌陽. 基于有色Petri網的車載設備模式轉換測試序列生成方法[J]. 中國鐵道科學， 2017， 38（4）： 115-122.

Zhao X Y， Yang Z J， Lv S Y. A Method for generating test sequence of on-board equipment mode conversion based on colored petri nets [J]. China Railway Science， 2017， 38（4）： 115-122.（in Chinese）

［11］??胡少強. 基于STPA和有色Petri網的列控系統安全分析[D]. 北京： 北京交通大學， 2018.

Hu S Q. Safety analysis of train control system based on STPA and colored petri net[D].Beijing： Beijing Jiaotong University， 2018. （in Chinese）

［12］??Koh K Y， Seong P H. SMV model-based safety analysis of software requirements[J]. Reliability Engineering & System Safety， 2009， 94（2）： 320-331.

［13］??趙偉慧. 基于場景的列控車載設備測試用例自動生成方法研究[D]. 北京： 北京交通大學， 2014.

Zhao W H. Research on automatic generation method of test cases for train control vehicle equipment based on scene[D].Beijing： Beijing Jiaotong University， 2014. （in Chinese）

［14］??Lh V， Hong L. Formal development and verification of railway control systems- in the context of ERTMS/ETCS level 2[D]. Copenhagen： DTU， 2015：13-20.

［15］??Huang W L， Peleska J. Complete model-based equivalence class testing[J]. International Journal on Software Tools for Technology Transfer， 2016， 18（3）： 265-283.

［16］??Jensen K， Kristensen L M， Wells L. Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems[J]. International Journal on Software Tools for Technology Transfer， 2007， 9（3/4）： 213-254.

（編輯??侯湘）