彭永成，李茂青，岳麗麗，王 陽

（1.蘭州交通大學(xué)自動(dòng)化與電氣工程學(xué)院，蘭州 730070；2.中國國家鐵路集團(tuán)有限公司鐵路安全研究中心，北京 100081）

目前，我國鐵路運(yùn)輸處于快速發(fā)展階段，列車運(yùn)行控制系統(tǒng)作為軌道交通中的關(guān)鍵技術(shù)之一，為列車的安全、高效運(yùn)行提供了保障。隨著運(yùn)營里程的增加和運(yùn)行速度的提高，我國干線鐵路列控系統(tǒng)實(shí)現(xiàn)了從CTCS-0（Chinese train control system level 0）到CTCS-3（Chinese train control system level 3）等級的國產(chǎn)化發(fā)展。然而，在城際鐵路中，列控系統(tǒng)仍存在一些問題，主要包括：1）由于軌旁設(shè)備過多，導(dǎo)致系統(tǒng)造價(jià)昂貴；2）區(qū)間和車站采用不同控制系統(tǒng)，使得設(shè)備結(jié)構(gòu)復(fù)雜，系統(tǒng)接口繁多；3）以地面為中心的控制模式使得信息流通環(huán)節(jié)較多，增加了通信延時(shí)。隨著列車定位技術(shù)和適用于軌道交通的通信技術(shù)日益成熟［1］，為實(shí)現(xiàn)線路資源的充分利用和運(yùn)營效率的進(jìn)一步提升，有必要對下一代列控系統(tǒng)進(jìn)行研究。文獻(xiàn)［2］指出：我國列控系統(tǒng)應(yīng)利用新技術(shù)簡化和優(yōu)化系統(tǒng)結(jié)構(gòu)，結(jié)合無線通信、衛(wèi)星定位和智能駕駛等技術(shù)進(jìn)一步提高鐵路運(yùn)輸效率，實(shí)現(xiàn)以車載設(shè)備為主體的列控系統(tǒng)架構(gòu)。國內(nèi)卡斯柯［3］和中車青島四方［4］等單位也在進(jìn)行下一代列車自主運(yùn)行系統(tǒng)的相關(guān)研究，主要目的是實(shí)現(xiàn)軌旁設(shè)備的精簡、系統(tǒng)功能分配的優(yōu)化、以車載為中心的自主資源管理以及列車間隔的主動(dòng)防護(hù)。文獻(xiàn)［5］介紹了新一代列控系統(tǒng)的關(guān)鍵技術(shù)：以列車為中心的資源管理、列車自主控制和精簡后的新架構(gòu)，并對其優(yōu)勢進(jìn)行了分析說明。文獻(xiàn)［6］針對新型列控系統(tǒng)提出了線路資源管理子系統(tǒng)的概念，并設(shè)計(jì)了子系統(tǒng)的模塊結(jié)構(gòu)和線路資源管理流程。文獻(xiàn)［7］提出了新型列控系統(tǒng)中鄰域協(xié)作的管理模式和方法，并針對故障場景設(shè)計(jì)了基于鄰域信息共享和控制模式切換相結(jié)合的列車群安全防護(hù)方法，以提高列車群整體對外界突發(fā)情況的應(yīng)對能力。文獻(xiàn)［8］設(shè)計(jì)了基于LTE技術(shù)的下一代CBTC數(shù)據(jù)通信系統(tǒng)，并對系統(tǒng)性能進(jìn)行了測試，將性能數(shù)據(jù)轉(zhuǎn)換為確定性隨機(jī)Petri網(wǎng)模型參數(shù)，用于評估重連接和切換場景下系統(tǒng)的可靠性。文獻(xiàn)［9］提出了適用于城際鐵路的車地協(xié)同列控系統(tǒng)，無資源競爭時(shí)由車載設(shè)備實(shí)現(xiàn)進(jìn)路功能，當(dāng)多車競爭道岔資源時(shí)由地面目標(biāo)控制器（object controller，OC）對車載或中心控制層的命令進(jìn)行沖突判別與仲裁，完成對資源的分配。該系統(tǒng)在提升列車自主化的同時(shí)，繼承了地面集中聯(lián)鎖進(jìn)路控制的整體性及復(fù)雜車況的適應(yīng)性。綜合以上文獻(xiàn)，由于新型列控系統(tǒng)處于開發(fā)試驗(yàn)階段，尚無確定的系統(tǒng)方案及相關(guān)的技術(shù)標(biāo)準(zhǔn)，現(xiàn)有文獻(xiàn)對車地協(xié)同列控系統(tǒng)追蹤運(yùn)行模塊的研究較少，故需要對車地協(xié)同進(jìn)行進(jìn)一步研究。

新型列控系統(tǒng)作為安全苛求系統(tǒng)，其設(shè)計(jì)開發(fā)需完成功能安全性的測試和驗(yàn)證。若系統(tǒng)軟件存在漏洞且產(chǎn)生不確定性行為，則有可能因影響正常運(yùn)行而造成經(jīng)濟(jì)損失，甚至造成事故。對于系統(tǒng)功能的正確性和安全性問題，除了依靠傳統(tǒng)的測試方法，在設(shè)計(jì)階段，國際標(biāo)準(zhǔn)EN 50129－2018強(qiáng)烈建議使用基于嚴(yán)密的數(shù)學(xué)理論和推理的形式化方法對系統(tǒng)進(jìn)行驗(yàn)證分析［10］。對于列控系統(tǒng)規(guī)范的建模與形式化驗(yàn)證，需要從系統(tǒng)規(guī)范到建模、驗(yàn)證之間建立完整的轉(zhuǎn)換規(guī)則，保證系統(tǒng)規(guī)范、模型以及程序代碼的高度一致性［11］，以消除自然語言可能造成的歧義。有色Petri網(wǎng)（colored Petri net，CPN）通過對系統(tǒng)結(jié)構(gòu)和狀態(tài)變化的精確描述，分析復(fù)雜系統(tǒng)運(yùn)行過程中的并發(fā)性、異步性和不確定性行為，以檢驗(yàn)系統(tǒng)狀態(tài)是否有不符合要求的異常標(biāo)識(shí)［12］。近年來，有色Petri網(wǎng)已經(jīng)成為列控系統(tǒng)建模和驗(yàn)證的一種重要理論方法。文獻(xiàn)［13］利用有色Petri網(wǎng)對無線閉塞中心（radio block center，RBC）進(jìn)行建模，研究了列車通過RBC 邊界時(shí)進(jìn)行RBC 切換的問題，并分析了影響切換的原因和提高成功概率的方法。文獻(xiàn)［14］利用有色Petri網(wǎng)對列車運(yùn)行過程中不同等級列控系統(tǒng)之間的轉(zhuǎn)換建立形式化模型，分析了列車速度和等級轉(zhuǎn)換實(shí)時(shí)性之間的關(guān)系。文獻(xiàn)［15］對鐵路平交道口控制系統(tǒng)建立了適用于定量安全分析的系統(tǒng)定時(shí)分層CPN 模型，通過探索標(biāo)準(zhǔn)的狀態(tài)空間報(bào)告來驗(yàn)證非時(shí)序CPN 模型，并基于模型仿真過程中采集的數(shù)據(jù)評估危險(xiǎn)事件平均時(shí)間的安全特性。文獻(xiàn)［16］利用有色Petri網(wǎng)理論，研究了不同的后備模式下設(shè)計(jì)間隔對列車模式切換成功率和運(yùn)行效率的影響，得到了列車模式切換的成功率和后備模式設(shè)計(jì)間隔的關(guān)系。文獻(xiàn)［17］針對基于衛(wèi)星定位的列控系統(tǒng)，在不同場景下對車載子系統(tǒng)構(gòu)建有色Petri網(wǎng)模型，并將所有場景整合成一個(gè)連貫的整體模型，采用狀態(tài)空間分析和基于模型的測試技術(shù)驗(yàn)證CPN 模型在標(biāo)準(zhǔn)和系統(tǒng)特定屬性方面的正確性和一致性。對列控系統(tǒng)的建模驗(yàn)證時(shí)，將系統(tǒng)劃分為不同的功能子模塊，以便于分析系統(tǒng)的具體功能。另外，通過接口庫所將不同場景下建立的子模型連接，構(gòu)成系統(tǒng)頂層模型，以保證驗(yàn)證分析時(shí)模型與系統(tǒng)設(shè)計(jì)的一致性。

本文基于文獻(xiàn)［6］中適用于城際鐵路的車地協(xié)同列控系統(tǒng)，進(jìn)一步研究其追蹤運(yùn)行模塊的實(shí)現(xiàn)。首先，基于車地協(xié)同系統(tǒng)的架構(gòu)和特點(diǎn)，對列車追蹤運(yùn)行的功能實(shí)現(xiàn)做合理設(shè)計(jì)，其移動(dòng)授權(quán)計(jì)算由車載設(shè)備實(shí)現(xiàn)，從而優(yōu)化功能分配，提高列車自主化程度；其次，采用分層有色Petri網(wǎng)（hierarchical coloured Petri net，HCPN）對移動(dòng)授權(quán)生成和安全防護(hù)功能的具體實(shí)現(xiàn)過程建立層次化模型，描述系統(tǒng)運(yùn)行中的信息交互和狀態(tài)變化；最后，基于具體的數(shù)據(jù)，利用模型檢驗(yàn)方法對模型狀態(tài)空間及節(jié)點(diǎn)狀態(tài)進(jìn)行分析，為列控系統(tǒng)的具體開發(fā)提供理論支撐。

1 車地協(xié)同系統(tǒng)追蹤運(yùn)行模塊功能實(shí)現(xiàn)

1.1 車地協(xié)同列控系統(tǒng)整體結(jié)構(gòu)

車地協(xié)同列控系統(tǒng)的結(jié)構(gòu)分為地面站內(nèi)設(shè)備、車載設(shè)備和地面軌旁設(shè)備3個(gè)部分，通過通信網(wǎng)絡(luò)實(shí)現(xiàn)信息交互。各部分子模塊之間傳遞的信息如圖1所示。

圖1 列控系統(tǒng)子模塊間傳遞的信息Fig.1 Information transmitted between sub-modules of the train control system

地面中心的調(diào)度集中系統(tǒng)（centralized traffic control，CTC）承擔(dān)與調(diào)度運(yùn)營相關(guān)的業(yè)務(wù)，行調(diào)人員通過CTC系統(tǒng)將行車計(jì)劃和臨時(shí)限速命令下發(fā)到列控系統(tǒng)。在車站內(nèi)設(shè)置地面列車管理單元（train management unit_center，TMU_C），接收CTC發(fā)送的信息，并將其作為管轄范圍內(nèi)列車運(yùn)行和進(jìn)行作業(yè)的依據(jù)。TMU_C將收到的運(yùn)行計(jì)劃和臨時(shí)限速命令進(jìn)行解析，發(fā)送給對應(yīng)列車的車載設(shè)備；同時(shí)，TMU_C會(huì)收集管轄范圍內(nèi)列車的實(shí)時(shí)運(yùn)行狀態(tài)，并轉(zhuǎn)發(fā)到該范圍內(nèi)列車車載設(shè)備。此外，在TMU_C中設(shè)置電子地圖數(shù)據(jù)庫，描述最新線路固定信息，包括用于輔助定位和進(jìn)路觸發(fā)等功能的虛擬應(yīng)答器、線路資源類型和線路固定限速等信息。當(dāng)有列車進(jìn)入TMU_C管轄范圍時(shí)，會(huì)通過TMU_C對車載電子地圖版本進(jìn)行校核和更新。

地面軌旁設(shè)備取消了信號機(jī)、軌道電路，站內(nèi)增設(shè)目標(biāo)控制器（OC）與線路道岔資源一一對應(yīng)，用于實(shí)現(xiàn)對道岔的征用以及對車載或中心控制層的命令進(jìn)行沖突判別與仲裁。

車載設(shè)備主要包括追蹤運(yùn)行模塊、聯(lián)鎖模塊、車載列車管理單元（train management unit_vehicle，TMU_V）和其他輔助模塊。聯(lián)鎖模塊實(shí)現(xiàn)列車進(jìn)路控制，向OC申請占用道岔資源，從而完成進(jìn)路的建立和解鎖等功能。追蹤運(yùn)行模塊由車載移動(dòng)授權(quán)計(jì)算單元（movement authority unit，MAU）、超速防護(hù)模塊（automatic train protection，ATP）和自動(dòng)駕駛子系統(tǒng)（automatic train operation，ATO）構(gòu)成。追蹤運(yùn)行模塊實(shí)現(xiàn)列車的運(yùn)行控制，保證列車在允許的范圍內(nèi)以合理速度運(yùn)行，且在追蹤運(yùn)行時(shí)主動(dòng)和前車保持間隔。

車地協(xié)同列控系統(tǒng)改變了現(xiàn)有列控系統(tǒng)以地面中心設(shè)備為主體的系統(tǒng)架構(gòu)，由車載和地面設(shè)備協(xié)同完成列車進(jìn)路管理和追蹤運(yùn)行控制功能，這有利于實(shí)現(xiàn)多車對道岔搶占與共享場景下的聯(lián)鎖功能，避免列車間的進(jìn)路沖突。

1.2 追蹤運(yùn)行模塊功能實(shí)現(xiàn)

追蹤運(yùn)行模塊的功能可劃分為移動(dòng)授權(quán)生成、超速防護(hù)和自動(dòng)駕駛。追蹤運(yùn)行模塊從其他模塊獲得的信息包括：

1）從電子地圖模塊獲取線路靜態(tài)數(shù)據(jù)；

2）與車載列車管理單元（TMU_V）實(shí)現(xiàn)信息交互，獲取相鄰列車實(shí)時(shí)位置和其他靜態(tài)障礙物（如站臺(tái)門、緊急停車按鈕等）信息；

3）與車載聯(lián)鎖模塊通信，實(shí)現(xiàn)對進(jìn)路信息的實(shí)時(shí)更新，并將其作為車載設(shè)備計(jì)算進(jìn)路移動(dòng)授權(quán)（movement authority，MA）的條件。

1.2.1 移動(dòng)授權(quán)計(jì)算單元功能實(shí)現(xiàn)

車地協(xié)同列控系統(tǒng)中，移動(dòng)授權(quán)的生成由追蹤運(yùn)行模塊中的車載移動(dòng)授權(quán)計(jì)算單元（MAU）實(shí)現(xiàn)。MAU 根據(jù)來自前方相鄰列車和地面設(shè)備的線路障礙物信息，確定列車運(yùn)行前方最近的障礙物，并將其設(shè)為移動(dòng)授權(quán)終點(diǎn)（end of authority，EOA）。從本車車尾到該EOA 范圍內(nèi)線路，按照允許的運(yùn)行方向被授予列車使用，作為控制列車運(yùn)行的依據(jù)。

車載移動(dòng)授權(quán)計(jì)算單元在自主計(jì)算移動(dòng)授權(quán)時(shí)，與其他子模塊的信息交互如圖2所示。中心設(shè)備獲取管轄范圍內(nèi)各列車信息，并轉(zhuǎn)發(fā)給車載TMU_V。車載聯(lián)鎖子系統(tǒng)收到行車計(jì)劃后，請求線路資源并向OC 發(fā)送操作命令。MAU 模塊周期性地更新運(yùn)行前方線路的靜態(tài)障礙物信息、前方列車信息和由聯(lián)鎖子系統(tǒng)處理生成的進(jìn)路信息，并結(jié)合電子地圖自主判斷最近障礙物及其類型，得到移動(dòng)授權(quán)終點(diǎn)。MA 計(jì)算完成后，MAU 模塊將該信息輸出至超速防護(hù)模塊。

圖2 MA計(jì)算階段各模塊信息交互圖Fig.2 Information interaction in the MA calculation phase

MA 計(jì)算流程如圖3所示。列車運(yùn)行時(shí)，車載自主定位單元實(shí)時(shí)獲取列車所在位置，根據(jù)運(yùn)行情況和自身參數(shù)信息，計(jì)算考慮了安全包絡(luò)的位置信息。若路徑探詢范圍內(nèi)有前車，則需根據(jù)前車的位置、速度、測距誤差、通信延時(shí)等信息計(jì)算出前車可能存在的位置，并在計(jì)算時(shí)考慮列車移動(dòng)距離，從而對列車追蹤間隔進(jìn)行優(yōu)化。

圖3 MA計(jì)算流程圖Fig.3 Flow chart of calculation for MA

在MA 計(jì)算階段，首先，MAU 依據(jù)TMU_V轉(zhuǎn)發(fā)的線路靜態(tài)障礙物信息，判斷運(yùn)行前方是否探詢到無權(quán)限的線路資源，包括由設(shè)備故障或者特殊情況導(dǎo)致的狀態(tài)異常資源。然后，MAU 根據(jù)電子地圖確定列車是否處于進(jìn)路觸發(fā)位置，再進(jìn)一步判斷前方是否有進(jìn)路或者列車，從而確定列車所處的場景是追蹤前車運(yùn)行還是觸發(fā)進(jìn)路，以及是否處于線路端點(diǎn)或者折返點(diǎn)。在此過程中，對于EOA 的計(jì)算與當(dāng)前所處的場景相關(guān)，通過獲取到的障礙物信息確定其類型及具體位置。若得到的EOA 要求列車立即停車或到此EOA 的距離不滿足安全制動(dòng)距離，則需根據(jù)場景判斷是否向車載發(fā)送緊急制動(dòng)信息；若該EOA 無需輸出緊急制動(dòng)，則確定MA 的范圍。MA 起點(diǎn)為本列車安全車尾，從該位置開始到EOA，遍歷線路區(qū)段、道岔等線路資源狀態(tài)，串接可用線路資源，從而實(shí)現(xiàn)MA 的延伸。在授權(quán)終點(diǎn)前預(yù)留一定的安全距離，以確保列車在靜態(tài)障礙物前安全停車，或在對前方列車追蹤運(yùn)行過程中與前車保持安全間隔。根據(jù)判斷出的不同場景，對于MA 范圍內(nèi)的線路資源做不同的處理。最后，根據(jù)電子地圖，在已確定的MA 線路中加入固定限速值。在計(jì)算MA 時(shí)，由列車當(dāng)前的運(yùn)行情況決定需要向前探詢的范圍，以減少對線路資源的不必要占用，從而實(shí)現(xiàn)對地面線路資源的優(yōu)化利用［18］。

1.2.2 超速防護(hù)模塊功能實(shí)現(xiàn)

超速防護(hù)模塊（ATP）中的信息處理流程如圖4所示。其功能主要由以下3個(gè)階段實(shí)現(xiàn)：

圖4 超速防護(hù)模塊信息處理Fig.4 Information processing of overspeed protection

1）ATP在獲取由MAU 自主計(jì)算生成的移動(dòng)授權(quán)后，與TMU_V 通信，檢查是否收到CTC 下達(dá)的臨時(shí)限速命令，若已下達(dá)則需添加該命令。

2）更新當(dāng)前位置信息，根據(jù)列車最大制動(dòng)距離生成速度監(jiān)控曲線，發(fā)送給自動(dòng)駕駛子系統(tǒng)（ATO），由ATO 完成對速度監(jiān)控曲線的跟蹤。

3）在列車運(yùn)行過程中，ATP 根據(jù)列車當(dāng)前的位置和實(shí)時(shí)速度信息，與速度監(jiān)控曲線進(jìn)行比較，判斷是否達(dá)到制動(dòng)條件，若觸發(fā)制動(dòng)，則立刻輸出相應(yīng)等級的制動(dòng)命令。ATP嚴(yán)格監(jiān)控列車的速度，根據(jù)需要生成警告信息，確保列車不越過移動(dòng)授權(quán)終點(diǎn)。若當(dāng)前時(shí)刻已輸出緊急制動(dòng)，則在列車停車之前持續(xù)輸出緊急制動(dòng)命令。

2 追蹤運(yùn)行模塊建模

有色Petri網(wǎng)對大型復(fù)雜系統(tǒng)的并發(fā)性、異步性的精確描述和直觀的圖形表達(dá)能力，常被應(yīng)用于鐵路信號軟件的形式化建模與驗(yàn)證中。在CPN 中，用庫所（place）表示一個(gè)或多個(gè)狀態(tài)量，用變遷（transition）描述狀態(tài)量的變化，模擬系統(tǒng)行為，用有向弧（arc）連接庫所和變遷，弧上的函數(shù)描述狀態(tài)的變化。通過標(biāo)準(zhǔn)元語言（standard meta language，SML）實(shí)現(xiàn)模型中函數(shù)的編譯。SML語言常被用于編譯器、編程語言研究以及自動(dòng)定理的證明研究。在CPN 模型中，SML 語言能夠自動(dòng)地指定多數(shù)表達(dá)式的類型，不要求顯式的類型標(biāo)注，而且能夠確保類型安全，有良好類型的SML 程序已被證明不會(huì)導(dǎo)致運(yùn)行時(shí)間類型的錯(cuò)誤［19］。

2.1 追蹤運(yùn)行模塊頂層模型

本文采用自上而下的建模思路建立分層CPN模型，以降低模型的復(fù)雜度。將功能實(shí)現(xiàn)過程進(jìn)行劃分，不同功能由替代變遷代表的不同子模塊完成。對于鄰車和其他功能作簡化抽象處理，主要對追蹤運(yùn)行功能建立精細(xì)化模型并對此功能的實(shí)現(xiàn)和安全性進(jìn)行驗(yàn)證。

在CPN模型中，用顏色集表示數(shù)據(jù)類型，部分顏色集定義如圖5所示，其中：TRAINID顏色集表示列車號，DIR顏色集表示列車的運(yùn)行方向，LINEPOS表示線路位置。由標(biāo)準(zhǔn)顏色集可以構(gòu)造出其他類型顏色集，TRINF是一個(gè)乘積類型（product）顏色集，由列車號、車頭位置、車尾位置以及運(yùn)行方向復(fù)合而來，表示列車位置信息。為便于描述，將線路的屬性分為站內(nèi)無岔、站內(nèi)有岔、區(qū)間和盡頭型，用顏色集MAPINF描述電子地圖中線路信息。SWITCH 顏色集表示道岔信息，包括道岔編號、道岔位置以及經(jīng)過該道岔時(shí)的限速。ROUTEINF表示經(jīng)聯(lián)鎖子系統(tǒng)處理的可用進(jìn)路信息，用來確定列車的初始位置、進(jìn)路的始終端位置及進(jìn)路內(nèi)道岔的開通位置。移動(dòng)授權(quán)計(jì)算完成后，其范圍內(nèi)每個(gè)虛擬區(qū)段的信息由顏色集合MASEC表示，最終以列表顏色集LISTMASEC類型輸出。在超速防護(hù)子模型中，顏色集SMTYPE表示區(qū)段所處的監(jiān)控區(qū)類型，SMSEC為被監(jiān)控區(qū)段的信息，LISTSMSEC為SMSEC的列表形式。

圖5 顏色集聲明Fig.5 Declaration of color set

追蹤運(yùn)行模塊頂層模型中設(shè)置5個(gè)代替變遷，分別完成追蹤運(yùn)行模塊的不同功能，如圖6所示。代替變遷Safe_position_process1 和Safe_position_process2對應(yīng)于安全位置處理子模型，分別完成本車和鄰車的安全位置計(jì)算，其結(jié)果由庫所Train_safe_position和Nei_train_safe_position表示。代替變遷MAU_process對應(yīng)于移動(dòng)授權(quán)計(jì)算子模型，判斷列車當(dāng)前的場景并計(jì)算得到MA，然后輸出到庫所MA_list。代替變遷ATP_process和ATO_process分別對超速防護(hù)子模塊和自動(dòng)駕駛子模塊建模。ATP_process子模型接收臨時(shí)限速信息TSR_inf和列車當(dāng)前動(dòng)態(tài)信息Train_dyn_inf，輸出制動(dòng)命令到庫所Brake_output；Monitoring_speed是一個(gè)接口庫所，通過此庫所可將ATP_process子模型生成的速度監(jiān)控曲線傳遞給ATO_process子模型。

圖6 追蹤運(yùn)行模塊頂層模型Fig.6 Top model of the tracking operation module

2.2 MAU 模塊模型

移動(dòng)授權(quán)模塊模型如圖7所示。初始狀態(tài)時(shí)，由進(jìn)路信息Routeinf、鄰車位置信息Nei_train_safe_position和無權(quán)限的線路資源Nonprivileged_resource觸發(fā)代替變遷EOA_process。在EOA_process對應(yīng)的子模型中，通過查詢電子地圖Map_e確定運(yùn)行前方的唯一列車，從而對比障礙物位置得到當(dāng)前EOA 信息。此外，為防止將非安全位置作為后一階段計(jì)算條件，非安全列車位置Train_positoin和Nei_train_position的狀態(tài)被設(shè)置為EOA_process觸發(fā)的限制條件，若未得到安全位置，則不能開始EOA 計(jì)算。最后，根據(jù)不同的列車運(yùn)行場景，結(jié)合EOA 類型選擇不同的算法，分別由代替變遷MA-r_process和MA-o_process表示授權(quán)終點(diǎn)為進(jìn)路終端和障礙物類型時(shí)的MA 計(jì)算。

圖7 MAU 模塊（MAU_process）模型Fig.7 Model of the MAU module（MAU_process）

當(dāng)EOA 被判斷為唯一前車時(shí)，建立的子模型如圖8所示。該模型描述此場景下MA 計(jì)算的具體實(shí)現(xiàn)過程。根據(jù)CPN 消息驅(qū)動(dòng)機(jī)制，若在庫所Fro_train_safe_position上有托肯，則表示已經(jīng)確定前方唯一列車為MA 終點(diǎn)障礙物；若庫所Safe_position上有托肯，則表明前一階段已計(jì)算出本車安全位置。

圖8 EOA為前車尾部時(shí)的MA計(jì)算（MA_obstacle process）子模型Fig.8 Sub-model of the calculation for MA in the scene when EOA is the rear of front train

在此場景下，首先，確定MA 起點(diǎn)和終點(diǎn)位置，庫所MA_startpoint表示MA 起點(diǎn)為本列車安全位置的尾部，庫所MA_endpoint表示MA 終點(diǎn)為前車尾部安全位置；由于此模型中已判定該范圍內(nèi)線路資源空閑且可用，故可確定MA 范圍內(nèi)的線路區(qū)段。之后，變遷MA_end_generate和MA_start_generate結(jié)合庫所Map_e中的電子地圖信息，通過周圍有向弧上的函數(shù)，將滿足條件的線路資源進(jìn)行串接，同時(shí)確定線路固定限速。最后，庫所MA_sec_list將MA線路以列表形式輸出，由端口庫所MA_to_frt_train表示EOA被判定為前車尾部時(shí)的移動(dòng)授權(quán)。

2.3 超速防護(hù)模塊模型

超速防護(hù)模塊模型如圖9所示。初始狀態(tài)時(shí)，庫所MA_list表示經(jīng)移動(dòng)授權(quán)模塊計(jì)算得到的MA信息。該模型主要分為3個(gè)部分：第1部分，由代替變遷TSR_process將臨時(shí)限速命令TSR_inf添加到MA 范圍內(nèi)的區(qū)段信息中；第2 部分，由代替變遷Monitoring_speed_process根據(jù)列車本身參數(shù)得到控車曲線，并通過接口庫所Monitoring_speed和Monitoring_speed_for_ATO 輸出；第3部分，由代替變遷Dyn_protection 根據(jù)列車當(dāng)前位置和動(dòng)態(tài)信息（速度、加速度、制動(dòng)情況）監(jiān)控列車實(shí)時(shí)運(yùn)行。以上3個(gè)代替變遷對應(yīng)的子模型完成各自具體功能，最終實(shí)現(xiàn)列車運(yùn)行時(shí)對速度的安全防護(hù)。

圖9 超速防護(hù)模塊（ATP_process）模型Fig.9 Model of the overspeed protection module

速度實(shí)時(shí)監(jiān)控子模型（Dyn_protection模型）如圖10所示。變遷Monitoring_speed輸入速度監(jiān)控曲線信息，同時(shí)產(chǎn)生托肯給庫所Trigger1 和Trigger2，用于提供其他變遷的觸發(fā)條件。更新列車位置信息后，變遷TSM_process和CSM_process通過守衛(wèi)函數(shù)，分別完成在不同監(jiān)控區(qū)對列車限速信息的處理。在列車動(dòng)態(tài)信息輸入階段，由變遷EB_judge判斷列車當(dāng)前制動(dòng)等級，若此時(shí)已輸出緊急制動(dòng)命令，則繼續(xù)輸出緊急制動(dòng)；若未輸出，則由變遷Braketype_judge1 和Braketype_judge2 及周圍弧函數(shù)根據(jù)列車位置和當(dāng)前速度輸出對應(yīng)等級的制動(dòng)。最終的制動(dòng)命令輸出至端口庫所Brake_output，表示超速防護(hù)模塊與列車制動(dòng)單元的接口。

圖10 速度實(shí)時(shí)監(jiān)控子模型Fig.10 Sub-model of the speed monitoring module

3 追蹤運(yùn)行模塊功能驗(yàn)證

考慮多車在區(qū)間追蹤運(yùn)行的場景，通過建立的模型對追蹤運(yùn)行模塊功能進(jìn)行驗(yàn)證。設(shè)區(qū)間內(nèi)有3輛列車追蹤運(yùn)行，前方列車分別為Train（1）和Train（2），本列車為Train（3）。改變輸入庫所的托肯值，以設(shè)置模型的初始狀態(tài)。庫所Train_positoin的托肯值設(shè)置為（Train（3），（19，2 800），（19，3 000），down），表示本車實(shí)時(shí)位置和運(yùn)行方向；庫所Nei_train_position的托肯值設(shè)置為1｀（Train（2），（21，6 000），（21，6 200），down）＋＋，1｀（Train（1），（23，7 900），（23，8 100），down），表示前方2輛列車位置信息；庫所Nonprivileged_resource 的托肯值設(shè)置為（switch，（27，11 600），（27，11 700）），表示前方無權(quán)限資源的類型及位置；庫所TRAIN_dyn_inf的托肯值設(shè)為（Train（3），260，nb，down），表示列車速度為260 km／h，未處于加速或制動(dòng)階段。將本場景下建立的模型逐步執(zhí)行，可觀測到模型的狀態(tài)變化，利用模型分析工具可生成狀態(tài)空間報(bào)告［20］。

3.1 移動(dòng)授權(quán)生成功能驗(yàn)證

移動(dòng)授權(quán)模型標(biāo)準(zhǔn)狀態(tài)空間統(tǒng)計(jì)數(shù)據(jù)中，狀態(tài)空間的可達(dá)狀態(tài)節(jié)點(diǎn)數(shù)量為264個(gè)，托肯綁定弧的數(shù)量為533個(gè)，統(tǒng)計(jì)狀態(tài)為完全；強(qiáng)連接組件圖中，可達(dá)節(jié)點(diǎn)數(shù)量為264個(gè)，托肯綁定弧的數(shù)量為533個(gè)。

移動(dòng)授權(quán)模型狀態(tài)空間統(tǒng)計(jì)結(jié)果狀態(tài)為完全，表明計(jì)算出的狀態(tài)空間是完整的，模型的所有可達(dá)狀態(tài)節(jié)點(diǎn)已被納入統(tǒng)計(jì)，可達(dá)狀態(tài)節(jié)點(diǎn)和托肯綁定弧的數(shù)量均為有限值，終節(jié)點(diǎn)標(biāo)號為264。由于強(qiáng)連接組件圖與狀態(tài)空間中的狀態(tài)節(jié)點(diǎn)數(shù)量和托肯綁定弧數(shù)量相同，故模型中不存在活鎖。由圖11中的模型家態(tài)性（Home Properties）和活性（Liveness Properties）報(bào)告可知：在此場景下，模型的家態(tài)節(jié)點(diǎn)（Home Markings）和唯一死節(jié)點(diǎn)（Dead Markings）的標(biāo)號都為264，與終節(jié)點(diǎn)標(biāo)號一致，表明系統(tǒng)總是可以到達(dá)最終節(jié)點(diǎn)；模型存在死變遷（Dead Transition Instances），由報(bào)告可知為移動(dòng)授權(quán)模塊收到多個(gè)靜態(tài)障礙物信息或進(jìn)路信息時(shí)對于障礙物的處理變遷，由于所選場景中靜態(tài)障礙物是唯一的且沒有進(jìn)路信息，故該變遷不會(huì)觸發(fā)，系統(tǒng)的活性滿足場景要求；由模型公平性（Fairness Properties）報(bào)告中“No infinite occurrence sequences”可知，模型不存在無限發(fā)生的序列，不會(huì)循環(huán)執(zhí)行，滿足公平性要求［21］。

圖11 移動(dòng)授權(quán)模型狀態(tài)空間報(bào)告Fig.11 State space report of the MAU model

對移動(dòng)授權(quán)模型可達(dá)節(jié)點(diǎn)的狀態(tài)及對應(yīng)庫所的具體托肯進(jìn)行檢查可知：無異常節(jié)點(diǎn)，模型功能安全性滿足設(shè)計(jì)需求。由狀態(tài)空間統(tǒng)計(jì)結(jié)果可知：統(tǒng)計(jì)模型終節(jié)點(diǎn)標(biāo)號為264，頂層模型在該節(jié)點(diǎn)處庫所的具體托肯值如圖12所示。由圖12可知：庫所MA_list的托肯值為1｀［（Train（3），（19，2 780），（19，4 600），section，180），（Train（3），（21，4 600），（21，5 920），section，200）］，表示模型最終狀態(tài)已計(jì)算出該場景下從本車到唯一前車的移動(dòng)授權(quán)。

圖12 移動(dòng)授權(quán)模型終節(jié)點(diǎn)托肯值Fig.12 Token of the ultimate node in MAU model

由模型初始狀態(tài)中列車當(dāng)前位置和前方障礙物信息，可確定本車Train（3）在區(qū)間對前方列車進(jìn)行追蹤運(yùn)行，且前車Train（2）被確定為前方唯一障礙物。從本車安全車尾位置到前車車尾的線路資源應(yīng)為（19，2 780）、（21，4 600）、（21，5 920），與圖12模型終節(jié)點(diǎn)中移動(dòng)授權(quán)的線路資源一致。該線路區(qū)段的限速值分別為180、200 km／h，與電子地圖中限速一致。

3.2 超速防護(hù)功能驗(yàn)證

超速防護(hù)模型標(biāo)準(zhǔn)狀態(tài)空間統(tǒng)計(jì)數(shù)據(jù)中，狀態(tài)空間的可達(dá)狀態(tài)節(jié)點(diǎn)數(shù)量為237個(gè)，托肯綁定弧的數(shù)量為386個(gè)，統(tǒng)計(jì)狀態(tài)為完全；強(qiáng)連接組件圖中，可達(dá)節(jié)點(diǎn)數(shù)量為237個(gè)，托肯綁定弧的數(shù)量為386個(gè)。

超速防護(hù)模型狀態(tài)空間統(tǒng)計(jì)結(jié)果狀態(tài)為完全，表明計(jì)算出的狀態(tài)空間是完整的，模型的所有可達(dá)狀態(tài)節(jié)點(diǎn)已被納入統(tǒng)計(jì)，可達(dá)狀態(tài)節(jié)點(diǎn)和托肯綁定弧的數(shù)量均為有限值，終節(jié)點(diǎn)標(biāo)號為237。由于強(qiáng)連接組件圖與狀態(tài)空間中的狀態(tài)節(jié)點(diǎn)數(shù)量和托肯綁定弧數(shù)量相同，故模型中不存在活鎖。家態(tài)性（Home Properties）和活性（Liveness Properties）報(bào)告見圖13。模型的家態(tài)節(jié)點(diǎn)（Home Markings）和唯一死節(jié)點(diǎn)（Dead Markings）為同一節(jié)點(diǎn)，且標(biāo)號與終節(jié)點(diǎn)一致，表明系統(tǒng)總是可以到達(dá)最終節(jié)點(diǎn)。模型的死變遷（Dead Transition Instances）為EB_judge。由于初始狀態(tài)下未輸出緊急制動(dòng)，故此場景下不會(huì)觸發(fā)該變遷，系統(tǒng)活性滿足要求。由模型公平性（Fairness Properties）報(bào)告中“No infinite occurrence sequences”可知：模型不存在無限發(fā)生序列，不會(huì)循環(huán)執(zhí)行。

圖13 超速防護(hù)模型狀態(tài)空間報(bào)告Fig.13 State space report of the overspeed protection module

對超速防護(hù)模型可達(dá)節(jié)點(diǎn)的狀態(tài)及對應(yīng)庫所的具體托肯進(jìn)行檢查可知：無異常節(jié)點(diǎn)，模型功能安全性滿足設(shè)計(jì)需求。模型的終節(jié)點(diǎn)中具體托肯值如圖14 所示。庫所Monitoring_speed的托肯值為1｀［（（2 780，4 600，19，180），tsm），（（4 600，4 800，21，200），tsm），（（4 800，5 800，21，180），tsm），（（5 800，5 920，21，200），tsm）］，以列表數(shù)據(jù)形式表示超速防護(hù)模塊生成的監(jiān)控速度。庫所Brake_output的托肯值為1｀eb，表示成功輸出緊急制動(dòng)命令。

圖14 超速防護(hù)模型終節(jié)點(diǎn)狀態(tài)托肯值Fig.14 Token of the ultimate node in overspeed protection module

由于列車位置在初始狀態(tài)時(shí)設(shè)置為［（19，2 800），（19，3 000）］，考慮列車安全包絡(luò)后到前方障礙物的距離為2 600 m，當(dāng)列車以0.8 m／s2為最大減速度進(jìn)行制動(dòng)情況下，在該位置可以安全停車的最大運(yùn)行速度為246 km／h，而當(dāng)前列車實(shí)時(shí)速度設(shè)置為260 km／h，故需輸出緊急制動(dòng)，與模型輸出制動(dòng)等級一致，滿足系統(tǒng)功能安全性需求。

4 結(jié)論

1）車地協(xié)同列控系統(tǒng)可解決城際鐵路傳統(tǒng)列控系統(tǒng)軌旁設(shè)備過多、結(jié)構(gòu)復(fù)雜和信息流通環(huán)節(jié)多的問題。對車地協(xié)同系統(tǒng)中追蹤運(yùn)行模塊的功能實(shí)現(xiàn)進(jìn)行設(shè)計(jì)，將移動(dòng)授權(quán)計(jì)算轉(zhuǎn)移至車載設(shè)備，從而達(dá)到優(yōu)化功能分配、提高列車自主化程度的目的。

2）為驗(yàn)證系統(tǒng)功能的正確性及安全性，將追蹤運(yùn)行模塊功能進(jìn)行了劃分，并采用有色Petri網(wǎng)建立層次化模型，用以描述移動(dòng)授權(quán)生成和超速防護(hù)功能的具體實(shí)現(xiàn)及信息交互。

3）利用建立的模型對追蹤運(yùn)行模塊功能進(jìn)行了驗(yàn)證，結(jié)果表明模型完成了預(yù)期功能；利用狀態(tài)空間報(bào)告驗(yàn)證了模型行為屬性的正確性，通過模型節(jié)點(diǎn)的狀態(tài)驗(yàn)證了模塊功能的安全性，為系統(tǒng)的設(shè)計(jì)和開發(fā)提供了理論參考。