移動授權的形式化建模與驗證

賀歡歡，陳永剛，羅雅允，張彩珍

(1.蘭州交通大學自動化與電氣工程學院，蘭州 730070;2.蘭州交通大學電子與信息工程學院，蘭州 730070)

移動授權的形式化建模與驗證

賀歡歡1，陳永剛1，羅雅允1，張彩珍2

(1.蘭州交通大學自動化與電氣工程學院，蘭州 730070;2.蘭州交通大學電子與信息工程學院，蘭州 730070)

基于通信的列車運行控制系統(tǒng)(Communications-Based Train Control System， CBTC)相較于傳統(tǒng)的基于軌道的列車運行控制系統(tǒng)，無論是從功能方面還是性能方面都有了很大的改進。在系統(tǒng)的研發(fā)過程中，對其進行建模和驗證，能夠發(fā)現系統(tǒng)設計的缺陷，進而保證系統(tǒng)的安全性和功能性。移動授權(Movement Authority， MA) 是CBTC系統(tǒng)的核心功能，用來保證列車的安全運行間隔。通過對移動授權生成原理的研究，采用時間自動機和其自動驗證工具UPPAAL對其進行建模以及驗證，驗證結果表明，搭建的移動授權模型能夠達到規(guī)定的安全要求和功能要求。因此UPPAAL能夠對復雜的實時系統(tǒng)進行仿真驗證。

CBTC；MA；時間自動機；UPPAAL

基于通信的列車運行控制系統(tǒng)CBTC相較于傳統(tǒng)的基于軌道的列車運行控制系統(tǒng)具有安全性高、線路運輸能力大、實時性好和軌旁設備少等優(yōu)點。世界上主要的經濟發(fā)達國家已經相繼研發(fā)出了自己的基于通信的列控系統(tǒng)，并且已經趨于成熟。而我國CBTC系統(tǒng)的開發(fā)還處于初步階段，移動授權的生成是聯系CBTC系統(tǒng)中各子系統(tǒng)的紐帶，并且直接影響行車效率和行車安全。采用形式化方法時間自動機對移動授權進行建模，并利用其自動驗證工具UPPAAL對模型的功能性能和安全性能進行驗證。

1 時間自動機與UPPAAL

時間自動機是一種形式化的建模方法，相較于有限自動機，它在模型的進程遷移間增加了時鐘約束。時間自動機模型由有限個控制位置和實數型時鐘構成，只有當控制位置間的時鐘約束滿足條件才能發(fā)生轉換?；跁r間自動機模型已經開發(fā)出了多種自動驗證工具，經過對比發(fā)現由Aalborg大學和Uppsala大學于1995年共同開發(fā)的UPPAAL驗證工具更為優(yōu)越。

UPPAAL工具主要由系統(tǒng)編輯器、模擬器和驗證器3個部分組成。編輯器用于創(chuàng)建和編輯要分析的系統(tǒng)，一個系統(tǒng)被描述為一系列過程模板、一些全局聲明、過程分配和一個系統(tǒng)定義。模擬器用于檢查所建模型可能的執(zhí)行是否有錯，以此在驗證前發(fā)現一些錯誤。驗證器通過快速搜索系統(tǒng)的狀態(tài)空間來檢查時鐘約束和活性。UPPAAL還專門為模型驗證提供了一種BNF語法：Prop::=A[]p|E<>p|E[]p |A<>p|p→p。這種語法的含義如表1所示。

表1 BNF語法的含義

2 移動授權生成原理分析

CBTC系統(tǒng)主要由區(qū)域控制器(Zone Control， ZC)、車載控制器(Vehicle On Board Controller， VOBC)、計算機聯鎖(Computer Interlocking， CI)、列車自動監(jiān)控系統(tǒng)(Automatic Train Supervision， ATS)、數據庫存儲單元(Database Storage Unit， DSU)和數據通信系統(tǒng)(Data Communication System， DCS)等組成。ZC作為CBTC系統(tǒng)重要的軌旁部件，根據CBTC其他子系統(tǒng)發(fā)送的各種狀態(tài)信息，為處于其管轄范圍內的列車分配移動授權，并通過DCS發(fā)送給列車，以此控制列車的安全運行。

IEEE1474.1將移動授權定義為：移動授權是為在一個給定的方向行駛的列車提供權限，使其進入或通過某一特殊的軌道區(qū)段，移動授權的分配、監(jiān)督和執(zhí)行由CBTC系統(tǒng)完成，該系統(tǒng)實現列車的安全分隔并通過聯鎖為列車提供防護[2]。實質上MA是指從列車的車尾起到列車前方第一個障礙物的這部分線路，ZC每次為列車計算授權時，需要明確授權起點、授權終點和授權方向3個要素，移動授權示意如圖1所示。

圖1 移動授權示意

MA的生成是通過CBTC系統(tǒng)中各個子系統(tǒng)間的信息交互實現的[3-5]。圖2為CBTC子系統(tǒng)的信息交互圖。

圖2 CBTC子系統(tǒng)信息交互

3 移動授權的自動機模型及驗證

3.1 移動授權過程分析

為了簡化模型，根據列車正常運行的過程，ZC可以把列車分為以下幾種狀態(tài)：未登錄狀態(tài)、登錄狀態(tài)、進入控制狀態(tài)、正常運行狀態(tài)以及注銷狀態(tài)[6]。在初始情況下，列車處于未登錄狀態(tài)，ZC通過VOBC發(fā)送給它的登陸申請來確定列車是否進入它的管轄范圍，如果ZC收到VOBC發(fā)送的登陸申請，則列車的狀態(tài)由未登陸狀態(tài)轉為登錄狀態(tài)；然后列車向ZC發(fā)送進入控制的申請，此時ZC需要判斷CI是否為列車排出進路，如果排出則進入正常運行狀態(tài)，否則列車保持在進入控制狀態(tài)不變；列車在進入正常運行狀態(tài)之后，則會按照ZC為它分配的移動授權運行；當列車接近ZC控制區(qū)域的盡頭時，會向ZC發(fā)送注銷請求信息，請求退出ZC控制，列車狀態(tài)轉為注銷狀態(tài)。一般情況下，列車只有在正常運行狀態(tài)才可以要求ZC為其發(fā)送移動授權[7]。移動授權的生成一般分為3個階段：第一為數據準備階段，ZC周期性的刷新從其他子系統(tǒng)發(fā)送的各種狀態(tài)信息，主要包括列車的位置信息以及障礙物的狀態(tài)信息；第二為移動授權生成階段，即對接收來的這些狀態(tài)信息進行一定的預處理，生成移動授權的過程可以分為兩個步驟，分別是障礙物的準備和障礙物的遍歷；第三為發(fā)送階段，即把生成的移動授權以及移動授權范圍內的障礙物信息通過DSU發(fā)送給列車。

移動授權生成的流程如圖3所示[8-10]。

圖3 移動授權生成流程

3.2 移動授權生成的自動機模型

通過對生成移動授權重要部件ZC的分析可知，ZC要實現移動授權的分配需要對ZC與其他子系統(tǒng)的信息交互、對列車各個狀態(tài)進行管理和移動授權生成3部分進行建模，而ZC與其他子系統(tǒng)的交互又分為與ATS的交互、與DSU的交互、與CI的交互和與VOBC的交互。

模型中主要位置如表2所示。

表2 模型中的主要位置

通過對以上5個部分進行建模，得到移動授權生成的成員自動機模型如圖4(a)～圖4(e)所示，分別為：列車、區(qū)域控制器、ZC與ATS信息交互、ZC與VOBC信息交互和ZC與CI信息交互。則整個系統(tǒng)的時間自動機模型為這些成員自動機模型之積，這是通過構造同步管道來實現的，用“!”結尾的通道表示發(fā)出此信息時轉換發(fā)生，用“？”結尾的通道表示接收到此信息時轉換發(fā)生，以此保證各成員自動機中相同的轉換同步。除了同步管道，UPPAAL中還另外增加了緊迫管道(urgent channel)、緊迫位置(urgent location)和堅定位置(committed location)。緊迫管道即當這個轉換發(fā)生時，沒有時間延遲，它對應的轉換上不能有時鐘約束。在緊迫位置處沒有時間延遲，理論上，它是增加了一個x<=0的時鐘約束。像緊迫位置一樣，堅定位置處也沒有時間延遲，但必須要有一個離開堅定位置的轉換[11-13]。

圖4 移動授權生成的時間自動機網絡模型

3.3 模型的仿真和驗證

在UPPAAL的編輯器中建立好移動授權的時間自動機網絡模型后，在模擬器中，對列車在運行過程中，會經歷未登錄、數據庫版本檢查、登陸、受控，正常運行和注銷這幾種狀態(tài)的轉換進行了模擬，同時在整個轉換過程中區(qū)域控制子系統(tǒng)完成了MA發(fā)送以及與其他子系統(tǒng)進行了狀態(tài)信息的交換。最后在UPPAAL的驗證器中，應用BNF語法對ZC的性能和功能要求進行描述驗證驗證結果如圖5所示。

圖5 性質驗證

(1) A []not deadlock通過驗證，即系統(tǒng)無死鎖；

(2)E<>((Train.Login)or(Train.Versioncheck) or (Train.Controlling) or (Train.Logoff))通過驗證，即列車能夠完成登陸，版本檢查，受控和注銷；

(3) E <> ZC. MAOutput通過驗證，即區(qū)域控制器能夠輸出MA信息；

(4) A []((Train.Login imply Train. T1<=T) or (Train. Controlling imply Train. T1<=T))通過驗證，即列車能夠在T個單位時間內完成登陸和受控。

4 結語

本文采用形式化方法時間自動機對移動授權進行建模并應用其自動驗證工具UPPAAL進行模擬驗證。成功的驗證了移動授權生成功能，保證了系統(tǒng)的活性完備性以及正確性，完成了對所建立模型的確認。因此，UPPAAL能夠對實時系統(tǒng)進行模擬驗證。

[1] 許丹.基于時間自動機的實時系統(tǒng)形式化建模與驗證[D].蘇州：蘇州大學， 2007.

[2] Rail Transit Vehicle Interface Standards Committee of the IEEE Vehicular Technology Society， IEEE Std 1474.1TM-1999，IEEE Standard for Communications-Based Train Control(CBTC) Performance and Functional Requirements[S]. USA: The Institute of Electrical and Electronics Eigineers，2005：1-20.

[3] 王莉莉，張玉平.城市軌道交通CBTC系統(tǒng)移動授權計算的研究[J].成都電子機械高等?？茖W校學報，2012，15(1):32-35.

[4] Wu Dong Yong， Zhang Yong. Researching Colored Petri nets Model of Communication Based Train Control System[J]. Journal of System Simulation， 2005，17(10):23-30.

[5] 李鳳華.城市軌道交通CBTC系統(tǒng)區(qū)域控制器的研究與仿真[D].蘭州：蘭州交通大學，2011.

[6] 劉曉娟，張雁鵬，李鳳華.基于通信的列車控制系統(tǒng)移動授權的研究與仿真[J].城市軌道交通研究， 2011，12(15):48-50.

[7] Meyer zu Horste， Michael Schnieder Eckehard. Modelling and Simulation of Train Control System Using Petri Nets[J]. World Congress on Formal Methods in the Development of Computing Science l709. Berlin: Springer， FME， September 1999， 2006.

[8] 朱光文.地鐵信號系統(tǒng)中車-地無線通信傳輸的抗干擾研究[J].鐵道標準設計，2012(8)：112-115.

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

[10]曹源，唐濤，徐田華，等.形式化方法在列車運行控制系統(tǒng)中的應用[J].交通運輸工程學報，2010，10(1):112-126.

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

[12]王淳.基于UPPAAL的系統(tǒng)建模驗證研究及其在CTCS-3列控系統(tǒng)的應用[D].北京：北京交通大學，2011.

[13]趙曉峰.基于螺旋模型的無線CBTC信號系統(tǒng)項目[J].鐵道標準設計，2012(9)：98-101.

Movement Authority Formal Modeling and Verification

HE Huan-huan1， CHEN Yong-gang1， LUO Ya-yun1， ZHANG Cai-zhen2

(School of automation and electrical engineering， Lanzhou Jiaotong University， Lanzhou 730070， China)

Compared with the traditional train control system， the communications-based train control system has been greatly improved either in function or in performance. In the development process of the system， system design flaws can be identified by modeling and verification so that the security and functionality of the system is guaranteed. Movement authority is a core function of CBTC system and is used to ensure the safe train interval. This paper， in the light of the generation principle of movement authority， uses timed automation modeling and UPPAAL verification for MA. The verification results show that the movement authority model so established can meet the requirements for safety and function. Thus， UPPAAL is capable of simulation and verification for complex real-time systems.

CBTC; MA; Timed Automation; UPPAAL

2014-05-29；

2014-06-10

甘肅省高校基本科研項目(620027)

賀歡歡(1990—)，女，碩士研究生。

1004-2954(2015)03-0118-04

U283

A

10.13238/j.issn.1004-2954.2015.03.028