基于MSC與UPPAAL的區域控制器切換場景建模與驗證

楊 璐，陳永剛

(蘭州交通大學自動化與電氣工程學院，蘭州 730070)

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

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

1 ZC切換過程分析

當列車從移交ZC轄區進入接管ZC轄區時，控制列車運行的區域控制器應從移交ZC切換至接管ZC，切換過程分為以下4步。

(1)列車在移交ZC區域內運行，當列車接近分界點P，即列車收到以分界點P為終點的MA時，移交ZC與接管ZC建立通信會話，觸發邊界切換功能，如圖1所示。

圖1 邊界切換觸發控制示意

(2) 如圖2所示，當移交ZC與接管ZC通信成功后，移交ZC計算MA1，同時向接管ZC發送切換預告信息并為列車請求接管ZC范圍內的進路，進路排出以后接管ZC將MA2發送給移交ZC，移交ZC將混合后的MixedMA發送給列車，控制列車運行。

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

(3) 如圖3所示，當列車前端越過分界點P時，車載系統與接管ZC之間建立通信連接，車載系統與接管ZC連接成功以后，車載系統向接管ZC發送登錄申請，接管ZC發送數據庫版本信息，列車向接管ZC發送登錄確認信息后登錄成功。

圖3 車頭越過邊界點時邊界切換控制示意

(4) 如圖4所示，當列車車尾越過分界點P后，列車向接管ZC發送受控申請，向移交ZC發送注銷申請，當列車收到接管ZC發送的控制列車的信息后，移交ZC向列車發送注銷確認信息，列車根據接管ZC發送的控制信息控制列車正常運行，至此，整個邊界切換過程結束。

圖4 車尾越過邊界時邊界切換控制示意

2 ZC切換過程建模

2.1 基于MSC的系統建模

消息順序圖(MSC)是一種簡潔的圖形化描述語言，用來直觀描述并行系統中各部件之間信息交互過程[8]。本文中采用MSC建立ZC切換場景的MSC模型，結合ZC切換過程中可能導致系統出現故障的各種情況，為后續時間自動機模型的建立提供依據。

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

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

(2)M={MTrain，MZC1，MZC2}分別表示與車載子系統、移交ZC子系統及接管ZC子系統相關的消息集，其中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映射到實數集I上的函數，如f(MAextendreq)=ITrain，t(MAexte-ndreq)=IZC1。發送消息事件m用!m表示，接收消息事件m用？m表示，如：消息事件MAextendreq從Train子系統發送至ZC1子系統表示為，ZC1子系統接受從Train子系統發來的MAextendreq消息表示為。≤i表示實體i發生的事件對應到時間軸上的先后順序，如對于實體Train上發生的兩個事件MAextendreq和MixedMA，事件MAextendreq先于事件MixedMA發生。 ≤io表示對于任意一個消息事件，事件的發送先于接收發生，即?m，!m≤io？m；如對于消息事件MAextendreq，Train子系統發送MAextendreq消息事件先于ZC1子系統接收MAextendreq消息事件發生。

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

圖5 ZC邊界切換過程MSC模型

2.2 模型描述

ZC切換過程中涉及的信息交互的對象有車載子系統(Train)，移交區域控制子系統(ZC1)，接管區域控制子系統(ZC2)。

(1)接近邊界點(授權的終點為分界點)：列車在ZC1區域運行過程中，若某時刻Train收到了以邊界點P為終點的移動授權，Train向ZC1發送授權延伸申請消息MAextendreq，然后ZC1向ZC2發送與ZC2建立通信連接的請求消息Connect2，ZC2向ZC1發送連接確認消息Conf2，相鄰ZC間建立通信過程完成。ZC1向ZC2發送切換預告信息YG，并為列車申請ZC2范圍內的進路，當聯鎖系統排出進路以后，ZC2將進路信息MA2發給ZC1，由ZC1將ZC1范圍內進路信息與之混合后將新的授權信息MixedMA發送給列車，控制列車運行，如果在T5(5s)內Train沒有收到MixedMA信息，則出現車地通信故障，實施緊急制動。

(2)車頭越過邊界點P：當列車車頭越過邊界點P后，Train收到切換執行應答器組(LTO)發送的執行轉換消息，Train根據之前MixedMA中ZC2的信息，向ZC2發送與ZC2建立通信連接的請求消息ConnectZC2，ZC2向Train發送連接確認消息Conf4，連接ZC2成功后，Train向ZC2發送登錄申請消息LoginZC2，ZC2將本身系統的版本號信息發送給Train，若版本號信息相同則Train向ZC2發送登錄確認消息Conf5，否則Train系統從數據庫存儲單元(DSU)重新下載。

(3)車尾通過邊界點P：當列車車尾越過邊界點P后，Train向ZC2發送受控申請消息Reqcontrol，并向ZC1發送注銷消息Cancel，當列車收到ZC2的控制消息ControlT后，ZC1向Train發送注銷確認消息ACKcancel，整個切換過程結束，此后Train子系統在ZC2的控制下繼續正常運行。

3 系統模型仿真

3.1 驗證工具UPPAAL

時間自動機是在自動機理論基礎上擴展的基于時間周期、時間約束和時間解釋的實時系統建模方法[9]，相較于CPN、SPN及CSP，其主要優勢在于有驗證工具為其提供建模、仿真和驗證環境[10]。UPPAAL通過模擬有限個控制結構和數值時鐘來驗證系統的安全性和受限活性[11-13]。

UPPAAL用戶界面的編輯器、模擬器和驗證器分別用于實時系統的建模、仿真和驗證。模擬器不僅可以按狀態轉移檢查狀態的轉移是否是期望的結果，當系統出現鎖死時，還可以檢查到出現鎖死的部位繼而對模型進行修正。驗證器通過對狀態空間的搜索來驗證系統的功能屬性和受限活性。UPPAAL專門為模型的驗證提供了一種BNF語法[14-15]。具體語法含義如表1所示。

表1 BNF語法的含義

3.2 ZC切換過程模型

對于ZC切換過程的MSC模型僅僅直觀描述了時間的進程，卻無法對模型進行有效的分析和驗證，所以需要將MSC模型描述的ZC切換過程轉換成時間自動機模型，然后用UPPAAL工具對其進行驗證。文中對ZC切換過程中涉及信息交互的3個活動對象分別建立各自的子時間自動機模型，即TATrain、TAZC1、TAZC2。ZC切換過程是這3個自時間自動機的積，即TA=TATrain||TAZC1||TAZC2。

圖6為ZC切換過程的時間自動機網絡模型。其中，以“!”為結尾的消息表示該條消息發出以后子系統位置發生轉換，以“？”為結尾的消息表示收到該條消息后子系統位置發生轉換，以此保證各子系統模型之間同一轉換的同步發生。x、y、z和t為時鐘約束，用于判斷ZC1與ZC2的連接時間、Train與ZC2的連接時間、Train登錄ZC2的時間以及ZC1計算MixedMA的時間是否超時。 routeorder、same和co mmunication為標志位，用于統一不同子系統間狀態遷移的同步性。

圖6 ZC邊界切換時間自動機模型

4 模型驗證

在UPPAAL用戶界面的編輯器中建立ZC切換過程中各子系統對應的時間自動機網絡模型并設置通道，在模擬器中對切換過程中出現的ZC1連接ZC2、ZC1申請進路、ZC2發送MA2、Train連接ZC2、Train登錄ZC2、Train注銷ZC1以及Train受控等信息的交互進行模擬校驗。最后在UPPAAL中，利用BNF語法對ZC切換過程的性能和功能要求進行驗證，驗證結果如圖7所示。

圖7 模型驗證結果示意

4.1 系統功能性要求

(1)系統無死鎖現象：A []not deadlock，驗證通過。

(2)在設備均正常的情況下，能實現列車控制權由ZC1向ZC2的切換：E <> (Train. Idle imply Train. Controled)，驗證通過。

(3) 當列車越過ZC切換邊界時，車載子系統能實現登錄ZC2、數據庫版本號校核以及與ZC1注銷的功能：E <> ((Train. BuildLoginZC2) or (Train. Compaison) or (Train. Loginoff))，驗證通過。

4.2 系統受限活性要求

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

(2)若ZC1未收到ZC2發送的MA2信息，則無法計算出跨越切換邊界的MA信息：A <> (not ZC1. CalculatenewMA) imply ZC1. SendMixedMA，驗證不滿足。因為ZC2范圍內的進路是經ZC2計算后發送給ZC的，若無MA2，ZC1無法得出MixedMA。

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

(4)車載子系統與ZC2連接時間不超過T3：A <> ((ZC2. BuildconnT imply ZC2. ConnTYES) and (y

(5)車載系統登錄ZC2的時間不超過T4：A <> ((ZC2. Login imply ZC2. LoginYES) and (z

(6)當車載子系統在T5時間內沒有收到跨越邊界點的MA時，則認為車地通信系統出現故障，車載子系統進入緊急制動狀態：A <> (Train. Approach and co mmunication==0) imply Train. Emerbreak，驗證通過。

5 結論

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

[1] 唐濤，郜春海，黃友能，等.CJ/T407—2012 城市軌道交通基于通信的列車自動控制系統技術要求[S].北京：中國標準出版社，2012.

[2] 王露，王長林.區域控制器移動授權的統一建模語言(UML)建模與驗證[J].城市軌道交通研究，2014(7)：40-43.

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

[4] 車玉龍，蘇宏升.基于蒙特卡羅的CTCS-3級列控系統單元重要度分析[J].鐵道標準設計，2013(8)：125-128.

[5] 劉金濤，唐濤，趙林，等.基于微分動態邏輯的無線閉塞中心交接協議建模與驗證[J].中國鐵道科學，2013(9)：98-103.

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

[7] 黃友能，張鵬基，侯曉鵬，等.基于混成自動機的城市軌道交通ZC子系統建模與驗證方法[J].中國鐵道科學，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的高鐵跨界臨時限速建模與驗證[J].鐵道標準設計，2016，60(10)：126-131.

[10] 曹源，唐濤，徐田華，等.形式化方法在列車運行控制系統中的應用[J].交通運輸工程學報，2010(2)：122-123.

[11] 曹源.高速鐵路列車運行控制系統的形式化建模與驗證方法研究[D].北京：北京交通大學，2011.

[12] 萬勇兵，徐中偉，梅萌.CTCS-3級列控系統臨時限速服務器建模與形式化驗證[J].系統仿真學報，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區域控制子系統建模與驗證[J].鐵道學報，2009，32(3)：59-64.

[15] 康仁偉.基于時間自動機的CTCS-3級列控系統建模方法與研究[D].北京：北京交通大學，2013：40-53.