孫維正,曠文珍,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)的建模。
區(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é)束。
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
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
有色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é)束。
有色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)。
根據(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]。
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ì)具有一定的參考意義。