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

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

移動(dòng)授權(quán)的形式化建模與驗(yàn)證

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

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

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

CBTC；MA；時(shí)間自動(dòng)機(jī)；UPPAAL

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

1 時(shí)間自動(dòng)機(jī)與UPPAAL

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

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

表1 BNF語(yǔ)法的含義

2 移動(dòng)授權(quán)生成原理分析

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

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

圖1 移動(dòng)授權(quán)示意

MA的生成是通過(guò)CBTC系統(tǒng)中各個(gè)子系統(tǒng)間的信息交互實(shí)現(xiàn)的[3-5]。圖2為CBTC子系統(tǒng)的信息交互圖。

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

3 移動(dòng)授權(quán)的自動(dòng)機(jī)模型及驗(yàn)證

3.1 移動(dòng)授權(quán)過(guò)程分析

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

移動(dòng)授權(quán)生成的流程如圖3所示[8-10]。

圖3 移動(dòng)授權(quán)生成流程

3.2 移動(dòng)授權(quán)生成的自動(dòng)機(jī)模型

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

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

表2 模型中的主要位置

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

圖4 移動(dòng)授權(quán)生成的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型

3.3 模型的仿真和驗(yàn)證

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

圖5 性質(zhì)驗(yàn)證

(1) A []not deadlock通過(guò)驗(yàn)證，即系統(tǒng)無(wú)死鎖；

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

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

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

4 結(jié)語(yǔ)

本文采用形式化方法時(shí)間自動(dòng)機(jī)對(duì)移動(dòng)授權(quán)進(jìn)行建模并應(yīng)用其自動(dòng)驗(yàn)證工具UPPAAL進(jìn)行模擬驗(yàn)證。成功的驗(yàn)證了移動(dòng)授權(quán)生成功能，保證了系統(tǒng)的活性完備性以及正確性，完成了對(duì)所建立模型的確認(rèn)。因此，UPPAAL能夠?qū)?shí)時(shí)系統(tǒng)進(jìn)行模擬驗(yàn)證。

[1] 許丹.基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)形式化建模與驗(yàn)證[D].蘇州：蘇州大學(xué)， 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)移動(dòng)授權(quán)計(jì)算的研究[J].成都電子機(jī)械高等?？茖W(xué)校學(xué)報(bào)，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].蘭州：蘭州交通大學(xué)，2011.

[6] 劉曉娟，張雁鵬，李鳳華.基于通信的列車控制系統(tǒng)移動(dòng)授權(quán)的研究與仿真[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] 朱光文.地鐵信號(hào)系統(tǒng)中車-地?zé)o線通信傳輸?shù)目垢蓴_研究[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2012(8)：112-115.

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

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

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

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

[13]趙曉峰.基于螺旋模型的無(wú)線CBTC信號(hào)系統(tǒng)項(xiàng)目[J].鐵道標(biāo)準(zhǔn)設(shè)計(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

甘肅省高?；究蒲许?xiàng)目(620027)

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

1004-2954(2015)03-0118-04

U283

A

10.13238/j.issn.1004-2954.2015.03.028