CBTC區(qū)域控制器切換場(chǎng)景的建模與驗(yàn)證

孫維正，曠文珍,2

(1.蘭州交通大學(xué) 自動(dòng)化與電氣工程學(xué)院，甘肅 蘭州 730070；2.甘肅省工業(yè)交通自動(dòng)化工程技術(shù)研究中心，甘肅 蘭州 730070)

隨著計(jì)算機(jī)技術(shù)和無線通信技術(shù)的快速發(fā)展，對(duì)于城市軌道交通通信方式的研究重點(diǎn)現(xiàn)已由有線信息傳輸轉(zhuǎn)向無線網(wǎng)絡(luò)通信，基于通信的列車運(yùn)行控制系統(tǒng)逐漸成為了我國(guó)城市軌道交通的重要組成部分[1]。CBTC系統(tǒng)是典型的高安全性和實(shí)時(shí)性關(guān)鍵系統(tǒng)，其對(duì)乘客的生命財(cái)產(chǎn)安全至關(guān)重要，在實(shí)際線路試驗(yàn)之前必須進(jìn)行嚴(yán)格的仿真測(cè)試。因此，采用合適的建模方法構(gòu)建符合CBTC系統(tǒng)功能需求的模型對(duì)列車高效、安全運(yùn)行具有重要意義。目前，國(guó)內(nèi)外對(duì)Petri網(wǎng)的運(yùn)用以及對(duì)CBTC的建模與仿真做了許多研究，德國(guó)學(xué)者HUNGAR等[2]以現(xiàn)有的ERTMS/ETCS規(guī)范為基礎(chǔ)，采用有色Petri網(wǎng)構(gòu)建了一個(gè)列控系統(tǒng)的形式化模型。張友兵等[3-4]采用有色Petri網(wǎng)對(duì)CTCS系統(tǒng)的無線閉塞中心RBC切換進(jìn)行了建模和分析，對(duì)不同數(shù)量車載電臺(tái)RBC的切換時(shí)間和成功率進(jìn)行了分析。有色Petri網(wǎng)有直觀的圖形表示并對(duì)顏色屬性進(jìn)行了拓展，但其對(duì)時(shí)間的建模還是很困難。楊旭文[5]采用UML建模方法對(duì)CBTC區(qū)域控制器的移動(dòng)授權(quán)(MA)生成功能進(jìn)行了建模與分析，并對(duì)SCADE所提供的基于系統(tǒng)模型的覆蓋率進(jìn)行了分析。UML是一種半形式化建模方法，不能對(duì)構(gòu)建的模型進(jìn)行檢驗(yàn)，具有一定的局限性，對(duì)系統(tǒng)的驗(yàn)證和分析帶來一定的困難。張鵬基[6]采用時(shí)間自動(dòng)機(jī)建模法對(duì)CBTC系統(tǒng)建立了進(jìn)路控制過程中各子模塊的模型。時(shí)間自動(dòng)機(jī)是一種形式化建模方法，適合描述反應(yīng)式離散數(shù)學(xué)系統(tǒng)，但構(gòu)造復(fù)雜系統(tǒng)時(shí)間自動(dòng)機(jī)模型的工作量太大，不適合描述具有并發(fā)狀態(tài)的連續(xù)系統(tǒng)。區(qū)域控制器是CBTC系統(tǒng)中安全性、實(shí)時(shí)性要求較高的地面設(shè)備，僅僅依靠傳統(tǒng)的建模語言無法完全描述ZC邊界切換時(shí)車載與地面的信息交互過程，因此需要一種能夠描述復(fù)雜系統(tǒng)的建模方法對(duì)其進(jìn)行分層建模。對(duì)比現(xiàn)有的有色Petri網(wǎng)、UML以及時(shí)間自動(dòng)機(jī)等單一的建模方法，利用UML結(jié)合層次時(shí)間有色Petri網(wǎng)(HTCPN)建立的模型可以直接用建模工具CPN Tools進(jìn)行驗(yàn)證和分析。對(duì)于分析ZC邊界切換這種復(fù)雜過程，采用UML模型可以直觀地描述ZC系統(tǒng)的功能需求和邊界切換過程；引入分層結(jié)構(gòu)可以簡(jiǎn)化系統(tǒng)結(jié)構(gòu)，減小系統(tǒng)驗(yàn)證復(fù)雜度；引入時(shí)間戳可以描述ZC邊界切換時(shí)車載與地面的通信周期，符合系統(tǒng)并發(fā)性、實(shí)時(shí)性的要求[7]。本文選用兩者相結(jié)合的集成建模方法更加適用于ZC切換場(chǎng)景，能夠解決系統(tǒng)空間爆炸問題，更有效地表現(xiàn)出系統(tǒng)的功能及結(jié)構(gòu)，更加適用于復(fù)雜系統(tǒng)的建模。

1 ZC邊界切換功能需求分析

區(qū)域控制器ZC通過與車載VOBC、列車自動(dòng)監(jiān)督系統(tǒng)ATS、數(shù)據(jù)儲(chǔ)存單元DSU以及聯(lián)鎖CI之間進(jìn)行頻繁的通信來保證列車的安全運(yùn)行[8]。ZC的具體功能有：線路狀態(tài)信息管理、列車的登錄與注銷、列車追蹤、ZC邊界切換和移動(dòng)授權(quán)(MA)生成[9]。

由于列車在線路上運(yùn)行的過程中只受其所占區(qū)段的區(qū)域控制器控制，所以當(dāng)列車越過2個(gè)區(qū)域控制器間的分界線，從一個(gè)ZC控制區(qū)域進(jìn)入另一個(gè)ZC控制區(qū)域時(shí)，控制該列車的區(qū)域控制器應(yīng)該從移交ZC(ZC1)切換至接管ZC(ZC2)[10]。ZC邊界切換如圖1所示，具體切換流程如下：

圖1 ZC切換示意圖Fig.1 ZC switching diagram

1)切換請(qǐng)求：當(dāng)列車即將到達(dá)分界線時(shí)，車載VOBC向移交ZC發(fā)送越界授權(quán)請(qǐng)求，移交ZC向接管ZC發(fā)送越界預(yù)告。接管ZC會(huì)將下一區(qū)段的進(jìn)路狀況發(fā)送給移交ZC，移交ZC再結(jié)合本區(qū)段的進(jìn)路情況計(jì)算混合MA發(fā)送給車載VOBC。

2)通信請(qǐng)求：當(dāng)列車車頭到達(dá)分界線時(shí)，車載VOBC向接管ZC發(fā)送通信請(qǐng)求。通信連接成功后列車只接收移交ZC計(jì)算發(fā)送的MA，車載和接管ZC只保持通信關(guān)系。

3)登錄請(qǐng)求：當(dāng)列車車尾越過分界線時(shí)，車載VOBC請(qǐng)求登錄接管ZC。接管ZC收到申請(qǐng)后向車載發(fā)送數(shù)據(jù)庫版本信息，當(dāng)列車數(shù)據(jù)庫版本與ZC數(shù)據(jù)庫版本兼容時(shí)，列車登錄成功[11]。

4)注銷請(qǐng)求：當(dāng)列車最小安全末端越過分界線時(shí)，車載VOBC向移交ZC發(fā)送注銷請(qǐng)求，同時(shí)向接管ZC發(fā)送接管請(qǐng)求。當(dāng)接管ZC收到移交ZC發(fā)送的列車注銷信息后正式控制列車，ZC邊界切換結(jié)束。

2 ZC邊界切換模型的構(gòu)建

2.1 構(gòu)建ZC邊界切換UML模型

UML是面向?qū)ο蠹夹g(shù)發(fā)展和軟件系統(tǒng)描述標(biāo)準(zhǔn)化、可視化、文檔化的產(chǎn)物，包括用例圖、順序圖和狀態(tài)圖等9種圖形[12]。根據(jù)ZC邊界切換具體流程構(gòu)建UML用例圖、順序圖和狀態(tài)圖。如圖2所示，用例圖描述了參與者和用例之間的關(guān)系，參與者包括車載VOBC，移交ZC(ZC1)和接管ZC(ZC2)，它們之間的用例關(guān)系包括正?？剀?Nor‐mal)、位置報(bào)告(Train Location)、進(jìn)路信息(Access Information)、斷 開 通 信(Disconnect Communica‐tion)和建立通信(Connect Communication)。

圖2 ZC切換UML用例圖模型Fig.2 ZCswitch UML use case diagram model

順序圖反映了ZC1，ZC2和車載VOBC之間的協(xié)作關(guān)系，說明了車載在不同位置、不同狀態(tài)下與ZC1和ZC2之間的交互過程以及發(fā)送消息的先后次序[12]。ZC邊界切換順序如圖3所示。

圖3 ZC切換UML順序圖模型Fig.3 ZCswitch UML sequence diagram model

狀態(tài)圖顯示了車載VOBC在ZC邊界切換過程中的狀態(tài)變化，描述了車載VOBC在切換過程中所有歷程，ZC邊界切換過程中列車狀態(tài)的轉(zhuǎn)換如圖4所示。

圖4 ZC切換UML狀態(tài)圖模型Fig.4 ZCswitch UML state diagram model

2.2 UML模型向CPN模型轉(zhuǎn)換

UML模型和CPN模型之間存在較大的語義差異，如果采用圖形轉(zhuǎn)換方法的話，很難確定雙方對(duì)應(yīng)的關(guān)系[13]。

本文通過UML模型中各類節(jié)點(diǎn)與CPN模型嚴(yán)格的一一對(duì)應(yīng)關(guān)系，將UML模型中的元素提取為不同類型的節(jié)點(diǎn)，形成UML模型向CPN模型轉(zhuǎn)移的中間模型。中間模型的節(jié)點(diǎn)分為5種類型，分別是簡(jiǎn)單節(jié)點(diǎn)、流程結(jié)構(gòu)類節(jié)點(diǎn)、功能類節(jié)點(diǎn)、復(fù)合節(jié)點(diǎn)和資源類節(jié)點(diǎn)[14]，表1為UML模型向CPN模型轉(zhuǎn)移的簡(jiǎn)單規(guī)則，圖5為提取后的中間模型XML格式。

圖5 提取后的中間模型Fig.5 Extracted intermediate model

表1 UML向CPN的轉(zhuǎn)移規(guī)則Table 1 UML to CPN transfer rules

2.3 構(gòu)建ZC邊界切換CPN模型

有色Petri網(wǎng)模型中有3個(gè)重要的模型元素：庫所、變遷和有向弧[15?16]。在ZC切換過程中車載VOBC和ZC1，ZC2不斷進(jìn)行信息交互，由于其他學(xué)者構(gòu)建CPN模型是從ZC角度來考慮，本文CPN的頂層模型則通過車載VOBC在行進(jìn)中不同狀態(tài)及位置轉(zhuǎn)換的角度來建立。根據(jù)2.2節(jié)的轉(zhuǎn)移規(guī)則，將UML用例圖轉(zhuǎn)換為CPN模型的頂層模型，順序圖和狀態(tài)圖轉(zhuǎn)換為子模型，轉(zhuǎn)換后的CPN模型由庫所集P和變遷集T組成，如圖6所示。

圖6 ZC切換頂層模型初始狀態(tài)Fig.6 ZCswitches the initial state of the top-level model

CPN模型庫所集為：

P={VOBC1，VOBC2，VOBC3，VOBC4，VOBC5，VOBC6}

CPN模型變遷集為：

T={Noraml，Near，F(xiàn)ront pass，Rear pass，MinRear pass}

頂層中的每個(gè)變遷都是替代變遷，每個(gè)替代變遷代表列車相對(duì)于ZC分界線的不同位置。替代變遷相鄰的庫所為槽庫所，將ZC切換用例圖中唯一的系統(tǒng)外部角色車載VOBC映射為槽庫所，VOBC1到VOBC6代表車載不同位置時(shí)的不同狀態(tài)。

CPN子模型為頂層模型中每個(gè)替代變遷細(xì)化后的部分，根據(jù)UML向CPN的轉(zhuǎn)移規(guī)則，將UML順序圖的對(duì)象ZC1，車載VOBC和ZC2，分別轉(zhuǎn)換為子網(wǎng)模型的主要庫所，將不同狀態(tài)下的車載VOBC設(shè)為輸入、輸出2個(gè)端口庫所，與頂層模型槽庫所相對(duì)應(yīng)。

CPN模型顏色集、變量定義如下：

colset MSG=string timed;

colset MOG=bool with(no,yes)timed;

colset MIG=int timed;

colset MIGxMSG=product MIG*MSGtimed;

colset MIGxMOG=product MIG*MOG timed;

colset NetDelay=int with 200..500 timed;

var m,n,q,e:MSG;

var h,k:MOG;

var s,p,r:MSG;

fun Dec()=MOG.ran();

fun Del()=NetDelay.ran();

CBTC系統(tǒng)對(duì)車地通信技術(shù)傳輸通道分為地對(duì)車信息傳輸(下行無線鏈路)和車對(duì)地信息傳輸(上行無線鏈路)。無論是車對(duì)地信息傳輸還是地對(duì)車信息傳輸，它們的通信周期都為200～500 ms，因此本文CPN子模型中均采用在變遷中設(shè)置“@+Del()”離散分布函數(shù)(在200到500中隨機(jī)產(chǎn)生一個(gè)延時(shí)時(shí)間值)的方式來模擬車載VOBC和區(qū)域控制器之間的通信周期。

圖7 ZC切換Normal子網(wǎng)模型Fig.7 ZCswitches Normal subnet model

Normal子網(wǎng)模型是車載在ZC切換前以ATP模式正常行駛的狀態(tài)，車載VOBC將位置信息(“Lo‐cation Report1”)發(fā)送給ZC1。ZC1會(huì)判斷列車是否接近分界線，若列車沒有接近，ZC1則向車載VOBC發(fā)送正?？剀嚸钋伊熊嚂?huì)繼續(xù)向ZC1發(fā)送位置信息，列車；若列車接近，ZC1則向列車發(fā)送移交命令(“Handover1”)。

圖8 ZC切換Near子網(wǎng)模型Fig.8 ZC switches Near subnet model

圖9 ZC切換Front pass子網(wǎng)模型Fig.9 ZCswitches Front pass subnet model

Near子網(wǎng)模型是列車最大前端接近ZC分界點(diǎn)，車載VOBC將位置信息(“Location Report2”)和切換預(yù)告發(fā)送給ZC1。ZC1向ZC2進(jìn)行通信請(qǐng)求，請(qǐng)求ZC2發(fā)送下個(gè)區(qū)段進(jìn)路信息。ZC2會(huì)判斷是否有新的空閑進(jìn)路，若有空閑進(jìn)路，則將進(jìn)路狀態(tài)計(jì)算發(fā)送給ZC1，ZC1再將信息整合計(jì)算為混合MA發(fā)送給車載VOBC。

圖10 ZC切換Rear pass子網(wǎng)模型Fig.10 ZCswitches Rear pass subnet model

圖11 ZC切換MinRear pass子網(wǎng)模型Fig.11 ZCswitches MinRear pass subnet model

Front pass子網(wǎng)模型是列車前端越過ZC分界線，車載VOBC將位置信息(“Location Report3”)發(fā)送給ZC1，同時(shí)向ZC2發(fā)送通信請(qǐng)求。ZC2收到請(qǐng)求后會(huì)發(fā)送回應(yīng)信息(“ACK”)。ZC1會(huì)判斷車載前端是否通過分界線，若前端通過分界線，則向列車發(fā)送移交命令(“Handover2”)。

Rear pass子網(wǎng)模型是列車末端越過ZC分界線，車載VOBC將位置信息(“Location Report4”)發(fā)送給ZC1，ZC1會(huì)判斷列車末端是否越過分界線。若列車末端越過分界線，則向列車發(fā)送移交命令(“Handover3”)，同時(shí)列車會(huì)向ZC2發(fā)送登錄申請(qǐng)。ZC2收到申請(qǐng)后將版本信息發(fā)送給車載VOBC，若可以匹配，則列車成功登錄ZC2。

MinRear pass子網(wǎng)模型是列車最小安全末端越過ZC分界線，車載VOBC將位置信息(“Location Report5”)和登出請(qǐng)求發(fā)送給ZC1。若ZC1判斷為“MinRear Pass”，ZC1會(huì)向車載發(fā)送終止通信MA(“Termination”)，ZC2接收到列車登出消息后正式控制列車并和ZC1結(jié)束通信，ZC邊界切換結(jié)束。

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

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

有色Petri網(wǎng)建模語言對(duì)模型的驗(yàn)證是利用CPN Tools的State space工具箱完成狀態(tài)空間自動(dòng)分析，本文采用狀態(tài)空間報(bào)告和ASK-CTL邏輯公式2種工具來驗(yàn)證所構(gòu)建的CPN模型。

1)狀態(tài)空間報(bào)告：針對(duì)模型本身的屬性，將模型的狀態(tài)空間進(jìn)行窮舉搜索，從而獲得模型的家態(tài)性、活性及公平性等動(dòng)態(tài)屬性信息。為避免偶然因素造成誤差，本文采用CPN Tools軟件對(duì)所構(gòu)建的CPN模型進(jìn)行500次仿真得到如圖12所示的頂層模型仿真結(jié)果和如圖13所示的狀態(tài)空間報(bào)告。

圖12 ZC切換頂層模型仿真結(jié)果Fig.12 ZCswitch top model simulation results

圖13 ZC切換自循環(huán)終端驗(yàn)證Fig.13 ZCswitching self-circulation terminal verification

由于列車在行進(jìn)過程中不斷與ZC進(jìn)行信息交互，因此邊界切換過程會(huì)不斷重復(fù)來保證ZC能夠?qū)崟r(shí)控制列車安全運(yùn)行。本文只取一次ZC邊界切換過程進(jìn)行分析，每個(gè)VOBC庫所的Token值代表列車在不同位置時(shí)車載接收到的信息，具體信息含義如表2所示。

2)ASK-CTL邏輯公式：通過對(duì)系統(tǒng)模型進(jìn)行系統(tǒng)邏輯性的驗(yàn)證分析(系統(tǒng)的自循環(huán)終端特性、死鎖特性等)來證明系統(tǒng)模型是否可執(zhí)行，從而得出構(gòu)建的CPN模型是否滿足系統(tǒng)規(guī)范要求的規(guī)則以及各組件之間的交互是否符合規(guī)范流程。

根據(jù)對(duì)CBTC系統(tǒng)需求規(guī)范中系統(tǒng)屬性的分析，對(duì)構(gòu)建的ZC切換CPN模型進(jìn)行了自循環(huán)終端檢測(cè)、死鎖和活鎖檢測(cè)驗(yàn)證。對(duì)所建CPN模型進(jìn)行自循環(huán)終端檢測(cè)是為了驗(yàn)證系統(tǒng)中死標(biāo)識(shí)的合理性，對(duì)模型執(zhí)行ASK-CTL公式得到的結(jié)果如圖13所示。

活鎖是觀察狀態(tài)空間報(bào)告中“State Space”和“SCC Graph”節(jié)點(diǎn)和弧的數(shù)量，以此來檢查模型中是否存在死循環(huán)。

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

根據(jù)模型驗(yàn)證結(jié)果分析系統(tǒng)的屬性，只有系統(tǒng)模型的動(dòng)態(tài)屬性符合系統(tǒng)功能需求且模型不存在死鎖和活鎖，才能驗(yàn)證系統(tǒng)功能屬性的正確性[17]。

1)ZC切換CPN模型動(dòng)態(tài)屬性

由狀態(tài)空間報(bào)告可知模型的動(dòng)態(tài)屬性情況：

①家態(tài)性：模型不存在回歸性標(biāo)志，即系統(tǒng)不存在可重復(fù)運(yùn)行的狀態(tài)節(jié)點(diǎn)。

②活性：模型中存在一個(gè)死標(biāo)識(shí)意味著存在一個(gè)無法觸發(fā)的變遷，需要通過進(jìn)一步驗(yàn)證死鎖來證明死標(biāo)識(shí)的存在是否合理。

③公平性：公平性即模型每個(gè)變遷發(fā)生的頻率。由狀態(tài)空間報(bào)告可知，模型中沒有無窮發(fā)生序列，即模型各部分對(duì)資源的占用是公平的。

2)ZC切換CPN模型自循環(huán)終端

由圖13的驗(yàn)證結(jié)果“No self loop terminal!”可知CPN模型中不存在自循環(huán)終端，驗(yàn)證了系統(tǒng)模型中死標(biāo)識(shí)是合理的，系統(tǒng)模型正確。說明構(gòu)建的CPN模型滿足CBTC系統(tǒng)規(guī)范，滿足ZC邊界切換功能需求。

3)ZC切換CPN模型無活鎖

“State Space”中節(jié)點(diǎn)數(shù)和弧與“SCC Graph”中節(jié)點(diǎn)數(shù)和弧的數(shù)量相同，即同構(gòu)。說明系統(tǒng)模型不存在死循環(huán)，系統(tǒng)中不存在活鎖。

綜上所述，構(gòu)建的ZC邊界切換CPN模型動(dòng)態(tài)屬性正常且不存在死鎖和活鎖，因此ZC邊界切換過程是安全的，所構(gòu)建的模型是正確的[18]。

4 結(jié)論

1)分析了ZC邊界切換具體流程并對(duì)切換場(chǎng)景下車載VOBC、移交ZC和接管ZC之間的信息交互和各自狀態(tài)進(jìn)行了UML用例圖和順序圖的建模。根據(jù)UML模型向CPN模型轉(zhuǎn)移的規(guī)則，提取了UML模型向CPN轉(zhuǎn)移的中間模型。

2)利用CPN Tools工具將中間模型構(gòu)建為CPN模型，并使用狀態(tài)空間報(bào)告和ASK-CTL公式對(duì)所建模型系統(tǒng)功能性質(zhì)進(jìn)行驗(yàn)證。根據(jù)驗(yàn)證結(jié)果分析得到系統(tǒng)功能模型的各種動(dòng)態(tài)屬性正常且無死鎖和活鎖，與系統(tǒng)需求規(guī)范一致。

3)此外，文中提出的UML和HTCPN相結(jié)合的建模也適用于其他安全性要求較高的復(fù)雜系統(tǒng)建模驗(yàn)證研究。該建模方法可以更直觀的展現(xiàn)系統(tǒng)功能；引入的分層結(jié)構(gòu)可以大大減少系統(tǒng)空間爆炸的概率；添加的時(shí)間戳可以解決系統(tǒng)時(shí)序關(guān)系限制的問題，確保系統(tǒng)符合實(shí)時(shí)性、并發(fā)性的特點(diǎn)，對(duì)安全苛求性要求較高的復(fù)雜系統(tǒng)的設(shè)計(jì)具有一定的參考意義。