黃友能，張鵬基，侯曉鵬，唐　濤

(1.北京交通大學(xué) 電子信息工程學(xué)院，北京　100044；2.北京交通大學(xué) 軌道交通運行控制系統(tǒng)國家工程研究中心，北京　100044)

基于通信的列車控制系統(tǒng)(Communication Based Train Control,CBTC)是保證城市軌道交通列車安全、高效運行的系統(tǒng)，其區(qū)域控制器(Zone Controller,ZC)子系統(tǒng)主要實現(xiàn)為管轄范圍內(nèi)列車計算移動授權(quán)(Movement Authority,MA)、區(qū)域控制器邊界切換等功能[1]，這些功能的安全性是保障行車安全的基礎(chǔ)，因此針對ZC子系統(tǒng)功能的安全驗證就顯得尤為重要。

ZC子系統(tǒng)主要通過無線傳輸方式接收車載子系(Vital OnBoard Computer,VOBC)的信息，因此在車地通信過程中不可避免會出現(xiàn)信號延遲或發(fā)送失敗等情況，同時，由于ZC子系統(tǒng)在同一時間段內(nèi)會與管轄范圍內(nèi)的所有列車進(jìn)行交互，因此要求該系統(tǒng)應(yīng)具有較強(qiáng)的并發(fā)性與實時性。另外，ZC子系統(tǒng)在計算移動授權(quán)的過程中，需要考慮列車連續(xù)變化參數(shù)(距離、速度和加速度等)的演化過程，以及設(shè)備交互的一些離散事件，具有明顯的混成特性[2]。

關(guān)于列車控制系統(tǒng)安全驗證的既有研究工作，有的針對系統(tǒng)的并發(fā)性與實時性進(jìn)行建模與驗證，如同濟(jì)大學(xué)的徐中偉教授等利用Petri網(wǎng)模型和故障樹實現(xiàn)了對聯(lián)鎖軟件的安全性評估等[3]，但缺少相應(yīng)的驗證環(huán)節(jié)。有的針對系統(tǒng)混成特性進(jìn)行研究，如北京交通大學(xué)的呂繼東博士利用混合通信進(jìn)程對系統(tǒng)進(jìn)行建模仿真，但缺少相應(yīng)的驗證軟件[4]。北京交通大學(xué)的劉金濤博士利用動態(tài)微分邏輯形式化語言對CTCS-3級列車控制系統(tǒng)進(jìn)行了仿真與驗證，但驗證過程需要大量的推導(dǎo)公式，效率和重用性都較低。

本文基于形式化建模驗證理論[5-6]，結(jié)合統(tǒng)一建模語言(Unified Modelling Language,UML)的交互流程描述能力和自定義擴(kuò)展能力，針對ZC子系統(tǒng)的混成特性，建立ZC子系統(tǒng)的UML順序圖；采用模型轉(zhuǎn)換方法，定義從源模型到目標(biāo)模型的轉(zhuǎn)換規(guī)則，將ZC子系統(tǒng)的UML順序圖轉(zhuǎn)換為線性混成自動機(jī)模型，用于ZC子系統(tǒng)功能的安全驗證；以實際的ZC子系統(tǒng)邊界切換控制功能場景為例，根據(jù)建立的ZC子系統(tǒng)線性混成自動機(jī)模型，采用形式化工具BACH(Bounded reachability checker)對該場景的7條功能性質(zhì)和4條安全性質(zhì)進(jìn)行驗證。

1　功能場景建模方法

針對ZC子系統(tǒng)具有連續(xù)變量(距離、速度和加速度等)的動態(tài)特性，首先采用UML順序圖描述系統(tǒng)的實時交互特性，然后利用UML的標(biāo)記值和約束的擴(kuò)展方式對順序圖進(jìn)行擴(kuò)展，給出模型轉(zhuǎn)換的定義及規(guī)則，使源模型與目標(biāo)模型的語義相同，將順序圖轉(zhuǎn)換為線性混成自動機(jī)模型。

1.1　UML順序圖擴(kuò)展

為了能夠表達(dá)ZC子系統(tǒng)的混成特性，需要對UML順序圖進(jìn)行擴(kuò)展[7]。將順序圖中的消息發(fā)送和消息接收采用事件表示，利用標(biāo)記值和約束的擴(kuò)展方式，對順序圖進(jìn)行了以下2個方面的擴(kuò)展。

1)對時間的擴(kuò)展

(1)事件上添加時鐘及其約束(可有多個時鐘)，即本事件在什么時間范圍內(nèi)發(fā)生；

(2)事件上添加時鐘變化率恒為1(以1 ms為時間單位長度)；

(3)動作的時間約束，即只有滿足時間約束時動作才會發(fā)生；

(4)動作的時鐘重置，即動作完成時要進(jìn)行時鐘重置。

2)對連續(xù)變量的擴(kuò)展

(1)事件上添加變量的約束(可有多個變量)，即本事件發(fā)生時變量的變化范圍；

(2)事件上添加變量的變化率(可為實數(shù)范圍如[0.9，1.1])；

(3)動作的變量約束，即只有滿足變量約束時動作才會發(fā)生；

(4)動作的變量賦值，即動作完成時要進(jìn)行的變量賦值。

圖1　UML擴(kuò)展內(nèi)容展示

1.2　線性混成自動機(jī)定義

以Alur提出的定義框架為基準(zhǔn)[8]，對線性混成自動機(jī)作如下定義。

定義1

線性混成自動機(jī)(Linear Hybrid Automata)形式為

H：(X,Y,V,E,V0,fflow,iinv,iinit)

其中各個參數(shù)的含義如下。

X:實數(shù)值系統(tǒng)變量的有限集合，X={x1,x2,…,xn}，其中n為變量的個數(shù)，也被稱為自動機(jī)的維度(dimension)。

Y：動作名有限集合。

V：位置節(jié)點的有限集合。

V0：初始位置節(jié)點集合。

1.3　模型轉(zhuǎn)換的定義、規(guī)則和步驟

1.3.1模型轉(zhuǎn)換的定義

UML順序圖定義了多種類型的交互片段，這些交互片段組成了UML順序圖的不同生命線即對象間的活動。本文在此基礎(chǔ)上增加定義了單元片段，用于刻畫比較簡單的消息傳遞過程。按照該定義，交互片段也可看作是由眾多單元片段按照一定規(guī)則組合而成的。

定義1：

單元片段語義表示為1個或多個可視的事件序列，每個單元片段由相應(yīng)的單個或多個事件序列組成。事件e1和e2間的關(guān)系應(yīng)當(dāng)滿足以下3種關(guān)系之一。

(1)在初始事件中，e1為消息發(fā)送事件，則e2為相對應(yīng)的消息接收事件。

(2)若在同一實例的生命線上，事件e1出現(xiàn)在e2之前，則e1是消息發(fā)送事件；并且事件e1和e2可作為可視對(e1，e2)。

(3)若在同一實例的生命線上，事件e1出現(xiàn)在事件e2之后，則e2是消息發(fā)送事件。

定義2：

1個單元片段是1個8元數(shù)據(jù)組，可表示為UF(I,W,M,Z,B,C,G,J)。

其中各參數(shù)的含義如下。

I：對象的有限集合。

W：事件的有限集合，W*為包括空事件串在內(nèi)的所有不重復(fù)事件串集合，p為事件串集合，?p∈H*，|p|為p的字符個數(shù)，p(n)為p中的第n個事件，2個事件用“.”連接。

M：有窮的動作集合，包括消息的接收與發(fā)送。

Z：可視對事件集合，Z={e，e′}代表1個可視對。

B：事件約束集合(包括時間與變量)。

C：事件間約束集合(包括時間與變量)。

G：事件標(biāo)簽值集合(時間與變量的變化率)。

J：消息賦值集合。

1.3.2模型轉(zhuǎn)換的規(guī)則

1)單元片段轉(zhuǎn)換規(guī)則

將單元片段進(jìn)行轉(zhuǎn)換，得到目標(biāo)單元自動機(jī)A(N,n0,L)。

UF(I,W,M,Z,B,C,G,J)→A(N,n0,L)

其中各參數(shù)的含義如下。

N：節(jié)點集合，N={p,d,r}，其中，p∈W*，并且對于∶?j

n0：集合N的1個空狀態(tài)。在每個單元片段上都建立1個空狀態(tài)，以便后期的組合優(yōu)化。

L：目標(biāo)單元自動機(jī)事件集合，L={l′,g,m,a,l}，與混成自動機(jī)轉(zhuǎn)換關(guān)系集合E相對應(yīng)，其中l(wèi)′和l為自動機(jī)的2個節(jié)點對應(yīng)于UML中可視事件對，且l′,l∈N；g為遷移條件，即進(jìn)行狀態(tài)跳變時變量需要滿足的條件，是UML圖中接收發(fā)送消息需要滿足的時間或變量條件的擴(kuò)展；m為動作集合，對應(yīng)于UML圖中消息的發(fā)送與接收；a為動作過程中賦值更新的集合，對應(yīng)于UML圖中動作的時間重置與變量賦值更新擴(kuò)展。

2)組合片段轉(zhuǎn)換規(guī)則

規(guī)則1：在1個多分支交互片段“Alt”中有q個互斥的可選分支，每個分支上都有執(zhí)行該分支的“使能”條件，只有條件為真的分支才被執(zhí)行，每個分支是1個單元片段或者組合片段。

定義函數(shù)Alt(g,AF)， 其中g(shù)為對應(yīng)可選分支的門條件，AF為所有可選片段的集合， 則可按照以下規(guī)則得到自動機(jī)AAlt(N,n0,L)。

Alt(g,AF)→AAlt(N,n0,L)

其中

N={n0}∪N1∪N2…

L={〈n0,ε,guard1,ε,n1,0〉，〈n0,ε,guard2,ε,n2,0〉}…∪L1∪L2…

式中：N1和N2為節(jié)點集合N的子集合；guard1和guard2為所要滿足條件集合guard中的子條件；n1,0和n2,0為集合N的另外2個空狀態(tài)；L1和L2為有限集合L的子集合。

圖2為有2種選擇的Alt組合片段轉(zhuǎn)換規(guī)則示意圖，圖中A，B，C為組合片段的組合對象；A1和A2為子自動機(jī)。

圖2　組合片段Alt轉(zhuǎn)換規(guī)則示意圖

規(guī)則2： 1個組合片段Opt是1種單選擇行為，這種單選擇行為類似于Alt組合片段中的某種行為。

定義選擇片段函數(shù)Opt(OF),其中OF為單分支選擇片段變量，可按照以下規(guī)則得到自動機(jī)AOpt(N,n0,L)。

Opt(OF)→AOpt(N,n0,L)

其中

L={〈n0,ε,guard1,ε,n1,0〉,〈n0,ε,else,ε,

n2,0〉}∪L1∪L2

式中：else為除guard外需要滿足的其他條件。

圖3為1個組合片段Opt的轉(zhuǎn)換規(guī)則示意圖。

圖3　組合片段Opt轉(zhuǎn)換規(guī)則示意圖

規(guī)則3：1個組合片段Loop表示1種循環(huán)行為，組合片段中的子片段會被不斷重復(fù)直到不滿足條件為止。

設(shè)函數(shù)Loop(LF,guard), 其中LF為所要不斷重復(fù)的子片段，guard為所要滿足的條件， 則可按照以下規(guī)則得到自動機(jī)ALoop(N,n0,L)。

Loop(LF,guard)→ALoop(N,n0,L)

其中

N={n0，ne}∪N1

L={〈n0,ε,guard,ε,n1,0〉，〈n0,ε,！guard,ε,ne〉}∪L1

式中：ne為集合N的1個新的空狀態(tài)；e為自然數(shù)。

圖4是1個組合片段loop轉(zhuǎn)化規(guī)則示意圖，圖中A1為需要循環(huán)片段構(gòu)造的子自動機(jī)。

圖4　組合片段Loop轉(zhuǎn)換規(guī)則示意圖

規(guī)則4：多個組合片段可組成1個完整的自動機(jī)，組合片段按照生命線由上到下的順序執(zhí)行。

設(shè)函數(shù)Combin(CF), 其中CF為所有的組合片段，guard為所要滿足的條件，則可按照以下規(guī)則得到自動機(jī)ACombin(N,n0,L)。

Combin(CF)→ACombin(N,n0,L)

其中，

N=N1∪N2…

n0=n1,0

L={〈ni,e,ε,ε,ε,ni+1,0〉}∪L1∪L2

(1≤i≤m-1)

式中：ni,e為集合N的另外的空狀態(tài)，i和e均為自然數(shù)。

1.3.3模型轉(zhuǎn)換的步驟

在得到1個擴(kuò)展的UML順序圖之后，經(jīng)過以下4步將其轉(zhuǎn)換為目標(biāo)線性混成自動機(jī)。

Step1：將擴(kuò)展后的UML順序圖根據(jù)時間先后順序拆分為不同組合片段，由于組合片段內(nèi)可能會嵌套著其他組合片段和單元片段，需要將組合片段繼續(xù)拆分，直至將整個順序圖拆分為單元片段。

Step2：根據(jù)單元片段轉(zhuǎn)換規(guī)則，將單元片段轉(zhuǎn)換為目標(biāo)單元自動機(jī)。

Step3：根據(jù)組合片段轉(zhuǎn)換規(guī)則，將1個組合片段對應(yīng)的多個單元片段都轉(zhuǎn)換成目標(biāo)單元自動機(jī)，然后再組合成該組合片段對應(yīng)的線性混成自動機(jī)。

Step4:根據(jù)拆分組合片段時的順序，將不同組合片段的線性混成自動機(jī)合成為完整的目標(biāo)線性混成自動機(jī)模型。

2　ZC子系統(tǒng)建模與驗證案例

針對CBTC系統(tǒng)的混成特性，根據(jù)北京地鐵亦莊線ZC邊界切換工程數(shù)據(jù)選取列車在小紅門ZC與亦莊橋ZC邊界切換控制功能場景進(jìn)行具體建模與驗證。ZC通信周期為400ms，VOBC通信周期為200 ms。

2.1　ZC邊界切換控制功能場景分析

當(dāng)列車從1個ZC管轄區(qū)域進(jìn)入另一個ZC管轄區(qū)域時，ZC將根據(jù)移交ZC發(fā)送的移動MA判斷列車是否已經(jīng)運行到地面區(qū)域分界點，如果已經(jīng)到達(dá)地面區(qū)域分界點，則由移交ZC向接管ZC發(fā)出移交列車申請，此后由這2個ZC分別計算列車在各自管轄范圍內(nèi)的MA，并由當(dāng)前控制列車ZC負(fù)責(zé)將這2部分MA信息混合后發(fā)送給列車。在車地通信正常的情況下，列車將接收到MA，并根據(jù)移動授權(quán)計算速度曲線；如列車在5 s內(nèi)仍接收不到新的MA，將認(rèn)為在ZC切換過程中發(fā)生了車地通信故障，列車將觸發(fā)緊急制動，使列車在車地通信故障前接收到的移動授權(quán)終點前停車。

列車從小紅門ZC管轄區(qū)域進(jìn)入亦莊橋ZC管轄區(qū)域時，越區(qū)切換的具體過程可以分為以下5個階段。

階段1：如圖5所示，列車在小紅門ZC區(qū)域內(nèi)運行，當(dāng)MA終點為小紅門ZC區(qū)域與亦莊橋ZC區(qū)域邊界點JZ9時，此時小紅門ZC(移交ZC)將與亦莊橋ZC(接管ZC)通信，觸發(fā)邊界切換控制功能。

圖5　ZC邊界切換觸發(fā)控制圖

階段2：在車地通信正常的情況下，如圖6所示，隨著列車的運行，移交ZC為列車計算移動授權(quán)MA1，接管ZC為列車計算移動授權(quán)MA2，由于此時列車仍受到移交ZC控制，移交ZC將MA1和MA2的信息混合后向列車發(fā)送“終點至H點”的移動授權(quán)。

圖6　車地通信正常情況下ZC邊界切換控制圖

階段3：當(dāng)列車車頭位置越過ZC邊界JZ9時，此時移交ZC為列車計算移動授權(quán)MA1，接管ZC為列車計算移動授權(quán)MA2，列車受接管ZC的控制，由接管ZC將MA1和MA2的信息混合后向列車發(fā)送“終點至H點”的移動授權(quán)。

階段4：在列車車尾越過ZC邊界JZ9時，將向移交ZC發(fā)送注銷申請，并根據(jù)接管ZC發(fā)送的移動授權(quán)完成行車作業(yè)。假如列車車尾在越過ZC邊界JZ9時前方有障礙物等情況，則計算安全制動曲線并根據(jù)曲線完成停車過程。

階段5：在車地通信故障的情況下，如圖7所示，列車將觸發(fā)緊急制動，列車在H點前停車。

圖7　車地通信故障情況下ZC邊界切換控制圖

2.2　ZC邊界切換控制功能場景建模

首先定義參數(shù)，見表1。

表1　參數(shù)定義表

針對ZC邊界切換控制功能場景，采用擴(kuò)展的UML順序圖，建立ZC邊界切換控制功能場景的UML順序圖；根據(jù)車地通信的5個階段，將建立的UML順序圖分為5個組合片段；以其中1個組合片段1為例，其UML順序圖如圖8所示。

根據(jù)模型轉(zhuǎn)換的定義和規(guī)則，將圖8所示的UML順序圖轉(zhuǎn)換為單元自動機(jī)；將所有的單元自動機(jī)根據(jù)轉(zhuǎn)換的先后順序組合成線性混成自動機(jī)模型，如圖9所示。

2.3　驗證及結(jié)果分析

本文利用線性混成自動機(jī)的形式化驗證軟件BACH對該場景的功能性質(zhì)和安全性質(zhì)進(jìn)行驗證。BACH是南京大學(xué)設(shè)計開發(fā)的面向線性混成系統(tǒng)有界可達(dá)性的模型驗證軟件，它將BMC思想擴(kuò)展到了線性混成自動機(jī)的可達(dá)性檢驗工作中。該工具主要檢驗功能有：單元自動機(jī)面向路徑可達(dá)性驗證；單自動機(jī)有界可達(dá)性驗證；自動機(jī)組系統(tǒng)面向路徑組可達(dá)性驗證；自動機(jī)組系統(tǒng)有界可達(dá)性驗證。本文主要運用后2種驗證功能。

根據(jù)圖9所示的ZC邊界切換控制功能線性混成自動機(jī)模型，采用BACH模型驗證軟件提供的可以針對每個成員自動機(jī)分別建立模型的功能，分別建立該具體場景下VOBC，移交ZC和接管ZC的線性混成自動機(jī)模型，如圖10所示。

圖8　ZC邊界切換控制功能場景部分UML順序圖

圖9　ZC邊界切換控制功能場景線性混成自動機(jī)模型

圖10　VOBC，移交ZC和接管ZC的線性混成自動機(jī)模型

通過BACH軟件中檢測模塊CLHA Checker對場景模型進(jìn)行功能性驗證。利用檢測模塊CLHA Checker中的Path-Oriented Reachability選項先對模型中自動機(jī)組的路徑可達(dá)性進(jìn)行檢測，然后針對ZC子系統(tǒng)邊界切換場景的7條功能性質(zhì)進(jìn)行驗證。檢測路徑及驗證結(jié)果如表2所示。

利用檢測模塊CLHA Checker中的Bounded Reachability選項對自動機(jī)組的有界可達(dá)性進(jìn)行檢測。在有界可達(dá)性的檢測過程中加入各個對象的線性混成自動機(jī)編碼文本。為了驗證列車安全性能，在VOBC線性混成自動機(jī)模型中加入減速狀態(tài)和超速狀態(tài)，選擇終點目標(biāo)節(jié)點，然后根據(jù)目標(biāo)節(jié)點選擇待可達(dá)性的檢查節(jié)點進(jìn)行有界可達(dá)性檢測。檢測完成后再針對4條安全性質(zhì)進(jìn)行驗證，安全性質(zhì)及驗證結(jié)果見表3。

表2　功能性質(zhì)驗證

表3　安全性質(zhì)驗證

在考慮了ZC邊界切換控制中車地通信正常以及故障2種情況的基礎(chǔ)上，通過表2中的7條路徑可達(dá)性性質(zhì)驗證可以看出，ZC邊界切換控制功能符合設(shè)計要求；通過表3中4條有界可達(dá)性安全性質(zhì)驗證可以看出，在ZC邊界切換控制功能場景下，列車能夠安全通過地面區(qū)域邊界點，也沒有超速情況，且能夠在接管ZC管轄范圍內(nèi)安全停車。但由于本案例在設(shè)計之初將障礙物的位置設(shè)置的距離邊界點較近，使得在ZC切換過程中，列車尚未完全通過邊界點就開始降速停車了。在將障礙物位置后移之后，通過檢測發(fā)現(xiàn)減速狀態(tài)可達(dá)，說明列車能夠安全通過地面區(qū)域邊界點且無降速，符合安全需求。

3　結(jié)　論

本文針對ZC子系統(tǒng)具有混成性的特點，利用擴(kuò)展后的UML順序圖對ZC子系統(tǒng)進(jìn)行建模；采用模型轉(zhuǎn)換方法，定義從源模型到目標(biāo)模型的轉(zhuǎn)換規(guī)則，將ZC子系統(tǒng)的UML順序圖模型轉(zhuǎn)換為形式化的線性混成自動機(jī)模型，用于ZC子系統(tǒng)功能的安全驗證。以北京地鐵亦莊線ZC邊界切換控制功能場景為例，建立該場景的UML順序圖；將其對應(yīng)車地通信的5個階段細(xì)分為5個組合片段；根據(jù)模型轉(zhuǎn)換定義及規(guī)則，進(jìn)一步將各組合片段拆分為單元片段，將1個組合片段對應(yīng)的多個單元片段轉(zhuǎn)換成目標(biāo)單元自動機(jī)后，再合成該組合片段對應(yīng)的線性混成自動機(jī)；根據(jù)拆分組合片段時的順序，將不同組合片段的線性混成自動機(jī)合成為完整的目標(biāo)線性混成自動機(jī)模型。根據(jù)建立的線性混成自動機(jī)模型，采用驗證工具BACH對該場景的7條功能性質(zhì)和4條安全性質(zhì)進(jìn)行驗證。結(jié)果表明：ZC邊界切換控制功能滿足設(shè)計要求，列車能夠安全通過地面區(qū)域邊界點，沒有超速情況且能夠在接管ZC管轄范圍內(nèi)安全停車。表明所提出的建模和驗證方法是可行的，彌補(bǔ)了對具有混成特性列車控制系統(tǒng)既有驗證方法的不足。

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

(TANG Tao,GAO Chunhai, HUANG Youneng,et al. CJ/T 407—2012 Technical Requirement of Communication Based Automatic Train Control System for Urban Rail Transit[S].Beijing:China Standard Press,2012.in Chinese)

[2]劉金濤,唐濤,趙林，等. 基于微分動態(tài)邏輯的無線閉塞中心交接協(xié)議建模與驗證[J].中國鐵道科學(xué),2012,33(5)：98-104.

(LIU Jintao,TANG Tao，ZHAO Lin,et al. Modeling and Verification of Radio Block Center Handover Protocol Based on Differential Dynamic Logic[J]. China Railway Science,2012,33(5)：98-104.in Chinese)

[3]杜軍威, 徐中偉, 王樹梅. 聯(lián)鎖邏輯模型的安全性分析[J].計算機(jī)工程與應(yīng)用,2007,43(2)：1-4.

(DU Junwei, XU Zhongwei,WANG Shumei. Safety Analysis of Interlocking Logic Model[J]. Computer Engineering and Applications, 2007,43(2)：1-4.in Chinese)

[4]呂繼東. 列車運行控制系統(tǒng)分層形式化建模與驗證分析[D]. 北京：北京交通大學(xué), 2011.

(Lü Jidong, Hierarchical Formal Modeling and Verification Train Control System[D].Beijing：Beijing Jiaotong University,2011.in Chinese)

[5]PLATZER A′e,QUESEL Jan-David. European Train Control System: a Case Study in Formal Verification[J]. Lecture Notes in Computer Science,2009,5885:246-265.

[6]WERNER Damm, ALFRED Mikschl, JENS Oehlerking, et al. Automating Verification of Cooperation, Control and Design in Traffic Applications[J]. Lecture Notes in Computer Science,2007,4770:115-169.

[7]ONJECT Management Group. Unified Modeling Language:Super Structure[EB/OL].2013-07-30[2015-04-15]. http://www.omg.org.

[8]ALURA R，COURCOUBETIS C，HALBWACHS N，et al.The Algorithmic Analysis of Hybrid Systems[J]. Theoretical Computer Science, 1995, 138(94):3-34.