列控系統等級轉換的建模研究

楊璐 陶漢卿

摘要：等級轉換是高速鐵路列車運行控制系統的一個主要運營場景。當列車通過CTCS-3級區域和CTCS-2級區域邊界時，車載子系統、無線閉塞中心、司機、預告應答器以及轉換應答器之間存在大量的信息交互過程，并對列車的安全運行和行車效率有直接的影響，因此有必要采取形式化建模方式對該過程進行分析和驗證。文章根據時間自動機理論對CTCS-3級向CTCS-2級轉換的過程進行建模，并應用UPPAAL對轉換過程各子系統的信息交互一致性和實時性進行驗證。結果表明，該過程滿足交互一致性和實時性的規范要求。

關鍵詞：等級轉換;時間自動機;UPPAAL;實時性

0 引言

中國列車運行控制系統CTCS（Chinese Train Control Systm）按其地面設備、車載設備配置和功能共分為5個等級[1]，即CTCS-0～CTCS-4。CTCS-3級列控系統通過GSM-R實現車-地無線大容量通信，利用RBC子系統計算獲得的移動授權以及其他的控車信息實現高速鐵路列車安全、高效運行。C3級列控系統采用分布式結構，具有連續式響應和實時性強的特點，采取有效的方法實現系統特性的描述和驗證已成為C3級列控系統的一項重要研究領域[2]。系統規范作為列控系統設計開發的起點和基礎，一旦其存在潛在缺陷，很可能會對運營列車的安全運行帶來風險[3]。因此，在C3級列控系統研發過程中對其各個場景進行建模、仿真和驗證，發現系統潛在缺陷，提高系統安全性，輔助系統開發，提高開發效率顯得尤為重要。列車跨越CTCS-3級區域和CTCS-2級區域邊界過程作為高速鐵路動車組列車運行過程的一個很重要的環節，是保障動車組安全運行和提高行車效率的基礎。因而，當列車跨越CTCS-3級區域和CTCS-2級區域邊界點時，針對C3向C2交接控車權并控制列車正常運行的建模研究就顯得尤為重要。

CTCS-3級列控系統作為一個典型的安全苛求系統和實時系統，根據國際電工委員會標準（IEC624425和IEC61508），針對高安全苛求系統，可通過形式化方法進行建模和驗證[4-5]。面向對象的同一建模語言（Unified Modeling Language，UML）具有較強的交互流程描述能力，且易于使用。文獻[6]作者采用UML方法對CTCS-1級列控系統的車載ATP進行建模，并采用計算機語言編程的方法進行了驗證。不難看出UML方法缺乏相應的驗證工具，無法直接實現模型驗證，不利于錯誤的有效定位。相比UML，時間自動機有其對應的驗證平臺UPPAAL，且UPPAAL工具平臺的模型驗證功能自動化程度高，當系統不滿足給定的性質時，在模擬器窗口可以實現對驗證錯誤的有效定位。因此，本文根據時間自動機理論對列車跨越CTCS-3級區域和CTCS-2級區域分界點時的等級轉換功能進行研究，建立了轉換過程中的列車模型、無線閉塞中心模型、預告應答器模型、切換應答器模型以及司機模型，基于該模型，對CTCS-3級轉CTCS-2級的功能進行驗證。

1 C3向C2轉換過程分析

當線路上運行的列車即將離開CTCS-3級管轄區域并駛入CTCS-2級管轄范圍區域時，RBC將根據距離轉換點前一定距離處設置的等級轉換預告應答器LTA的預告信息，向車載控制器發送等級轉換的預告命令[7]。列車繼續運行至距離等級轉換執行應答器LTO一定距離時，向司機申請轉換確認。當列車運行至前端通過轉換執行應答器LTO時，RBC根據LTO的轉換執行信息，向車載控制器發送轉換執行命令。當列車完全通過轉換點后，車載控制器與RBC結束通信。詳見圖1。

2 建立C3轉C2的信息交互圖

通過對列車從CTCS-3級管轄范圍駛入CTCS-2級管轄范圍的過程分析，可將車載控制器由CTCS-3級轉換為CTCS-2級，司機、RBC、預告應答器LTA以及執行應答器LTO之間的信息交互過程簡化為3個階段（見圖2）：

C3轉C2預告階段：列車正常運行在CTCS-3級線路上時，RBC為列車提供行車許可。當列車進入等級轉換區，運行至等級轉換預告應答器LTA，接收轉換預告信息，RBC向列車下達轉換預告命令。此時車載控制器根據命令激活CTCS-2級控制單元，進行實際運行速度與C2允許速度比較過程。

C3轉C2等級轉換執行階段：當列車繼續運行至前端通過轉換點LTO時，執行轉換命令，列車自動轉至CTCS-2級控車。若之前司機未進行轉換確認，當車載轉入C2控車后的5 s內允許司機繼續進行確認[8]。

列車尾部通過轉換點，結束與RBC通信階段：當列車繼續運行至尾部通過轉換點LTO后，車載控制器與RBC斷開連接，結束通信。

3 列車跨越C3-C2分界點的等級轉換模型

3.1 UPPAAL工具

1995年，Aalborg大學和Uppsala大學聯合提出UPPAAL，可以通過時間自動機子模型來描述各個子系統的屬性和行為，多個單獨的子模型組成整個系統完整的時間自動機網絡模型。通過UPPAAL平臺下的模擬器窗口可以準確對其錯誤的路徑進行定位，從而修正模型。UPPAAL驗證平臺為系統規范的驗證提供了BNF語法[9-10]，具體語法含義如表1所示。

3.2 CTCS-3轉CTCS-2的UPPAAL模型

根據前面所述對列車從CTCS-3級管轄范圍駛入CTCS-2級管轄范圍的過程分析，建立了列車跨越CTCS-3級區域向CTCS-2級分界點的等級轉換的時間自動機網絡模型TA=TATrain||TARBC||TADriver||TALTA||TALTO。列車跨越CTCS-3級區域向CTCS-2級分界點等級轉換的時間自動機網絡模型由Train子模型，RBC子模型，Driver子模型，LTA子模型，LTO子模型組成，分別如圖3（a）～（e）所示。模型中a！表示某個子系統發送端發送消息事件a，a？表示某個子系統接收端接收消息事件a，以保證子模型中相同的轉換同時發生。

4 模型的仿真與驗證

在UPPAAL模擬器中對列車跨越CTCS-3級區域向CTCS-2級區域進行等級轉換過程中出現的列車通過預告應答器LTA過程、收到轉換預告命令后激活C2控制單元進行實際速度與C2允許速度比較的過程、請求司機進行轉換確認的過程，到達轉換執行應答器LTO執行轉換的過程，列車尾部越過分界點后與RBC斷開連接結束通信會晤的過程進行多次模擬。按照CTCS系統中，列車跨越CTCS-3級區域向CTCS-2級區域進行等級轉換時，根據CTCS各子系統的性能和功能要求，對所建立的列車跨越CTCS-3級區域向CTCS-2級區域進行等級轉換的時間自動機網絡模型進行驗證。用BNF語言描述的系統性能和功能要求如下：

（1）系統無死鎖：A[]not deadlock，通過。

（2）列車能完成激活C2控制單元，越過轉換分界點后轉換為CTCS-2級控車以及尾部越過分界點后斷開與RBC連接的功能：E<>（（Train.T_C2UnitActive）or（Train.T_C2-Control）or（Train.T_UnConnect）），驗證通過。

（3）當司機在列車運行距離轉換邊界前5 s內未進行等級轉換確認時，司機可在列車越過轉換分界點轉為CTCS-2級系統工作后5 s內繼續進行確認：A<>（（Train.T_WaitConf1）imply（Train.T_C2 Control）and（T1>=5 and T2<5）），驗證通過。

（4）車載控制器激活C2控制單元后會對運行速度進行監督，只有當運行速度低于C2允許速度時，才能實施等級轉換由CTCS-3級轉為CTCS-2級：E[]（（Train.T_C2UnitActive）imply（Train.T_C2-Control）and（NowSpeed<=250）），驗證通過。

（5）轉換預告點LTA距C3與C2轉換邊界的距離>10 s（車載與RBC通信時間5 s加司機確認時間5 s）：A<>（（Train.T_A-rriveLTA）imply（Train.T_1ArriveLTO）and（T3>10）），驗證通過。

5 結語

本文采用時間自動機理論，以列車跨越CTCS-3級區域向CTCS-2級區域進行等級轉換時CTCS-3級列控系統各個子系統之間的信息交互為依據，建立了列車跨越CTCS-3級區域向CTCS-2級區域運行時的時間自動機網絡模型，并對所建立的模型進行了多次模擬仿真和修正。最后對列車由CTCS-3級轉換為CTCS-2級所需的功能和性能要求進行了驗證。驗證結果表明：列車跨越CTCS-3級區域向CTCS-2級區域進行等級轉換時，等級轉換功能的完備性和正確性，保證了列車跨越C3/C2分界點時系統的安全性和受限活性。因此，此種方法適用于復雜系統需求規范的驗證。

參考文獻：

[1]董 昱.區間信號與列車運行控制系統[M].北京：中國標準出版社，2008.

[2]陳永剛，丁春平.基于TRSL的RBC等級轉換場景研究[J].鐵道標準設計，2016，60（8）：122-129.

[3]唐 濤，郜春海，黃友能，等.CJ/T407-2012城市軌道交通基于通信的列車自動控制系統技術要求[M].北京：中國標準出版社，2012.

[4]IEC.IEC62425：2007.Railway Applications-Communication，Signaling and Processing Systems-Safety Related Electronic for Signaling [S].IEC.2007.

[5]IEC.IEC61508：2005.Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems [S].IEC.2005.

[6]張紫菡，劉中田，王穎卓，等.基于UML語言的CTCS-1級車載ATP功能建模分析[J].鐵路計算機應用.2017，26（5）：5-10.

[7]張曙光.CTCS-3級列控系統總體技術方案[M].北京：中國標準出版社，2008.

[8]丁春平.基于域+Timed RAISE的列控系統等級轉換場景建模與驗證[D].蘭州：蘭州交通大學，2016.

[9]王永偉.基于構件的形式化方法在軟件開發中的應用研究[D].哈爾濱：哈爾濱工程大學，2010.

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