楊璐 陶漢卿

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

關(guān)鍵詞：等級(jí)轉(zhuǎn)換;時(shí)間自動(dòng)機(jī);UPPAAL;實(shí)時(shí)性

0 引言

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

CTCS-3級(jí)列控系統(tǒng)作為一個(gè)典型的安全苛求系統(tǒng)和實(shí)時(shí)系統(tǒng)，根據(jù)國際電工委員會(huì)標(biāo)準(zhǔn)（IEC624425和IEC61508），針對(duì)高安全苛求系統(tǒng)，可通過形式化方法進(jìn)行建模和驗(yàn)證[4-5]。面向?qū)ο蟮耐唤ＵZ言（Unified Modeling Language，UML）具有較強(qiáng)的交互流程描述能力，且易于使用。文獻(xiàn)[6]作者采用UML方法對(duì)CTCS-1級(jí)列控系統(tǒng)的車載ATP進(jìn)行建模，并采用計(jì)算機(jī)語言編程的方法進(jìn)行了驗(yàn)證。不難看出UML方法缺乏相應(yīng)的驗(yàn)證工具，無法直接實(shí)現(xiàn)模型驗(yàn)證，不利于錯(cuò)誤的有效定位。相比UML，時(shí)間自動(dòng)機(jī)有其對(duì)應(yīng)的驗(yàn)證平臺(tái)UPPAAL，且UPPAAL工具平臺(tái)的模型驗(yàn)證功能自動(dòng)化程度高，當(dāng)系統(tǒng)不滿足給定的性質(zhì)時(shí)，在模擬器窗口可以實(shí)現(xiàn)對(duì)驗(yàn)證錯(cuò)誤的有效定位。因此，本文根據(jù)時(shí)間自動(dòng)機(jī)理論對(duì)列車跨越CTCS-3級(jí)區(qū)域和CTCS-2級(jí)區(qū)域分界點(diǎn)時(shí)的等級(jí)轉(zhuǎn)換功能進(jìn)行研究，建立了轉(zhuǎn)換過程中的列車模型、無線閉塞中心模型、預(yù)告應(yīng)答器模型、切換應(yīng)答器模型以及司機(jī)模型，基于該模型，對(duì)CTCS-3級(jí)轉(zhuǎn)CTCS-2級(jí)的功能進(jìn)行驗(yàn)證。

1 C3向C2轉(zhuǎn)換過程分析

當(dāng)線路上運(yùn)行的列車即將離開CTCS-3級(jí)管轄區(qū)域并駛?cè)隒TCS-2級(jí)管轄范圍區(qū)域時(shí)，RBC將根據(jù)距離轉(zhuǎn)換點(diǎn)前一定距離處設(shè)置的等級(jí)轉(zhuǎn)換預(yù)告應(yīng)答器LTA的預(yù)告信息，向車載控制器發(fā)送等級(jí)轉(zhuǎn)換的預(yù)告命令[7]。列車?yán)^續(xù)運(yùn)行至距離等級(jí)轉(zhuǎn)換執(zhí)行應(yīng)答器LTO一定距離時(shí)，向司機(jī)申請(qǐng)轉(zhuǎn)換確認(rèn)。當(dāng)列車運(yùn)行至前端通過轉(zhuǎn)換執(zhí)行應(yīng)答器LTO時(shí)，RBC根據(jù)LTO的轉(zhuǎn)換執(zhí)行信息，向車載控制器發(fā)送轉(zhuǎn)換執(zhí)行命令。當(dāng)列車完全通過轉(zhuǎn)換點(diǎn)后，車載控制器與RBC結(jié)束通信。詳見圖1。

2 建立C3轉(zhuǎn)C2的信息交互圖

通過對(duì)列車從CTCS-3級(jí)管轄范圍駛?cè)隒TCS-2級(jí)管轄范圍的過程分析，可將車載控制器由CTCS-3級(jí)轉(zhuǎn)換為CTCS-2級(jí)，司機(jī)、RBC、預(yù)告應(yīng)答器LTA以及執(zhí)行應(yīng)答器LTO之間的信息交互過程簡化為3個(gè)階段（見圖2）：

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

C3轉(zhuǎn)C2等級(jí)轉(zhuǎn)換執(zhí)行階段：當(dāng)列車?yán)^續(xù)運(yùn)行至前端通過轉(zhuǎn)換點(diǎn)LTO時(shí)，執(zhí)行轉(zhuǎn)換命令，列車自動(dòng)轉(zhuǎn)至CTCS-2級(jí)控車。若之前司機(jī)未進(jìn)行轉(zhuǎn)換確認(rèn)，當(dāng)車載轉(zhuǎn)入C2控車后的5 s內(nèi)允許司機(jī)繼續(xù)進(jìn)行確認(rèn)[8]。

列車尾部通過轉(zhuǎn)換點(diǎn)，結(jié)束與RBC通信階段：當(dāng)列車?yán)^續(xù)運(yùn)行至尾部通過轉(zhuǎn)換點(diǎn)LTO后，車載控制器與RBC斷開連接，結(jié)束通信。

3 列車跨越C3-C2分界點(diǎn)的等級(jí)轉(zhuǎn)換模型

3.1 UPPAAL工具

1995年，Aalborg大學(xué)和Uppsala大學(xué)聯(lián)合提出UPPAAL，可以通過時(shí)間自動(dòng)機(jī)子模型來描述各個(gè)子系統(tǒng)的屬性和行為，多個(gè)單獨(dú)的子模型組成整個(gè)系統(tǒng)完整的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型。通過UPPAAL平臺(tái)下的模擬器窗口可以準(zhǔn)確對(duì)其錯(cuò)誤的路徑進(jìn)行定位，從而修正模型。UPPAAL驗(yàn)證平臺(tái)為系統(tǒng)規(guī)范的驗(yàn)證提供了BNF語法[9-10]，具體語法含義如表1所示。

3.2 CTCS-3轉(zhuǎn)CTCS-2的UPPAAL模型

根據(jù)前面所述對(duì)列車從CTCS-3級(jí)管轄范圍駛?cè)隒TCS-2級(jí)管轄范圍的過程分析，建立了列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)分界點(diǎn)的等級(jí)轉(zhuǎn)換的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型TA=TATrain||TARBC||TADriver||TALTA||TALTO。列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)分界點(diǎn)等級(jí)轉(zhuǎn)換的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型由Train子模型，RBC子模型，Driver子模型，LTA子模型，LTO子模型組成，分別如圖3（a）～（e）所示。模型中a！表示某個(gè)子系統(tǒng)發(fā)送端發(fā)送消息事件a，a？表示某個(gè)子系統(tǒng)接收端接收消息事件a，以保證子模型中相同的轉(zhuǎn)換同時(shí)發(fā)生。

4 模型的仿真與驗(yàn)證

在UPPAAL模擬器中對(duì)列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)區(qū)域進(jìn)行等級(jí)轉(zhuǎn)換過程中出現(xiàn)的列車通過預(yù)告應(yīng)答器LTA過程、收到轉(zhuǎn)換預(yù)告命令后激活C2控制單元進(jìn)行實(shí)際速度與C2允許速度比較的過程、請(qǐng)求司機(jī)進(jìn)行轉(zhuǎn)換確認(rèn)的過程，到達(dá)轉(zhuǎn)換執(zhí)行應(yīng)答器LTO執(zhí)行轉(zhuǎn)換的過程，列車尾部越過分界點(diǎn)后與RBC斷開連接結(jié)束通信會(huì)晤的過程進(jìn)行多次模擬。按照CTCS系統(tǒng)中，列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)區(qū)域進(jìn)行等級(jí)轉(zhuǎn)換時(shí)，根據(jù)CTCS各子系統(tǒng)的性能和功能要求，對(duì)所建立的列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)區(qū)域進(jìn)行等級(jí)轉(zhuǎn)換的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型進(jìn)行驗(yàn)證。用BNF語言描述的系統(tǒng)性能和功能要求如下：

（1）系統(tǒng)無死鎖：A[]not deadlock，通過。

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

（3）當(dāng)司機(jī)在列車運(yùn)行距離轉(zhuǎn)換邊界前5 s內(nèi)未進(jìn)行等級(jí)轉(zhuǎn)換確認(rèn)時(shí)，司機(jī)可在列車越過轉(zhuǎn)換分界點(diǎn)轉(zhuǎn)為CTCS-2級(jí)系統(tǒng)工作后5 s內(nèi)繼續(xù)進(jìn)行確認(rèn)：A<>（（Train.T_WaitConf1）imply（Train.T_C2 Control）and（T1>=5 and T2<5）），驗(yàn)證通過。

（4）車載控制器激活C2控制單元后會(huì)對(duì)運(yùn)行速度進(jìn)行監(jiān)督，只有當(dāng)運(yùn)行速度低于C2允許速度時(shí)，才能實(shí)施等級(jí)轉(zhuǎn)換由CTCS-3級(jí)轉(zhuǎn)為CTCS-2級(jí)：E[]（（Train.T_C2UnitActive）imply（Train.T_C2-Control）and（NowSpeed<=250）），驗(yàn)證通過。

（5）轉(zhuǎn)換預(yù)告點(diǎn)LTA距C3與C2轉(zhuǎn)換邊界的距離>10 s（車載與RBC通信時(shí)間5 s加司機(jī)確認(rèn)時(shí)間5 s）：A<>（（Train.T_A-rriveLTA）imply（Train.T_1ArriveLTO）and（T3>10）），驗(yàn)證通過。

5 結(jié)語

本文采用時(shí)間自動(dòng)機(jī)理論，以列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)區(qū)域進(jìn)行等級(jí)轉(zhuǎn)換時(shí)CTCS-3級(jí)列控系統(tǒng)各個(gè)子系統(tǒng)之間的信息交互為依據(jù)，建立了列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)區(qū)域運(yùn)行時(shí)的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，并對(duì)所建立的模型進(jìn)行了多次模擬仿真和修正。最后對(duì)列車由CTCS-3級(jí)轉(zhuǎn)換為CTCS-2級(jí)所需的功能和性能要求進(jìn)行了驗(yàn)證。驗(yàn)證結(jié)果表明：列車跨越CTCS-3級(jí)區(qū)域向CTCS-2級(jí)區(qū)域進(jìn)行等級(jí)轉(zhuǎn)換時(shí)，等級(jí)轉(zhuǎn)換功能的完備性和正確性，保證了列車跨越C3/C2分界點(diǎn)時(shí)系統(tǒng)的安全性和受限活性。因此，此種方法適用于復(fù)雜系統(tǒng)需求規(guī)范的驗(yàn)證。

參考文獻(xiàn)：

[1]董 昱.區(qū)間信號(hào)與列車運(yùn)行控制系統(tǒng)[M].北京：中國標(biāo)準(zhǔn)出版社，2008.

[2]陳永剛，丁春平.基于TRSL的RBC等級(jí)轉(zhuǎn)換場景研究[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2016，60（8）：122-129.

[3]唐 濤，郜春海，黃友能，等.CJ/T407-2012城市軌道交通基于通信的列車自動(dòng)控制系統(tǒng)技術(shù)要求[M].北京：中國標(biāo)準(zhǔn)出版社，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級(jí)車載ATP功能建模分析[J].鐵路計(jì)算機(jī)應(yīng)用.2017，26（5）：5-10.

[7]張曙光.CTCS-3級(jí)列控系統(tǒng)總體技術(shù)方案[M].北京：中國標(biāo)準(zhǔn)出版社，2008.

[8]丁春平.基于域+Timed RAISE的列控系統(tǒng)等級(jí)轉(zhuǎn)換場景建模與驗(yàn)證[D].蘭州：蘭州交通大學(xué)，2016.

[9]王永偉.基于構(gòu)件的形式化方法在軟件開發(fā)中的應(yīng)用研究[D].哈爾濱：哈爾濱工程大學(xué)，2010.

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