基于Timed-UML順序圖的RBC交接形式化建模與分析

安　越，李國寧

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

?

基于Timed-UML順序圖的RBC交接形式化建模與分析

安越，李國寧

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

摘要：在CTCS-3級列控系統(tǒng)中，采用RBC技術將線路劃分成多個管轄區(qū)段。當列車行駛并跨越相鄰RBC交界區(qū)域時，控制權將會移交至前方相鄰RBC，整個過程稱為RBC交接。在運行中，RBC交接過程能否實時安全可靠地執(zhí)行，直接影響著列車的行車效率和乘客的生命安全。采用一種基于添加實時約束的UML順序圖與時間自動機結合的模型來建立RBC交接場景。以雙車載電臺的RBC切換策略出發(fā)，建立切換的Timed-UML順序圖模型，然后按照UML-TA轉換規(guī)則，建立得到完整的時間自動機網絡模型。并利用UPPAAL驗證工具對RBC交接模型進行形式化建模及分析，對模型的死鎖和功能實現做了驗證，從而達到對CTCS-3級RBC子系統(tǒng)的實時性以及設計規(guī)范合理性的驗證目的。

關鍵詞：車載系統(tǒng)；RBC交接；實時UML順序圖；時間自動機

1概述

RBC子系統(tǒng)作為CTCS-3級列控系統(tǒng)車-地數據信息交互中心，主要負責給列車發(fā)送行車控制所需的數據信息，包括移動授權MA(Move Authority)及線路信息等。車載子系統(tǒng)根據接收到MA數據，結合列車當前所在的位置，計算距離-速度監(jiān)控曲線，對列車的運行狀態(tài)實時監(jiān)控，保證行車安全。RBC交接是CTCS-3級列車控制系統(tǒng)非常重要的運行場景之一，在整個交接過程中主要是由兩個相鄰RBC系統(tǒng)以及車載之間的數據信息的交互來完成。

根據RBC切換的功能要求，從數據的傳輸到切換功能的實現，必須滿足數據及其交互的一致性，實時性和安全性要求，采用形式化建模與驗證方法是可行的。形式化模型方法具有嚴格的數學語法和語義，可以準確地描述系統(tǒng)模型，但其所包含的復雜數學理論很大程度上限制了工程人員的學習和使用[1]。在工程實踐中，人們更多地傾向于使用統(tǒng)一建模語言UML來建模和交流，但對于實時性系統(tǒng)來說，UML的建模能力有限。

時間自動機TA(Timed Automata)是在自動機理論的基礎上擴展時間約束，為了解決實時系統(tǒng)建模和驗證問題，它提供了一種簡單而有效的方法以描述帶有時間因素的系統(tǒng)，為實時系統(tǒng)的行為建模和性能分析提供了形式化模型[2]。為了實現自動模擬和分析實時系統(tǒng)的行為特性，有學者在時間自動機原理的基礎上開發(fā)了一種模型檢測工具UPPAAL。該驗證工具采用帶有整型變量的TA網絡模擬實時系統(tǒng)的行為，采用時序邏輯TCTL(Time Computation Tree Logic)刻畫系統(tǒng)的實時特性，然后將二者載入驗證器中，通過有限狀態(tài)搜索驗證系統(tǒng)是否具備所期望的性質。

根據RBC切換功能有著嚴格的實時性等特征，本文結合了UML和時間自動機(TA)的優(yōu)點，在UML2.0的基礎上，將UML順序圖擴展了時間機制，并建立了RBC切換模型，然后將UML順序圖轉化成相應的TA網絡模型；并通過UPPAAL驗證工具對RBC切換的TA模型進行形式化驗證和分析[3-4]。

2基于UML擴展模型的建模

UML時序圖是強調信息時間順序的交互圖，它描述了對象之間消息傳送的時間順序，并按照時間順序對系統(tǒng)控制進行建模，是系統(tǒng)的動態(tài)試圖，強調了對象間發(fā)送信息的順序和交互，顯示的是對象間的動態(tài)轉化和合作關系[5-6]。

但是在模擬實時系統(tǒng)時，無法精確地表示很多消息傳遞時間或者事件間隔的時間長短，只能簡單的表述事件或者消息的先后關系，這使得模型并不能全面地體現系統(tǒng)的實時性能。UML2.0中實現了對于實時系統(tǒng)的時間擴展，提供了表示時間、時間間隔約束以及用來觀測時間進展的動作的原模型，這使得可以利用此機制對模型進行精確地建模。具體實例操作如圖1所示。

圖1　UML順序圖中的時間機制

為了使擴充的順序圖能夠表達實時性并體現RBC交接中涉及的各設備間的獨立時鐘以及體現數據老化時間概念，對順序圖進行了一下擴展。

(1)事件上的標簽值添加兩個時間約束：

①時間重復；

②事件上發(fā)生對象的獨立時鐘時間。

(2)事件中的時間約束是表示在事件發(fā)生時必須滿足的條件約束。在滿足條件的時刻，系統(tǒng)就會轉移到下個事件。

(3)當只有在滿足相應的時間約束時，事件中的消息傳遞才能發(fā)生。

(4)根據UML2.0的時間機制，對象的每兩個事件進行老化時間賦值。

3時間自動機的轉換機制

在RBC交接過程中，車載系統(tǒng)需要處理的數據有：自身計算得到的列車所在的位置信息，以及從接口得到的RBC設備發(fā)送的MA數據和與RBC系統(tǒng)的通信信息。隨著列車運行，這些數據信息會實時和動態(tài)地產生。根據動態(tài)數據中存在的依賴關系和數據老化特點，提出了基于TA模型的數據安全驗證方法，以UML為源模型，進行了時間上的擴展，并以模型間轉換規(guī)則為基礎，將 UML順序圖 建立的時序模型轉換為TA擴展模型并進行驗證，解決了車-地動態(tài)數據存在的一致性問題和數據在應用過程中出現的組合錯誤等問題，并通過具體實例表明模型間轉換的可行性[7]。

3.1時間自動機擴展

根據標準定義，時間自動機自帶的時間的約束功能已經很好地體現了實時系統(tǒng)的一些時間方面的要求。但是標準的時間自動機并沒有老化時間的概念，從而也無法體現老化時間對于系統(tǒng)的影響，所以需要在原有的模型上添加老化時間集合[8]。

擴展的時間自動機定義:時間自動機TA是一個七元組

其中：

(1)S是有窮位置集合；

(2)是初始位置集合；

(3)是有窮事件集合；

(4)X是有窮時鐘集合，I是一個映射(它給每個位置S指定了一個時鐘約束)；

(5)DA是老化時間集合；

(6)E∈L×∑×φ(X)×2X×DA，為狀態(tài)轉移集合。

TA的一種狀態(tài)遷移公式為，更加直觀的表示是，這個轉移公式表示在事件 α(α∈∑) 發(fā)生的條件下，當事件α的發(fā)生時間滿足時鐘約束δ時，TA從狀態(tài)n遷移到狀態(tài)m，成功遷移之后，λ內部的全部時鐘重新設置為0，之后從狀態(tài)發(fā)生遷移的這一時刻起重新計算時間[9-10]。見圖2。

圖2　TA的狀態(tài)轉移

3.2UML-TA場景模型轉換規(guī)則

規(guī)則一：單元片段轉化。

為了得到相應的單元自動機，需要將每個單元片段的數據集合進行對應轉化。

自動機集合S的格式為(W，da，T)的有限狀態(tài)集，其中有滿足R中所定義的可視事件對。da集合是時間W上的老化時間單元。對于同一對象的可視化事件對，先發(fā)生的da為時間min，后發(fā)生的時間為max，對應于UML圖中的老化時間；T集合是事件上的時鐘集，對應于UML時序圖中對象間發(fā)生事件的時間約束條件。

規(guī)則二：組合片段轉化。

UML2.0中有alt，opt，loop等組合約束片段，以及多個組合片段組成一個完整的組合，在UML中組合片段是嚴格按照生命線上的順序執(zhí)行，將上述這些不同的組合片段分別進行轉化，得到相應的TA模型。

(1)Alt片段表示在一組行為中根據特定的條件選擇交互，模型為if…else。

設函數Alt(G，A)，A代表所有可以選擇片段集合，G代表對應可選分支的約束。根據Alt片段的邏輯定義，構造的TA模型為TAn(N，n0，L)。TA1，TA2，…是可選片段各自構造的自動機，從相應的UML-TA轉換規(guī)則得到：

Alt(G，A)→TAalt(N，n0，L)

n0是一個新的空狀態(tài)，N={n0}∪N1∪N2… ，L={，}…∪L1∪L2…。

(2)Opt片段表示單獨選擇，模型為switch；

設函數Opt(S)，S代表單個分支片段。TA1，TA2是各自構造的自動機，相應的轉換規(guī)則：

Opt(S)→TAopt(N，n0，L)

n0是一個是新的空狀態(tài)，N={n0}∪N1∪N2，L={，}∪L1∪L2。

(3)Par片段支持多個片段并發(fā)執(zhí)行，執(zhí)行順序沒有特定要求。

設函數Par(PF，n)，PF表示組合中包含多個片段，n表示組合中的片段個數。TA1，TA2…是多個片段組合各自構造的自動機，按照以下轉換規(guī)則得到相應的自動機結構

Par(F，n)→TApar(N，n0，L)

n0是一個新的空狀態(tài)，N={n0}∪N1∪N2… ，L={，…}∪L1∪L2…|{

n1，0>，…}∪L1∪L2…|…，其中S1，S2…是等概率發(fā)生事件，每個并行片段發(fā)生概率都是1/n。

(4)Loop片段表示交互片段會被循環(huán)執(zhí)行。

設函數Loop(LF，guard)，LF為所要重復的子片段，guard為條件，TA是需要循環(huán)片段構造的自動機，按照以下規(guī)則得到對應的自動機

Loop(LF，guard)→TAloop(N，n0，L)

n0是一個新的空狀態(tài)，N={n0，ne}∪N1，ne是一個新的空狀態(tài)L={，}∪L1。

(5)Strict片段表示一組片段執(zhí)行的次序有特定要求。

設函數Strict(SF，SForder)，SF為多個片段集合，SForder為片段排列順序。TA1，TA2，…是多個片段組合各自構造的自動機，按照以下規(guī)則得到相應的自動機結構

Strict(SF，SForder)→TAstrict(N，n0，L)

4RBC交接場景的形式化建模

4.1RBC切換協(xié)議

RBC交接采用的是車載EVC和相鄰RBC之間交互通信的方式實現RBC交接數據信息的交互，并且使用的RBC負責與前方相鄰RBC在設定的兩交界區(qū)域完成列車的無縫交接[11-12]。在交接過程中，不僅要實現自動執(zhí)行交接，而且不能引起列車制動。

RBC交接有兩種實現策略，包括車載單電臺模式和車載雙電臺模式。本文以雙電臺的交接策略為實例進行分析，整個執(zhí)行流程如下。

當列車行駛靠近兩個RBC邊界，并到達預告應答器組LTA時，車載設備給“YRBC”發(fā)送列車位置數據信息(msg136)。當“YRBC”收到列車位置信息后，會給車載EVC傳送切換命令信息(msg201)，并將車載的ID信息和當前位置信息等數據發(fā)送給“HRBC”；車載再依據RBC提供的ID建立起和“HRBC”設備的通信，并給“HRBC”發(fā)送列車的基本數據信息；“YRBC”給“HRBC”發(fā)送列車移交預告和進路請求數據信息，并且依據獲得的進路信息、“HRBC”的答復信息和線路狀況數據信息計算得到包括了RBC交界的移動授權MA；車載系統(tǒng)依據RBC提供的ID，使用2號電臺呼叫“HRBC”，呼叫成功后，建立通信。當列車的最大安全前端行駛過RBC交界處后，車載系統(tǒng)給相鄰的兩個RBC發(fā)送列車的位置信息，當“YRBC”獲得列車的位置信息后，給“HRBC”發(fā)送列車已進入其所管轄線路的信息的通知；當“HRBC”接收到位置信息并檢測到列車最大安全前端已經通過了RBC間的邊界區(qū)域后，則給“YRBC”發(fā)送控制權接收的信息；當列車最小安全末端穿越過RBC交界后，車載系統(tǒng)不再接收任何由“YRBC”發(fā)送的命令信息，除了“斷鏈命令”命令；當整個列車通過RBC交界區(qū)域后，“YRBC”向車載系統(tǒng)發(fā)送停止會話命令信息，車載系統(tǒng)成功收到這個命令后切斷與YRBC的信息交互連接[13-14]。

4.2RBC切換的UML順序圖

以CTCS-3級列控系統(tǒng)總體技術方案內容為理論基礎，并以車載雙電臺切換策略為實例，根據UML順序圖的擴展時間機制，對整個交接流程進行可視化建模，如圖4所示。

圖4　帶有時間擴展的RBC 切換順序

4.3RBC切換的TA模型

本文通過UPPAAL工具對RBC交接場景進行建模，并根據TA網絡積的概念，建立相應的TA模型：EVC||HRBC||TRBC。其部分模型如圖5所示。

圖5　RBC切換TA圖

模型中，以“!”標記的同步通道表示發(fā)出此信號時狀態(tài)發(fā)生遷移；以“？”為后綴的同步通道表示接收到該條件時狀態(tài)發(fā)生遷移。除此之外，定義了一些成員函數和局部變量來表示系統(tǒng)模型的屬性和行為，在整個模型與系統(tǒng)之間還設置了全局變量來保證模型邏輯功能的正確性。見表1和表2。

在時間控制方面，Tevc代表車載子系統(tǒng)EVC的內部時鐘，Tacc代表接受RBC的內部時鐘，Thov代表移交RBC系統(tǒng)的內部時鐘，它們分別對各個TA模型網絡的狀態(tài)運行進行記錄。在狀態(tài)標識中，標有U的狀態(tài)為緊迫位置，沒有延遲時間，從而減小整個模型中的時鐘數量，從而降低了模型分析的復雜度，標有C的狀態(tài)代表緊急狀態(tài)，利用其的不允許下一個轉移有時間上的延遲的特性，可以實現車載設備和RBC系統(tǒng)之間的無延遲時間數據交互[14]。模型中還設定了一些常整數rbcCycle表示RBC的數據處理時間；evcCycle表示車載EVC的數據處理時間；LTA2RN表示從交接預告應答器組到交接邊界的長度距離。

表1　模型中的主要同步通道

表2　模型中的主要變量定義

5模型的驗證分析

UPPAAL工具利用了時序邏輯公式在TA網絡中進行有窮搜索來完成對功能的驗證，該軟件使用的是時間分支時序邏輯的子集，可以準確的描述線性時序邏輯[13]。BNF語法公式為

Prop::=A[]p|E<>p|E[]p|A<>p|P→p

其中：

1)E<>p表示Possible; E<>p為真，當且僅當在轉換系統(tǒng)中存在一個序列s0→s1→…→sn，使得s0是初始狀態(tài)，sn代表目標狀態(tài)；

2)A[]p表示Invariantly，等價于not E<>not p；

3)E[]p表示Potentially always，E[]p為真，當且僅當存在一個序列s0→s1→…→si→…使得p在所有狀態(tài) si中都有效，并且這個序列無窮或者在狀態(tài)sn終止；

4)A<>p表示Eventually，等價于notE[]p；

5)P→p表示Lead to ，等價于A[](P imply A<>p)。

并且利用BNF語法表達的時態(tài)邏輯公式能夠準確的描述并發(fā)系統(tǒng)的性質，比如受限活性和安全性[15]。接下來將從功能邏輯、安全性和實時性對RBC切換的TA網絡模型進行驗證和結果分析。

邏輯功能和安全性驗證。

a)A[]not deadlock，表示系統(tǒng)沒有死鎖；

b)E<>(EVC.wait4MA)and s>=aFirstMA，表示列車能夠發(fā)送申請MA請求；

c)E<>(EVC.gotMA)and((hovRBC.stMA2)or (hovRBC.stMA))，表示列車能夠接受MA；

d)(checkCount()==1)and(not accRBC.ConEsted)->EVC.abortion，表示安全建鏈失敗下放棄RBC切換；

e)A<> (EVC.headOverRN)and s>=LTA2RN，表示車頭越過RN能夠發(fā)出關鍵位置報告；

f)A<>(EVC.tailOverRN)and s>=(LTA2RN+LENGTH_T)，表示車尾越過RN能夠發(fā)出關鍵位置報告；

g)A<>EVC.headOverRN imply(hovRBC.gotLocationReport or hovQueue.hcatchMAX)，表示移交RBC總能收到頭車過RN的位置報告；

h)A<>EVC.tailOverRN imply(hovRBC.gotLocationReport2 or hovRBC.joint7 or hovQueue.HcatchM-IN2)，表示RBC總能收到車尾過RN的位置報告；

i)E<>(accRBC.ready4Data)and >=aFirstMA，表示接管RBC能夠收到線路請求；

j)A<>(accRBC.stTransmit1 or ccRBC.joint2) imply(accQueue.acatchTransmit1 or accRBC.gothovL-

Report or accRBC.joint1 or accRBC.gotMARes)，表示總能收到來自移交RBC的MSG136MAX的轉發(fā)；

k)A<>(accRBC.stTransmit2 or ccRBC.joint3) imply(accQueue.acatchTransmit1 or accRBC.gotTrans-

mit2 or accRBC.joint6 or accRBC.endacc)，表示總能收到來自移交RBC的MSG136MAX的轉發(fā)；

l) A<>((hovRBC.gotLocationReportReport or hovQueue.hcatchMAX)and accQueue.acatchMAX)

imply BREAK==1，表示未與接管RBC建立通信會晤即跨越RN時必須制動。

6結語

本文以車載雙電臺的模式為實例，對CTCS-3級列控系統(tǒng)運行場景之一的RBC交接進行分析，對其過程的實現原理，邏輯功能和實時性以及安全性進行了形式化建模和驗證分析。文中利用一種將擴展了時間約束的UML順序圖和擴展了老化時間的TA模型相結合的方法對基于車載雙電臺的RBC交接場景進行分析，并使用UPPAAL檢驗工具對交接場景建立了相應的TA網絡模型，然后對模型進行了完整的形式化驗證和結果分析。通過文中的方法和操作，完整地驗證和分析了整個RBC交接過程中的實時性、邏輯功能

等安全性能，并得到理想的結果，從而保證了CTCS-3級列車控制系統(tǒng)中車載子系統(tǒng)和RBC間的數據信息通信的安全及暢通。

參考文獻：

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

[2]韓德帥，楊啟亮，邢建春.一種軟件自適應UML 建模及其形式化驗證方法[J].軟件學報，2015，26(4)：730-746.

[3]姬莉霞，馬建紅.基于時間自動機UML模型轉換與驗證研究[J].鄭州大學學報(理學版)，2013，1(45)：50-55.

[4]吳永剛，陸慧娟，程倬，等.基于時間自動機的實時系統(tǒng)建模及驗證[J].計算機時代，2011，6：1-3.

[5]黃友能.城軌CBTC系統(tǒng)數據的安全處理與驗證方法研究[D].北京：北京交通大學，2014.

[6]周清雷，姬莉霞，王艷梅.基于UPPAAL的實時系統(tǒng)模型驗證[J].計算機應用，2004，24(9)：130.

[7]劉傳會.基于UML2.0的實時軟件動態(tài)行為模型一致性驗證[D].蘇州：蘇州大學，2008.

[8]李巖.可調整時間自動機可達性算法的研究[J].信息技術，2014(9)：4-7.

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

[10]李波，楊弘平，呂海華，等.UML2基礎、建模與設計實踐[M].北京：清華大學出版社，2014.

[11]叢新宇，虞慧群.基于實時UML順序圖的物聯(lián)網交互模型[J].計算機科學，2014，11(14)：79-87.

[12]鐵道部科技司.CTCS-3級列控系統(tǒng)標準規(guī)范系統(tǒng)-無線閉塞技術規(guī)范[M].北京：中國鐵道出版社，2008.

[13]徐世澤，肖蒙.基于Timed RAISE的高速列車RBC切換協(xié)議形式化建模及驗證[J].鐵道標準設計，2015,59(6):138-143.

[14]唐濤，趙林，徐田華，等.基于模型的列車運行控制系統(tǒng)設計與驗證方法[M].北京：中國鐵道出版社，2014.

[15]胡雪蓮，陶彩霞.基于MSC與UPPAAL的列控系統(tǒng)等級轉換場景形式化驗證[J].鐵道標準設計，2015，59(2):122-127.

收稿日期：2015-09-16； 修回日期：2015-10-23

作者簡介：安越(1987—)，男，碩士研究生，研究方向為高速鐵路計算機技術的應用，E-mail：feixuerenzhe2377@163.com。

文章編號：1004-2954(2016)06-0132-06

中圖分類號：U284.48

文獻標識碼：A

DOI:10.13238/j.issn.1004-2954.2016.06.027

Formal Modeling and Analysis of RBC Handover Based on Timed UML Sequence Diagram

AN Yue，LI Guo-ning

(School of Automatization & Electric Engineering，Lanzhou Jiaotong University，Lanzhou 730070，China)

Abstract：In the CTCS-3 level train control system，a line is divided into several RBC control sections. When the train runs through an adjacent RBC region，the control of the train will be handed over to the region，which is called RBC handover. In the operation of the train，safe and reliable RBC handover is the key to the operation efficiency and safety of passengers. In this paper，a model based on the combination of the UML sequence diagram with the time automaton with real-time constraints is used to establish RBC handover scenario. Based on RBC switching strategy of dual onboard radio station，the timed-UML sequence diagram model is established，and then the complete time automaton network model is established according to the UML-TA conversion rule. The UPPAAL verification tool is used to model and analyze RBC handover. The deadlock and the function realization of RBC handover model are verified to confirm the real-time performance and the rationality of the design specifications for CTCS-3 level control system．

Key words：On-board system; RBC handover; Timed UML sequence diagram; Time automaton