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

楊 璐，陳永剛

(蘭州交通大學(xué)自動(dòng)化與電氣工程學(xué)院，蘭州 730070)

基于通信的列車(chē)運(yùn)行控制系統(tǒng)(Communication Based Train Control， CBTC)用于控制城市軌道交通列車(chē)的運(yùn)行，是保證列車(chē)安全、高效運(yùn)行的系統(tǒng)，區(qū)域控制子系統(tǒng)作為其關(guān)鍵的軌旁設(shè)備，主要實(shí)現(xiàn)為轄區(qū)內(nèi)的列車(chē)計(jì)算移動(dòng)授權(quán)(Moving Authorization， MA)、完成邊界切換等功能[1-2]。如果ZC子系統(tǒng)控制邏輯存在潛在缺陷，很可能導(dǎo)致CBTC系統(tǒng)在運(yùn)行中失效，造成人員傷亡或重大財(cái)產(chǎn)損失等災(zāi)難性后果[3]。為了保證列車(chē)安全運(yùn)行、降低事故發(fā)生率、需要高可靠性、高安全性的列車(chē)運(yùn)行控制系統(tǒng)作為保障[4]。ZC切換作為CBTC系統(tǒng)的重要場(chǎng)景，是保證行車(chē)安全的基礎(chǔ)，因而，針對(duì)ZC邊界切換功能安全性的驗(yàn)證就顯得尤為重要。

目前，已有許多學(xué)者對(duì)列控系統(tǒng)的安全性和實(shí)時(shí)性進(jìn)行了大量的研究，如劉金濤博士采用基于微分動(dòng)態(tài)邏輯理論的推理證明方式對(duì)RBC子系統(tǒng)進(jìn)行了建模驗(yàn)證，采用大量的公式推理，驗(yàn)證過(guò)程繁瑣復(fù)雜[5]。張友兵采用有色Petri網(wǎng)和故障樹(shù)實(shí)現(xiàn)了對(duì)RBC兩種切換方式的建模，并對(duì)切換成功率進(jìn)行了評(píng)估，但沒(méi)有實(shí)現(xiàn)有效的驗(yàn)證[6]。黃友能采用混成自動(dòng)機(jī)理論對(duì)城市軌道交通ZC子系統(tǒng)的混成性進(jìn)行了研究，但組合片段轉(zhuǎn)換過(guò)程復(fù)雜易出錯(cuò)[7]。本文采用半形式化方法MSC和形式化方法UPPAAL相結(jié)合的方法對(duì)ZC切換場(chǎng)景進(jìn)行研究，建立ZC切換過(guò)程的MSC模型，將其轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)模型，采用驗(yàn)證工具UPPAAL對(duì)其安全性和受限活性進(jìn)行驗(yàn)證。

1 ZC切換過(guò)程分析

當(dāng)列車(chē)從移交ZC轄區(qū)進(jìn)入接管ZC轄區(qū)時(shí)，控制列車(chē)運(yùn)行的區(qū)域控制器應(yīng)從移交ZC切換至接管ZC，切換過(guò)程分為以下4步。

(1)列車(chē)在移交ZC區(qū)域內(nèi)運(yùn)行，當(dāng)列車(chē)接近分界點(diǎn)P，即列車(chē)收到以分界點(diǎn)P為終點(diǎn)的MA時(shí)，移交ZC與接管ZC建立通信會(huì)話(huà)，觸發(fā)邊界切換功能，如圖1所示。

圖1 邊界切換觸發(fā)控制示意

(2) 如圖2所示，當(dāng)移交ZC與接管ZC通信成功后，移交ZC計(jì)算MA1，同時(shí)向接管ZC發(fā)送切換預(yù)告信息并為列車(chē)請(qǐng)求接管ZC范圍內(nèi)的進(jìn)路，進(jìn)路排出以后接管ZC將MA2發(fā)送給移交ZC，移交ZC將混合后的MixedMA發(fā)送給列車(chē)，控制列車(chē)運(yùn)行。

圖2 MA延伸至接管ZC時(shí)切換控制示意

(3) 如圖3所示，當(dāng)列車(chē)前端越過(guò)分界點(diǎn)P時(shí)，車(chē)載系統(tǒng)與接管ZC之間建立通信連接，車(chē)載系統(tǒng)與接管ZC連接成功以后，車(chē)載系統(tǒng)向接管ZC發(fā)送登錄申請(qǐng)，接管ZC發(fā)送數(shù)據(jù)庫(kù)版本信息，列車(chē)向接管ZC發(fā)送登錄確認(rèn)信息后登錄成功。

圖3 車(chē)頭越過(guò)邊界點(diǎn)時(shí)邊界切換控制示意

(4) 如圖4所示，當(dāng)列車(chē)車(chē)尾越過(guò)分界點(diǎn)P后，列車(chē)向接管ZC發(fā)送受控申請(qǐng)，向移交ZC發(fā)送注銷(xiāo)申請(qǐng)，當(dāng)列車(chē)收到接管ZC發(fā)送的控制列車(chē)的信息后，移交ZC向列車(chē)發(fā)送注銷(xiāo)確認(rèn)信息，列車(chē)根據(jù)接管ZC發(fā)送的控制信息控制列車(chē)正常運(yùn)行，至此，整個(gè)邊界切換過(guò)程結(jié)束。

圖4 車(chē)尾越過(guò)邊界時(shí)邊界切換控制示意

2 ZC切換過(guò)程建模

2.1 基于MSC的系統(tǒng)建模

消息順序圖(MSC)是一種簡(jiǎn)潔的圖形化描述語(yǔ)言，用來(lái)直觀描述并行系統(tǒng)中各部件之間信息交互過(guò)程[8]。本文中采用MSC建立ZC切換場(chǎng)景的MSC模型，結(jié)合ZC切換過(guò)程中可能導(dǎo)致系統(tǒng)出現(xiàn)故障的各種情況，為后續(xù)時(shí)間自動(dòng)機(jī)模型的建立提供依據(jù)。

定義：MSC是一個(gè)五元組，并且有MSC=(IMft{≤i}i∈l)用來(lái)描述ZC切換場(chǎng)景中各個(gè)子系統(tǒng)之間的信息交互關(guān)系，其定義如下。

(1)I={ITrain，IZC1，IZC2}分別表示車(chē)載子系統(tǒng)，移交ZC子系統(tǒng)和接管ZC子系統(tǒng)。

(2)M={MTrain，MZC1，MZC2}分別表示與車(chē)載子系統(tǒng)、移交ZC子系統(tǒng)及接管ZC子系統(tǒng)相關(guān)的消息集，其中MTrain={MAextendreq， ConnectZC1， Conf， Login1， Version1， Conf1， Control， MixedMA， ConnectZC2， Con-f4， LoginZC2， Version， Conf5， Pass， Conf6， Reqcontrol，Cancel， ControlT， Ackcancel};MZC1={MAextendreq， YG， Conf2， Conf3， Connect2， Routereq， MA2， MixedMA， ConnectZC1， Conf， Login1， Version1， Conf1， Control， Cancel， Ackcancel};MZC2={Connect2， Conf2， YG， Conf3， Routereq， MA2， Conf4， ConnectZC2， LoginZC2， Version， Conf5， Pass， Conf6， Reqcontrol， ControlT}。

(3)≤inst=Ui∈I。

(4)≤io={(!m，？m) |m∈M}。

定義中的f和t是從消息集M映射到實(shí)數(shù)集I上的函數(shù)，如f(MAextendreq)=ITrain，t(MAexte-ndreq)=IZC1。發(fā)送消息事件m用!m表示，接收消息事件m用？m表示，如：消息事件MAextendreq從Train子系統(tǒng)發(fā)送至ZC1子系統(tǒng)表示為，ZC1子系統(tǒng)接受從Train子系統(tǒng)發(fā)來(lái)的MAextendreq消息表示為?！躨表示實(shí)體i發(fā)生的事件對(duì)應(yīng)到時(shí)間軸上的先后順序，如對(duì)于實(shí)體Train上發(fā)生的兩個(gè)事件MAextendreq和MixedMA，事件MAextendreq先于事件MixedMA發(fā)生。 ≤io表示對(duì)于任意一個(gè)消息事件，事件的發(fā)送先于接收發(fā)生，即?m，!m≤io？m；如對(duì)于消息事件MAextendreq，Train子系統(tǒng)發(fā)送MAextendreq消息事件先于ZC1子系統(tǒng)接收MAextendreq消息事件發(fā)生。

根據(jù)以上定義，對(duì)ZC邊界切換過(guò)程進(jìn)行建模，假定切換過(guò)程中發(fā)生的消息事件都按正常的消息流程進(jìn)行，根據(jù)消息事件發(fā)送、接收的因果關(guān)系，建立ZC切換過(guò)程的MSC模型，如圖5所示。

圖5 ZC邊界切換過(guò)程MSC模型

2.2 模型描述

ZC切換過(guò)程中涉及的信息交互的對(duì)象有車(chē)載子系統(tǒng)(Train)，移交區(qū)域控制子系統(tǒng)(ZC1)，接管區(qū)域控制子系統(tǒng)(ZC2)。

(1)接近邊界點(diǎn)(授權(quán)的終點(diǎn)為分界點(diǎn))：列車(chē)在ZC1區(qū)域運(yùn)行過(guò)程中，若某時(shí)刻Train收到了以邊界點(diǎn)P為終點(diǎn)的移動(dòng)授權(quán)，Train向ZC1發(fā)送授權(quán)延伸申請(qǐng)消息MAextendreq，然后ZC1向ZC2發(fā)送與ZC2建立通信連接的請(qǐng)求消息Connect2，ZC2向ZC1發(fā)送連接確認(rèn)消息Conf2，相鄰ZC間建立通信過(guò)程完成。ZC1向ZC2發(fā)送切換預(yù)告信息YG，并為列車(chē)申請(qǐng)ZC2范圍內(nèi)的進(jìn)路，當(dāng)聯(lián)鎖系統(tǒng)排出進(jìn)路以后，ZC2將進(jìn)路信息MA2發(fā)給ZC1，由ZC1將ZC1范圍內(nèi)進(jìn)路信息與之混合后將新的授權(quán)信息MixedMA發(fā)送給列車(chē)，控制列車(chē)運(yùn)行，如果在T5(5s)內(nèi)Train沒(méi)有收到MixedMA信息，則出現(xiàn)車(chē)地通信故障，實(shí)施緊急制動(dòng)。

(2)車(chē)頭越過(guò)邊界點(diǎn)P：當(dāng)列車(chē)車(chē)頭越過(guò)邊界點(diǎn)P后，Train收到切換執(zhí)行應(yīng)答器組(LTO)發(fā)送的執(zhí)行轉(zhuǎn)換消息，Train根據(jù)之前MixedMA中ZC2的信息，向ZC2發(fā)送與ZC2建立通信連接的請(qǐng)求消息ConnectZC2，ZC2向Train發(fā)送連接確認(rèn)消息Conf4，連接ZC2成功后，Train向ZC2發(fā)送登錄申請(qǐng)消息LoginZC2，ZC2將本身系統(tǒng)的版本號(hào)信息發(fā)送給Train，若版本號(hào)信息相同則Train向ZC2發(fā)送登錄確認(rèn)消息Conf5，否則Train系統(tǒng)從數(shù)據(jù)庫(kù)存儲(chǔ)單元(DSU)重新下載。

(3)車(chē)尾通過(guò)邊界點(diǎn)P：當(dāng)列車(chē)車(chē)尾越過(guò)邊界點(diǎn)P后，Train向ZC2發(fā)送受控申請(qǐng)消息Reqcontrol，并向ZC1發(fā)送注銷(xiāo)消息Cancel，當(dāng)列車(chē)收到ZC2的控制消息ControlT后，ZC1向Train發(fā)送注銷(xiāo)確認(rèn)消息ACKcancel，整個(gè)切換過(guò)程結(jié)束，此后Train子系統(tǒng)在ZC2的控制下繼續(xù)正常運(yùn)行。

3 系統(tǒng)模型仿真

3.1 驗(yàn)證工具UPPAAL

時(shí)間自動(dòng)機(jī)是在自動(dòng)機(jī)理論基礎(chǔ)上擴(kuò)展的基于時(shí)間周期、時(shí)間約束和時(shí)間解釋的實(shí)時(shí)系統(tǒng)建模方法[9]，相較于CPN、SPN及CSP，其主要優(yōu)勢(shì)在于有驗(yàn)證工具為其提供建模、仿真和驗(yàn)證環(huán)境[10]。UPPAAL通過(guò)模擬有限個(gè)控制結(jié)構(gòu)和數(shù)值時(shí)鐘來(lái)驗(yàn)證系統(tǒng)的安全性和受限活性[11-13]。

UPPAAL用戶(hù)界面的編輯器、模擬器和驗(yàn)證器分別用于實(shí)時(shí)系統(tǒng)的建模、仿真和驗(yàn)證。模擬器不僅可以按狀態(tài)轉(zhuǎn)移檢查狀態(tài)的轉(zhuǎn)移是否是期望的結(jié)果，當(dāng)系統(tǒng)出現(xiàn)鎖死時(shí)，還可以檢查到出現(xiàn)鎖死的部位繼而對(duì)模型進(jìn)行修正。驗(yàn)證器通過(guò)對(duì)狀態(tài)空間的搜索來(lái)驗(yàn)證系統(tǒng)的功能屬性和受限活性。UPPAAL專(zhuān)門(mén)為模型的驗(yàn)證提供了一種BNF語(yǔ)法[14-15]。具體語(yǔ)法含義如表1所示。

表1 BNF語(yǔ)法的含義

3.2 ZC切換過(guò)程模型

對(duì)于ZC切換過(guò)程的MSC模型僅僅直觀描述了時(shí)間的進(jìn)程，卻無(wú)法對(duì)模型進(jìn)行有效的分析和驗(yàn)證，所以需要將MSC模型描述的ZC切換過(guò)程轉(zhuǎn)換成時(shí)間自動(dòng)機(jī)模型，然后用UPPAAL工具對(duì)其進(jìn)行驗(yàn)證。文中對(duì)ZC切換過(guò)程中涉及信息交互的3個(gè)活動(dòng)對(duì)象分別建立各自的子時(shí)間自動(dòng)機(jī)模型，即TATrain、TAZC1、TAZC2。ZC切換過(guò)程是這3個(gè)自時(shí)間自動(dòng)機(jī)的積，即TA=TATrain||TAZC1||TAZC2。

圖6為ZC切換過(guò)程的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型。其中，以“!”為結(jié)尾的消息表示該條消息發(fā)出以后子系統(tǒng)位置發(fā)生轉(zhuǎn)換，以“？”為結(jié)尾的消息表示收到該條消息后子系統(tǒng)位置發(fā)生轉(zhuǎn)換，以此保證各子系統(tǒng)模型之間同一轉(zhuǎn)換的同步發(fā)生。x、y、z和t為時(shí)鐘約束，用于判斷ZC1與ZC2的連接時(shí)間、Train與ZC2的連接時(shí)間、Train登錄ZC2的時(shí)間以及ZC1計(jì)算MixedMA的時(shí)間是否超時(shí)。 routeorder、same和co mmunication為標(biāo)志位，用于統(tǒng)一不同子系統(tǒng)間狀態(tài)遷移的同步性。

圖6 ZC邊界切換時(shí)間自動(dòng)機(jī)模型

4 模型驗(yàn)證

在UPPAAL用戶(hù)界面的編輯器中建立ZC切換過(guò)程中各子系統(tǒng)對(duì)應(yīng)的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型并設(shè)置通道，在模擬器中對(duì)切換過(guò)程中出現(xiàn)的ZC1連接ZC2、ZC1申請(qǐng)進(jìn)路、ZC2發(fā)送MA2、Train連接ZC2、Train登錄ZC2、Train注銷(xiāo)ZC1以及Train受控等信息的交互進(jìn)行模擬校驗(yàn)。最后在UPPAAL中，利用BNF語(yǔ)法對(duì)ZC切換過(guò)程的性能和功能要求進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如圖7所示。

圖7 模型驗(yàn)證結(jié)果示意

4.1 系統(tǒng)功能性要求

(1)系統(tǒng)無(wú)死鎖現(xiàn)象：A []not deadlock，驗(yàn)證通過(guò)。

(2)在設(shè)備均正常的情況下，能實(shí)現(xiàn)列車(chē)控制權(quán)由ZC1向ZC2的切換：E <> (Train. Idle imply Train. Controled)，驗(yàn)證通過(guò)。

(3) 當(dāng)列車(chē)越過(guò)ZC切換邊界時(shí)，車(chē)載子系統(tǒng)能實(shí)現(xiàn)登錄ZC2、數(shù)據(jù)庫(kù)版本號(hào)校核以及與ZC1注銷(xiāo)的功能：E <> ((Train. BuildLoginZC2) or (Train. Compaison) or (Train. Loginoff))，驗(yàn)證通過(guò)。

4.2 系統(tǒng)受限活性要求

(1)ZC1計(jì)算MixedMA信息的時(shí)間不超過(guò)T5：A <> ((ZC1. Routecheck imply ZC1. SendMixed MA) and (t

(2)若ZC1未收到ZC2發(fā)送的MA2信息，則無(wú)法計(jì)算出跨越切換邊界的MA信息：A <> (not ZC1. CalculatenewMA) imply ZC1. SendMixedMA，驗(yàn)證不滿(mǎn)足。因?yàn)閆C2范圍內(nèi)的進(jìn)路是經(jīng)ZC2計(jì)算后發(fā)送給ZC的，若無(wú)MA2，ZC1無(wú)法得出MixedMA。

(3)ZC1與ZC2連接時(shí)間不超過(guò)T2：A <> ((ZC2. Buildconn1 imply ZC2. Conn1YES) and (x

(4)車(chē)載子系統(tǒng)與ZC2連接時(shí)間不超過(guò)T3：A <> ((ZC2. BuildconnT imply ZC2. ConnTYES) and (y

(5)車(chē)載系統(tǒng)登錄ZC2的時(shí)間不超過(guò)T4：A <> ((ZC2. Login imply ZC2. LoginYES) and (z

(6)當(dāng)車(chē)載子系統(tǒng)在T5時(shí)間內(nèi)沒(méi)有收到跨越邊界點(diǎn)的MA時(shí)，則認(rèn)為車(chē)地通信系統(tǒng)出現(xiàn)故障，車(chē)載子系統(tǒng)進(jìn)入緊急制動(dòng)狀態(tài)：A <> (Train. Approach and co mmunication==0) imply Train. Emerbreak，驗(yàn)證通過(guò)。

5 結(jié)論

基于通信的列車(chē)運(yùn)行控制系統(tǒng)(CBTC)是一個(gè)結(jié)構(gòu)比較復(fù)雜的實(shí)時(shí)系統(tǒng)，從ZC子系統(tǒng)的實(shí)際出發(fā)，將MSC半形式化方法作為描述ZC切換場(chǎng)景的切入點(diǎn)，然后使用時(shí)間自動(dòng)機(jī)形式化方法對(duì)該切換過(guò)程進(jìn)行描述和驗(yàn)證。首先，建立整個(gè)ZC邊界切換場(chǎng)景中各子系統(tǒng)信息交互的MSC模型，其次，根據(jù)MSC模型的描述，建立時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，最后，采用驗(yàn)證工具UPPAAL對(duì)ZC邊界切換過(guò)程的功能屬性和受限活性進(jìn)行驗(yàn)證。結(jié)果表明：ZC邊界切換功能滿(mǎn)足設(shè)計(jì)要求，在通過(guò)地面分界點(diǎn)P時(shí)，列車(chē)控制權(quán)可以由移交ZC切換至接管ZC。因此，MSC與UPPAAL相結(jié)合的建模驗(yàn)證方法是可行的。

[1] 唐濤，郜春海，黃友能，等.CJ/T407—2012 城市軌道交通基于通信的列車(chē)自動(dòng)控制系統(tǒng)技術(shù)要求[S].北京：中國(guó)標(biāo)準(zhǔn)出版社，2012.

[2] 王露，王長(zhǎng)林.區(qū)域控制器移動(dòng)授權(quán)的統(tǒng)一建模語(yǔ)言(UML)建模與驗(yàn)證[J].城市軌道交通研究，2014(7)：40-43.

[3] 李耀，陳榮武，郭進(jìn)，等.基于TSSM的城市軌道交通CBTC區(qū)域控制器建模與驗(yàn)證[J].西南交通大學(xué)學(xué)報(bào)，2015(2)：27-34.

[4] 車(chē)玉龍，蘇宏升.基于蒙特卡羅的CTCS-3級(jí)列控系統(tǒng)單元重要度分析[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2013(8)：125-128.

[5] 劉金濤，唐濤，趙林，等.基于微分動(dòng)態(tài)邏輯的無(wú)線(xiàn)閉塞中心交接協(xié)議建模與驗(yàn)證[J].中國(guó)鐵道科學(xué)，2013(9)：98-103.

[6] 張友兵，唐濤.基于有色Petri網(wǎng)CTCS-3級(jí)列控系統(tǒng)RBC切換的建模與形式化分析[J].鐵道學(xué)報(bào)，2012(7)：49-53.

[7] 黃友能，張鵬基，侯曉鵬，等.基于混成自動(dòng)機(jī)的城市軌道交通ZC子系統(tǒng)建模與驗(yàn)證方法[J].中國(guó)鐵道科學(xué)，2016(3)：114-120.

[8] Alur R， Etessami K， Yannakakis M. Inference of Message Sequence Charts[J]. IEEE Transaction on Software Engineering，2003，29(7)：623-633.

[9] 周翔，武曉春.基于MSC與UPPAAL的高鐵跨界臨時(shí)限速建模與驗(yàn)證[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2016，60(10)：126-131.

[10] 曹源，唐濤，徐田華，等.形式化方法在列車(chē)運(yùn)行控制系統(tǒng)中的應(yīng)用[J].交通運(yùn)輸工程學(xué)報(bào)，2010(2)：122-123.

[11] 曹源.高速鐵路列車(chē)運(yùn)行控制系統(tǒng)的形式化建模與驗(yàn)證方法研究[D].北京：北京交通大學(xué)，2011.

[12] 萬(wàn)勇兵，徐中偉，梅萌.CTCS-3級(jí)列控系統(tǒng)臨時(shí)限速服務(wù)器建模與形式化驗(yàn)證[J].系統(tǒng)仿真學(xué)報(bào)，2013，25(1)：132-138.

[13] Larsen K G， Mikucionis M， Nielsen B. Online Testing of Real-time System Using UPPAAL[C]∥International Conference on Formal Approaches to Software Testing， 2004，3395：79-94.

[14] 呂繼東，唐濤，燕飛，等.基于UPPAAL的城市軌道交通CBTC區(qū)域控制子系統(tǒng)建模與驗(yàn)證[J].鐵道學(xué)報(bào)，2009，32(3)：59-64.

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