基于混成自動機的城市軌道交通ZC子系統建模與驗證方法

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

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

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

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

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

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

1　功能場景建模方法

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

1.1　UML順序圖擴展

為了能夠表達ZC子系統的混成特性，需要對UML順序圖進行擴展[7]。將順序圖中的消息發送和消息接收采用事件表示，利用標記值和約束的擴展方式，對順序圖進行了以下2個方面的擴展。

1)對時間的擴展

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

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

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

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

2)對連續變量的擴展

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

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

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

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

圖1　UML擴展內容展示

1.2　線性混成自動機定義

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

定義1

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

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

其中各個參數的含義如下。

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

Y：動作名有限集合。

V：位置節點的有限集合。

V0：初始位置節點集合。

1.3　模型轉換的定義、規則和步驟

1.3.1模型轉換的定義

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

定義1：

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

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

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

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

定義2：

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

其中各參數的含義如下。

I：對象的有限集合。

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

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

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

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

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

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

J：消息賦值集合。

1.3.2模型轉換的規則

1)單元片段轉換規則

將單元片段進行轉換，得到目標單元自動機A(N,n0,L)。

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

其中各參數的含義如下。

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

n0：集合N的1個空狀態。在每個單元片段上都建立1個空狀態，以便后期的組合優化。

L：目標單元自動機事件集合，L={l′,g,m,a,l}，與混成自動機轉換關系集合E相對應，其中l′和l為自動機的2個節點對應于UML中可視事件對，且l′,l∈N；g為遷移條件，即進行狀態跳變時變量需要滿足的條件，是UML圖中接收發送消息需要滿足的時間或變量條件的擴展；m為動作集合，對應于UML圖中消息的發送與接收；a為動作過程中賦值更新的集合，對應于UML圖中動作的時間重置與變量賦值更新擴展。

2)組合片段轉換規則

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

定義函數Alt(g,AF)， 其中g為對應可選分支的門條件，AF為所有可選片段的集合， 則可按照以下規則得到自動機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為節點集合N的子集合；guard1和guard2為所要滿足條件集合guard中的子條件；n1,0和n2,0為集合N的另外2個空狀態；L1和L2為有限集合L的子集合。

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

圖2　組合片段Alt轉換規則示意圖

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

定義選擇片段函數Opt(OF),其中OF為單分支選擇片段變量，可按照以下規則得到自動機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的轉換規則示意圖。

圖3　組合片段Opt轉換規則示意圖

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

設函數Loop(LF,guard), 其中LF為所要不斷重復的子片段，guard為所要滿足的條件， 則可按照以下規則得到自動機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個新的空狀態；e為自然數。

圖4是1個組合片段loop轉化規則示意圖，圖中A1為需要循環片段構造的子自動機。

圖4　組合片段Loop轉換規則示意圖

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

設函數Combin(CF), 其中CF為所有的組合片段，guard為所要滿足的條件，則可按照以下規則得到自動機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的另外的空狀態，i和e均為自然數。

1.3.3模型轉換的步驟

在得到1個擴展的UML順序圖之后，經過以下4步將其轉換為目標線性混成自動機。

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

Step2：根據單元片段轉換規則，將單元片段轉換為目標單元自動機。

Step3：根據組合片段轉換規則，將1個組合片段對應的多個單元片段都轉換成目標單元自動機，然后再組合成該組合片段對應的線性混成自動機。

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

2　ZC子系統建模與驗證案例

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

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

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

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

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

圖5　ZC邊界切換觸發控制圖

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

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

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

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

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

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

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

首先定義參數，見表1。

表1　參數定義表

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

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

2.3　驗證及結果分析

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

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

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

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

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

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

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

表2　功能性質驗證

表3　安全性質驗證

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

3　結　論

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

[1]唐濤,郜春海,黃友能，等. CJ/T 407—2012 城市軌道交通基于通信的列車自動控制系統技術要求[S].北京:中國標準出版社，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]劉金濤,唐濤,趙林，等. 基于微分動態邏輯的無線閉塞中心交接協議建模與驗證[J].中國鐵道科學,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]杜軍威, 徐中偉, 王樹梅. 聯鎖邏輯模型的安全性分析[J].計算機工程與應用,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]呂繼東. 列車運行控制系統分層形式化建模與驗證分析[D]. 北京：北京交通大學, 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.