CTCS-3級(jí)列控車(chē)載設(shè)備的形式化建模與驗(yàn)證

何濤 韓敬佳

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

收稿日期：2020-06-09

基金項(xiàng)目：國(guó)家自然科學(xué)基金資助項(xiàng)目（U2268206）。

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

作者簡(jiǎn)介：何濤（1977—），男，教授，碩導(dǎo)，主要從事軌道交通測(cè)試研究方向研究。

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

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

關(guān)鍵詞：列控系統(tǒng)；車(chē)載設(shè)備；模式轉(zhuǎn)換；有色Petri網(wǎng)

中圖分類(lèi)號(hào)：TP391；U284 ?????????文獻(xiàn)標(biāo)志碼：A ?????文章編號(hào)：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

近年來(lái)，中國(guó)對(duì)于時(shí)速超過(guò)250 km/h的鐵路采用的是CTCS-3級(jí)列車(chē)運(yùn)行控制系統(tǒng)（以下簡(jiǎn)稱(chēng)C3級(jí)列控系統(tǒng)）^[1]，車(chē)載設(shè)備是C3級(jí)列控系統(tǒng)的重要組成部分，其安全性、可靠性直接影響列車(chē)運(yùn)行安全。因此對(duì)列控車(chē)載設(shè)備進(jìn)行建模，驗(yàn)證車(chē)載設(shè)備系統(tǒng)功能及轉(zhuǎn)換流程滿(mǎn)足相關(guān)系統(tǒng)需求規(guī)范，對(duì)保證列車(chē)運(yùn)行安全，改進(jìn)系統(tǒng)需求規(guī)范具有重要意義。

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

1車(chē)載設(shè)備功能需求分析

CTCS-3級(jí)列控系統(tǒng)的主要功能有保障行車(chē)安全、保證運(yùn)輸效率、保證乘客舒適度等^[6]。C3級(jí)列控系統(tǒng)主要由2部分組成：一部分是提供監(jiān)控列車(chē)所需要的線(xiàn)路允許速度、行車(chē)許可等基礎(chǔ)數(shù)據(jù)的地面設(shè)備；另一部分是根據(jù)相關(guān)設(shè)備傳送上來(lái)的地面信息監(jiān)控列車(chē)運(yùn)行速度、運(yùn)行條件的車(chē)載設(shè)備。

C3級(jí)列控車(chē)載設(shè)備是C3級(jí)列控系統(tǒng)的核心設(shè)備，采用故障-安全設(shè)計(jì)，車(chē)載設(shè)備主要構(gòu)成有：主控單元車(chē)載安全計(jì)算機(jī)（VC）、?GSM-R無(wú)線(xiàn)通信、軌道電路信息讀取器（STM）、應(yīng)答器信息接收單元（BTM）、列車(chē)接口單元（TIU）、人機(jī)界面（DMI）、等^[7]。C3級(jí)列控車(chē)載設(shè)備構(gòu)成如圖1所示，其主要功能包括：

1）?向RBC發(fā)送列車(chē)運(yùn)行所需動(dòng)態(tài)信息，處理來(lái)自車(chē)載的調(diào)車(chē)請(qǐng)求。

2）?處理來(lái)自RBC的緊急停車(chē)消息，根據(jù)情況對(duì)列車(chē)實(shí)行控制命令。

3）?接收無(wú)線(xiàn)閉塞中心RBC發(fā)送來(lái)的正常行車(chē)許可MA、列車(chē)位置報(bào)告等。

4）?根據(jù)接收到的應(yīng)答器信息，計(jì)算行車(chē)曲線(xiàn)及列車(chē)位置校正。

5）?接收軌道電路傳送的線(xiàn)路參數(shù)信息。

6）?實(shí)時(shí)測(cè)量列車(chē)運(yùn)行速度和行走距離并計(jì)算目標(biāo)距離模式控制曲線(xiàn)。

7）?RBC/RBC的交接。

8）?DMI的管理、司法數(shù)據(jù)的記錄功能。

車(chē)載安全計(jì)算機(jī)VC是C3級(jí)列控車(chē)載系統(tǒng)的控制核心，主要完成車(chē)載設(shè)備工作模式的判斷及轉(zhuǎn)換，根據(jù)從其他模塊獲取的信息，必要時(shí)對(duì)列車(chē)實(shí)施制動(dòng)，以保證車(chē)載系統(tǒng)對(duì)列車(chē)安全防護(hù)功能的具體實(shí)現(xiàn)和操作。因此，選用車(chē)載安全計(jì)算機(jī)中工作模式轉(zhuǎn)換作為車(chē)載設(shè)備安全計(jì)算機(jī)的主要狀態(tài)。

2CPN模型的構(gòu)建

2.1建模研究思路

根據(jù)有色Petri網(wǎng)建模語(yǔ)言的建模流程，將對(duì)車(chē)載設(shè)備的建模思想總體分為3部分：一是系統(tǒng)功能分析，根據(jù)系統(tǒng)規(guī)范了解車(chē)載設(shè)備間信息交互和車(chē)載設(shè)備中工作模式轉(zhuǎn)換條件；二是根據(jù)系統(tǒng)功能構(gòu)建CPN模型；三是根據(jù)系統(tǒng)屬性對(duì)構(gòu)建的模型進(jìn)行驗(yàn)證。CTCS-3級(jí)列控車(chē)載設(shè)備形式化建模與驗(yàn)證的總體框架圖如圖2所示。

具體建模流程如下：

1）?根據(jù)《CTCS-3級(jí)列控系統(tǒng)需求規(guī)范（SRS）》^[8]中的要求，采用有色Petri網(wǎng)對(duì)CTCS-3級(jí)列控系統(tǒng)車(chē)載設(shè)備各部分之間的信息交互以及車(chē)載安全計(jì)算機(jī)中工作模式轉(zhuǎn)換進(jìn)行建模。

2）?基于有色Petri網(wǎng)構(gòu)建出車(chē)載設(shè)備以及模式轉(zhuǎn)換的CPN模型，其中對(duì)系統(tǒng)模型采用分層（2層）的構(gòu)建規(guī)則，根據(jù)系統(tǒng)需求規(guī)范中的模式轉(zhuǎn)換條件，將車(chē)載安全計(jì)算機(jī)設(shè)為替代變遷，它的子頁(yè)模型為各模式之間的轉(zhuǎn)換。

3）?在CPN Tools工具中引入分支時(shí)序邏輯ASK-CTL公式對(duì)構(gòu)建的CPN模型進(jìn)行形式化驗(yàn)證，分析模型是否滿(mǎn)足《CTCS-3級(jí)列控系統(tǒng)需求規(guī)范（SRS）》要求的車(chē)載設(shè)備信息交互功能以及模型是否符合車(chē)載設(shè)備模式轉(zhuǎn)換流程，若不滿(mǎn)足，則重新采用有色Petri網(wǎng)對(duì)車(chē)載設(shè)備進(jìn)行建模。

4）?在模型驗(yàn)證結(jié)果正確的基礎(chǔ)上，分析系統(tǒng)的屬性是否滿(mǎn)足車(chē)載設(shè)備信息交互功能以及是否符合模式轉(zhuǎn)換流程。

2.2有色Petri網(wǎng)建模方法

有色Petri網(wǎng)是一種形式化的建模語(yǔ)言，與其他建模語(yǔ)言相比有色Petri網(wǎng)構(gòu)建的CPN模型更加直觀(guān)形象，還能對(duì)復(fù)雜系統(tǒng)進(jìn)行分層建模來(lái)描述系統(tǒng)的功能和行為，大大簡(jiǎn)化系統(tǒng)模型的復(fù)雜度。CPN作為一種圖形化的表達(dá)形式，主要由庫(kù)所（P用圓表示，代表系統(tǒng)的狀態(tài)）、變遷（T用矩形表示，代表系統(tǒng)狀態(tài)的改變或動(dòng)作的執(zhí)行）、托肯（token代表數(shù)據(jù)類(lèi)型）、有向?。ˋ用箭頭表示，代表托肯的流動(dòng)方向）組成。

ASK-CTL模型檢驗(yàn)用于驗(yàn)證建模語(yǔ)言有色Petri網(wǎng)描述的系統(tǒng)模型與設(shè)計(jì)的系統(tǒng)性質(zhì)是否一致。將系統(tǒng)需要驗(yàn)證的性質(zhì)用ASK-CTL公式進(jìn)行描述與驗(yàn)證，如果系統(tǒng)模型符合描述的驗(yàn)證語(yǔ)言則返回結(jié)果“true”，如果不滿(mǎn)足則返回“false”，以便根據(jù)驗(yàn)證結(jié)果對(duì)設(shè)計(jì)進(jìn)行修改^[9]。

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

在CPN Tools中對(duì)系統(tǒng)模型進(jìn)行檢測(cè)時(shí)常用的函數(shù)是eval_node（），函數(shù)的格式是：val eval_node（VALUE self， NODE* node），其中self是ASK-CTL庫(kù)中自帶的查詢(xún)函數(shù)^[10]，例如自循環(huán)終端的檢測(cè)常用OutNodes（）函數(shù)，當(dāng)返回結(jié)果為“There is No loop Terminal！”時(shí)，表示系統(tǒng)模型不存在自循環(huán)；死鎖的檢測(cè)常用InvalidTerminal（）函數(shù)，當(dāng)返回結(jié)果為“No Deadlock Markings！”時(shí)，表示系統(tǒng)模型不存在死鎖。

2.3構(gòu)建車(chē)載設(shè)備CPN模型

C3級(jí)列控車(chē)載設(shè)備是對(duì)安全性要求較高的復(fù)雜系統(tǒng)。僅僅依靠傳統(tǒng)的建模語(yǔ)言無(wú)法完全描述出CTCS-3級(jí)列控車(chē)載設(shè)備模式轉(zhuǎn)換的多樣性，因此，需要一種能夠描述復(fù)雜系統(tǒng)的建模語(yǔ)言對(duì)模式轉(zhuǎn)換進(jìn)行分層建模，能夠更好表現(xiàn)出系統(tǒng)功能及結(jié)構(gòu)。

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

CPN模型以車(chē)載安全計(jì)算機(jī)為中心，車(chē)載設(shè)備主要變遷設(shè)為RBC、司機(jī)、列車(chē)、應(yīng)答器，將其與車(chē)載安全計(jì)算機(jī)的信息交互設(shè)為CPN模型的系統(tǒng)狀態(tài)即庫(kù)所，根據(jù)車(chē)載設(shè)備的功能可知庫(kù)所的主要狀態(tài)如表1所示。

車(chē)載設(shè)備的工作過(guò)程由工作模式不斷轉(zhuǎn)換來(lái)實(shí)現(xiàn)，因此將模式轉(zhuǎn)換作為安全計(jì)算機(jī)的主要狀態(tài)進(jìn)行建模。CTCS-3級(jí)列控車(chē)載設(shè)備主要包括待機(jī)模式（SB）、完全監(jiān)控模式（FS）、調(diào)車(chē)模式（SH）、目視行車(chē)模式（OS）、引導(dǎo)模式（CO）、休眠模式（SL）、冒進(jìn)防護(hù)模式（TR）、冒進(jìn)后防護(hù)模式（PT）、隔離模式（IS）9種工作模式^[12]。系統(tǒng)需求規(guī)范中規(guī)定了各工作模式轉(zhuǎn)換之間的轉(zhuǎn)換條件。車(chē)載設(shè)備工作模式轉(zhuǎn)換實(shí)例如表2所示。

CTCS-3級(jí)列控系統(tǒng)需求規(guī)范的模式轉(zhuǎn)換部分定義了列控車(chē)載設(shè)備的工作模式、與模式有關(guān)的功能以及各模式之間的轉(zhuǎn)換條件^[13?14]。主要工作模式對(duì)應(yīng)的車(chē)載設(shè)備職責(zé)：

1）?待機(jī)模式SB是一種默認(rèn)模式，司機(jī)不能對(duì)其進(jìn)行選擇，車(chē)載設(shè)備啟動(dòng)，自檢和測(cè)試通過(guò)后自動(dòng)進(jìn)入待機(jī)模式；

2）?當(dāng)車(chē)載設(shè)備接收到來(lái)自RBC的行車(chē)許可MA，列車(chē)數(shù)據(jù)和線(xiàn)路數(shù)據(jù)都具備后，車(chē)載設(shè)備轉(zhuǎn)入完全監(jiān)控模式FS，根據(jù)動(dòng)態(tài)曲線(xiàn)監(jiān)控列車(chē)運(yùn)行，并向司機(jī)顯示列車(chē)速度；

3）?調(diào)車(chē)模式SH用于列車(chē)進(jìn)行調(diào)車(chē)作業(yè)時(shí)，由司機(jī)選擇調(diào)車(chē)，車(chē)載設(shè)備應(yīng)向RBC申請(qǐng)授權(quán)并在進(jìn)入調(diào)車(chē)模式后與RBC斷開(kāi)連接；

4）?當(dāng)?shù)孛嬖O(shè)備故障，車(chē)載設(shè)備顯示禁止但列車(chē)需要繼續(xù)運(yùn)行時(shí)，由司機(jī)選擇轉(zhuǎn)入目視行車(chē)模式OS，從RBC接收請(qǐng)求，列車(chē)每運(yùn)行一定距離需司機(jī)確認(rèn)一次；

5）?引導(dǎo)模式CO用于開(kāi)放引導(dǎo)信號(hào)，接收RBC的請(qǐng)求后司機(jī)應(yīng)在此模式下檢查軌道占用；

6）?休眠模式SL用于非本務(wù)端車(chē)載設(shè)備，如果開(kāi)啟（異常操作），應(yīng)轉(zhuǎn)入待機(jī)模式SB；

7）?當(dāng)車(chē)載設(shè)備停用，隔離車(chē)載設(shè)備的制動(dòng)功能后，列控車(chē)載設(shè)備處于隔離模式IS，應(yīng)向司機(jī)指示車(chē)載設(shè)備已被隔離；

8）?當(dāng)車(chē)載設(shè)備輸出緊急制動(dòng)命令時(shí)進(jìn)入冒進(jìn)防護(hù)模式TR，應(yīng)要求司機(jī)確認(rèn)，列車(chē)實(shí)施緊急制動(dòng)；

9）?冒進(jìn)后防護(hù)模式PT時(shí)車(chē)載設(shè)備應(yīng)緩解緊急制動(dòng)，司機(jī)選擇啟動(dòng)，向RBC發(fā)送MA請(qǐng)求。

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

3CPN模型的驗(yàn)證與分析

3.1CPN模型的驗(yàn)證

有色Petri網(wǎng)建模語(yǔ)言對(duì)模型的驗(yàn)證是用ASK-CTL分支時(shí)序邏輯公式描述系統(tǒng)的性質(zhì)，通過(guò)對(duì)系統(tǒng)模型進(jìn)行系統(tǒng)邏輯性的驗(yàn)證分析，例如系統(tǒng)的自循環(huán)終端特性、死鎖特性等來(lái)證明系統(tǒng)模型是否可執(zhí)行，從而得出構(gòu)建的CPN模型是否滿(mǎn)足系統(tǒng)規(guī)范要求的規(guī)則以及各組件之間的交互是否符合規(guī)范流程。根據(jù)對(duì)系統(tǒng)需求規(guī)范中系統(tǒng)屬性分析，對(duì)構(gòu)建的車(chē)載設(shè)備CPN功能模型以及模式轉(zhuǎn)換CPN模型進(jìn)行了自循環(huán)終端檢測(cè)、死鎖和活鎖檢測(cè)驗(yàn)證。驗(yàn)證結(jié)果如下：

對(duì)所建車(chē)載設(shè)備CPN模型進(jìn)行自循環(huán)終端檢測(cè)是為了驗(yàn)證系統(tǒng)中死標(biāo)識(shí)的合理性，對(duì)模型執(zhí)行ASK-CTL公式，由圖7可知驗(yàn)證結(jié)果為“There is no loop terminal！”。

對(duì)車(chē)載設(shè)備CPN模型進(jìn)行死鎖分析，執(zhí)行ASK-CTL公式，由圖8可知驗(yàn)證結(jié)果為“No Deadlock Markings！”。

活鎖的檢查是根據(jù)狀態(tài)空間報(bào)告中OG和SCCG節(jié)點(diǎn)和弧的數(shù)量相同，即同構(gòu)的，則系統(tǒng)不存在活鎖。部分狀態(tài)空間報(bào)告如圖9所示。

采用ASK-CTL公式對(duì)模型進(jìn)行自循環(huán)驗(yàn)證和死鎖分析等，是為了驗(yàn)證模型的邏輯特性，只有系統(tǒng)死標(biāo)識(shí)合理，無(wú)死鎖及活鎖等特性，模型才是安全可執(zhí)行的。另外，還可通過(guò)CPNTools工具對(duì)模型進(jìn)行功能行為特性的檢查：如驗(yàn)證系統(tǒng)的活性、可達(dá)性、有界性、轉(zhuǎn)移性和公平性等^[15]。例如針對(duì)圖6系統(tǒng)工作狀態(tài)下進(jìn)行模式轉(zhuǎn)換規(guī)則驗(yàn)證，車(chē)載設(shè)備初始工作模式始終為待機(jī)SB模式，驗(yàn)證系統(tǒng)是否存在某條路徑，使待機(jī)模式SB轉(zhuǎn)入調(diào)車(chē)模式SH，驗(yàn)證執(zhí)行結(jié)果“true”，表示系統(tǒng)模型之間可轉(zhuǎn)移。

3.2模型驗(yàn)證結(jié)果分析

根據(jù)模型驗(yàn)證結(jié)果分析系統(tǒng)的屬性，只有系統(tǒng)模型中不存在死鎖、活鎖等屬性，才能驗(yàn)證系統(tǒng)功能屬性的正確性^[16]。

1） 車(chē)載設(shè)備自循環(huán)終端

自循環(huán)終端檢測(cè)是為了驗(yàn)證系統(tǒng)死標(biāo)識(shí)的合理性，由圖7的驗(yàn)證結(jié)果“There is no loop terminal！”?可知CPN模型中不存在自循環(huán)終端，驗(yàn)證了系統(tǒng)模型中死標(biāo)識(shí)是合理的，系統(tǒng)模型正確。說(shuō)明構(gòu)建的CPN模型滿(mǎn)足《CTCS-3級(jí)列控系統(tǒng)需求規(guī)范（SRS）》要求的車(chē)載設(shè)備信息交互流程。

2） 模式轉(zhuǎn)換無(wú)死鎖

無(wú)死鎖是指系統(tǒng)不會(huì)永遠(yuǎn)停留在一個(gè)狀態(tài)。根據(jù)圖8ASK-CTL描述的系統(tǒng)性質(zhì)驗(yàn)證結(jié)果?“No Deadlock Markings！”，可知系統(tǒng)在模式轉(zhuǎn)換過(guò)程中無(wú)死鎖，系統(tǒng)模型正確。

3） 模式轉(zhuǎn)換無(wú)活鎖

檢查系統(tǒng)活鎖的目的是為了發(fā)現(xiàn)系統(tǒng)中存在的死循環(huán)。由圖9可知，“State Space”中節(jié)點(diǎn)數(shù)和弧與“Scc Graph”中節(jié)點(diǎn)數(shù)和弧的數(shù)量相同，即同構(gòu)，說(shuō)明系統(tǒng)中不存在活鎖，系統(tǒng)模型正確。

系統(tǒng)模型既無(wú)死鎖也無(wú)活鎖，系統(tǒng)功能屬性正確，說(shuō)明構(gòu)建的CPN模型滿(mǎn)足《CTCS-3級(jí)列控系統(tǒng)需求規(guī)范（SRS）》要求的模式轉(zhuǎn)換功能。

4） 工作狀態(tài)下系統(tǒng)的行為特性

轉(zhuǎn)移性是指模型中一個(gè)模式與另一個(gè)模式之間存在遷移關(guān)系，即系統(tǒng)可經(jīng)過(guò)轉(zhuǎn)移從一個(gè)模式轉(zhuǎn)換到另一個(gè)模式，建模驗(yàn)證返回的執(zhí)行結(jié)果為true，表示系統(tǒng)從SB狀態(tài)可以經(jīng)過(guò)轉(zhuǎn)換步驟遷移到SH狀態(tài)，由此可知構(gòu)建的模式轉(zhuǎn)換CPN模型符合系統(tǒng)規(guī)范要求的CTCS-3級(jí)列控車(chē)載設(shè)備模式轉(zhuǎn)換條件。

4結(jié)??語(yǔ)

由于CTCS-3級(jí)列控車(chē)載設(shè)備是一個(gè)安全苛求性較高的復(fù)雜系統(tǒng)，而有色Petri網(wǎng)建模方法能夠?qū)δＰ瓦M(jìn)行分層建模，適用于復(fù)雜系統(tǒng)建模。研究主要分析了列控車(chē)載設(shè)備功能設(shè)計(jì)時(shí)涉及到的安全問(wèn)題，對(duì)CTCS-3 級(jí)列控系統(tǒng)車(chē)載設(shè)備之間的功能信息交互以及車(chē)載設(shè)備中安全計(jì)算機(jī)主要狀態(tài)工作模式轉(zhuǎn)換的各模式之間轉(zhuǎn)換路徑和模式之間具體轉(zhuǎn)換流程進(jìn)行了CPN建模，并在驗(yàn)證工具CPN Tools中使用時(shí)序邏輯公式ASK-CTL對(duì)所建模型系統(tǒng)功能性質(zhì)進(jìn)行描述，根據(jù)驗(yàn)證結(jié)果分析得到系統(tǒng)功能模型與相關(guān)系統(tǒng)需求規(guī)范的一致性。此外，提出的有色Petri網(wǎng)建模方法也適用于其他安全性要求較高的復(fù)雜系統(tǒng)建模驗(yàn)證研究。該建模驗(yàn)證方法能夠?qū)ο到y(tǒng)進(jìn)行圖形化描述，對(duì)復(fù)雜系統(tǒng)還可以進(jìn)行分層建模，大大減少系統(tǒng)空間爆炸的概率。形式化的建模方法能夠使建模工具對(duì)系統(tǒng)模型進(jìn)行驗(yàn)證確保系統(tǒng)設(shè)計(jì)規(guī)則的正確性和安全性，減少?gòu)?fù)雜系統(tǒng)設(shè)計(jì)規(guī)則的不可靠性，對(duì)安全苛求性要求較高的復(fù)雜系統(tǒng)的設(shè)計(jì)具有一定的參考意義。

參考文獻(xiàn)

［1］??張曙光. CTCS-3級(jí)列控系統(tǒng)總體技術(shù)方案[M]. 北京： 中國(guó)鐵道出版社， 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級(jí)列控車(chē)載設(shè)備建模、仿真和測(cè)試研究[D]. 北京： 北京交通大學(xué)， 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］??曹加云. 基于時(shí)間自動(dòng)機(jī)的CTCS-3級(jí)列控車(chē)載設(shè)備建模與驗(yàn)證[D]. 成都： 西南交通大學(xué)， 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網(wǎng)的測(cè)試用例生成研究進(jìn)展[J]. 重慶交通大學(xué)學(xué)報(bào)（自然科學(xué)版）， 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］??中國(guó)鐵路總公司. CTCS-3級(jí)列車(chē)運(yùn)行控制系統(tǒng)[M]. 北京： 中國(guó)鐵道出版社， 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級(jí)列控系統(tǒng)標(biāo)準(zhǔn)規(guī)范-CTCS-3級(jí)列控系統(tǒng)系統(tǒng)需求規(guī)范（SRS）（第一冊(cè)）[S]. 北京： 中國(guó)鐵道出版社， 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］??馬國(guó)富， 劉文良， 周建勇， 等. 基于ASK-CTL的有色Petri網(wǎng)模型檢驗(yàn)算法研究[J]. 計(jì)算機(jī)應(yīng)用與軟件， 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］??趙曉宇， 楊志杰， 呂旌陽(yáng). 基于有色Petri網(wǎng)的車(chē)載設(shè)備模式轉(zhuǎn)換測(cè)試序列生成方法[J]. 中國(guó)鐵道科學(xué)， 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］??胡少?gòu)?qiáng). 基于STPA和有色Petri網(wǎng)的列控系統(tǒng)安全分析[D]. 北京： 北京交通大學(xué)， 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］??趙偉慧. 基于場(chǎng)景的列控車(chē)載設(shè)備測(cè)試用例自動(dòng)生成方法研究[D]. 北京： 北京交通大學(xué)， 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.

（編輯??侯湘）