城軌CBTC系統聯鎖表數據安全邏輯驗證方法研究

張 淼，黃友能，任嘯宇

（北京交通大學 軌道交通控制與安全國家重點實驗室, 北京 100044）

城軌CBTC系統聯鎖表數據安全邏輯驗證方法研究

張 淼，黃友能，任嘯宇

（北京交通大學 軌道交通控制與安全國家重點實驗室, 北京 100044）

聯鎖表是聯鎖安全邏輯的體現，本文針對聯鎖表數據的安全邏輯驗證問題，提出一種基于CSP的驗證方法。首先對聯鎖表數據進行建模，將聯鎖表數據抽象為調度員、道岔、信號機、區段和聯鎖控制器5個進程的并發組合模型，并對各進程進行建模。依據聯鎖系統安全約束條件，從功能性和安全性兩個方面，通過對模型正確性的驗證來說明數據的安全邏輯正確性。最后以北京地鐵亦莊站聯鎖表數據的安全邏輯驗證為例，說明該方法的可行性。

CBTC；聯鎖表邏輯；CSP

基于無線通信的列車自動控制系統（CBTC）是保證列車安全運行的關鍵系統。計算機聯鎖設備作為該系統中一個重要的組成部分，主要實現站臺和道岔區段信號機、道岔和進路之間的轉換與解鎖。

聯鎖表用來在車站和車輛段之間實現聯鎖關系，建立進路，控制道岔的轉換，信號機的開放以及進路解鎖，從而保證行車安全[1]。目前主要通過人工和功能測試的方法來保證聯鎖表數據安全邏輯的正確性，對人工和功能測試案例都提出了較高要求。

本文運用統一建模語言（UML，Unified Modeling Language，）對聯鎖表邏輯進行分析，將其抽象為對象及對象之間的信息交互過程，選取通信順序進程（CSP）形式化語言[2]描述對象的狀態轉移關系，利用這種方法自身底層的數學理論支持，對所有節點可以全部遍歷的優勢，以北京地鐵亦莊站為例，提出一種基于形式化的聯鎖表安全邏輯驗證方法。

1 CSP定義及特點

CSP語法中，具體刻畫某一客體相關全體事件名稱的集合叫做這個客體的字母表，用進程代表客體的行為，并規定這些客體的行為是能用組成客體字母表的事件的有限集合來說明的。對象狀態的轉移實質就是行為的樹狀示意圖中樹根到該節點沿途遇到的標記序列。

CSP是一種研究與并發性相關的理論問題的優秀工具，它可以提供并發系統的形式化研究所需的所有機制[3]。作為一種形式化方法，不僅形象直觀而且有數學理論支持，側重研究系統間的交互通信，具有遍歷節點的驗證特性，能全面證明聯鎖表數據的安全邏輯。本文著重分析聯鎖表安全邏輯，用UML分析5個對象的交互關系，重點闡述聯鎖表邏輯的形式化建模與驗證方法。主要研究路線如圖1所示。

圖1 主要研究路線

2 聯鎖表安全邏輯建模與驗證

2.1 聯鎖表中的聯鎖邏輯

聯鎖表包含進路、信號機、道岔及區段等信息，從進路選排到進路防護信號機開放主要經過操作、選路、道岔轉動、進路鎖閉和信號開放5個階段。

具體以北京地鐵亦莊站典型道岔區段為例，列車進路F4～F6如圖2所示。

圖2 F4～F6進路示意圖

對應以上進路的聯鎖表信息如表1所示。

表1 亦莊站部分聯鎖表

由表1可知，在CBTC模式下，選擇進路F4～F6，在滿足邏輯區段20G空閑的狀態條件下，檢查道岔位置3/6，4/5是否為定位，若不是則轉換道岔以滿足要求；確定道岔狀態后，檢查敵對進路F6沒有建立；則允許開放信號機F4，保持并開放進路。

2.2 UML順序圖描述聯鎖表邏輯信息

2.2.1 UML順序圖介紹

順序圖主要用二維圖來描述系統運行時各對象之間的交互時序關系，可以實現用例的邏輯建模。主要由4個標記符構成：對象、生命線、消息和激活?？v向是時間軸，時間沿著生命線向下延伸，橫向則代表參與相互作用的對象。消息由一個對象的生命線指向另一個對象的生命線的直線箭頭來表示，上面注明發送的消息名。

2.2.2 聯鎖表邏輯的UML順序圖模型

由2.1聯鎖表邏輯過程分析，可以將參與聯鎖表邏輯的對象抽象為：調度員、道岔、信號機、區段和聯鎖控制器；對象之間的邏輯關系由系統對象間交互信息來表達。這樣就可以將聯鎖表安全邏輯轉化成在滿足約束條件關系的前提下進行狀態轉移的關系。

具體到亦莊站的例子，用USER、SWITCH、F2、TRACK和CI 分別表示系統對象，對象間消息的傳遞通道定義得到聯鎖表對象間的交互關系，用UML順序圖[4]形象直觀地表達，如圖3所示。

圖3 進程F4-F6內部的消息傳遞示意圖

2.3 聯鎖表邏輯的CSP模型及驗證

在用CSP對系統建模過程中，將每個對象的操作稱為一個進程。因此聯鎖表邏輯被看作5個進程間的并發交互過程。對象之間需要通過通道進行信息交互，狀態轉換用基于CSP語義模型[5]中的跡圖表示。

2.3.1 聯鎖表邏輯的模型化

聯鎖表邏輯可以表達成5個對象之間的信息交互過程。下面分別對不同對象的動作進行分析，并用CSP對其建模。

首先分析USER進程，調度員通過chU2C發送選擇進路的命令給CI，滿足信號開放的條件后，CI通過chC2U反饋給調度信號機F4開放和進路建立成功的消息。其CSP的跡模型如圖4左側所示。

USER=chU2C!selectRoute-＞chC2U?F4opened-＞chC2U?routeBuilt-＞USER

同理對于信號機F4來說，接收到聯鎖控制器發來的openF4信息后開放信號機，繼而通過chS2R通道將狀態信息反饋給CI進程。F4進程的CSP語義描述為：

F4 = chR2S?o p e n F4-＞c hS2R!F4o pe n ed-＞chR2S?F4hold-＞F4

圖4 USER和信號機F4進程跡圖

SWITCH進程通過chC2S通道收到聯鎖檢查4號道岔和6號道岔的要求，操作過程中并不關注具體的時序關系，所以將道岔分別處理并看作兩個進程，只有當這兩個進程都滿足條件時才能開放進路。在CSP中可以用并發來表達嚴格同步的兩事件構成整個系統的行為，并同時參與到公共事件上。

這里對4號道岔的檢查作如下說明，如果其位于正位，直接鎖閉；若位于反位，則將其扳至正位，再進行鎖閉，這之間是選擇的關系，只有道岔鎖閉后才能允許信號機F4開放。

SWITCH4=chC2S?checkSwitch4-＞(chS2C! normal-＞chC2S?lockSwitch4)[](chS2C!reverse-＞chC2S?turnSwitch4-＞chS2C!normal-＞chC2S?lock-Switch4)-＞openF4-＞SWITCH4

同理對于6號道岔的檢查、操作與鎖閉用CSP代碼表達如下：

SWITCH6=chC2S?checkSwitch6-＞(chS2C!-normal-＞chC2S?lockSwitch6)[](chS2C!reverse-＞chC2S?turnSwitch6-＞chS2C!normal-＞chC2S?lockSwitch6)-＞openF4-＞SWITCH6

只有當上述兩個進程進行到公共事件，openF4才可以發生，滿足案例的實際需求，道岔進程的CSP最終表達式如下：

SWITCH= SWITCH4|| SWITCH6

對應跡圖如圖5所示。

圖5 SWITCH進程跡圖

道岔鎖閉之后，要對區段出清以及敵對進路未建立做進一步的確認。這就要對Track20D對象進行分析建模。Track20D通過chC2S通道接收聯鎖控制器發來的檢查軌道區段狀態的命令，分別檢查20D是否空閑以及敵對信號F6是否開放，對應的CSP模型表達如下：

基于CSP語義模型中的跡模型，進程TRACK的跡模型如圖6所示。

控制器作為最復雜的元件和系統中所有對象之間都存在交互關系，從時間的先后進行角度，首先CI進程由通道chU2C收到調度員發出的選排路指令，如果符合道岔鎖閉在正確位置、區段空閑且不存在敵對進路的條件則開放信號機，若其中一個條件不滿足，則進路無法建立。用CSP跡圖形象直觀的表達上述建立進路的聯鎖邏輯信息，圖7為先對道岔4位置檢查的聯鎖控制器進程跡圖。

圖6 TRACK進程跡圖

圖7 CI部分進程跡圖

綜上所述，進路F4～F6的行為就是5個對象的行為的并發組合：

F4-F6=USER||SWITCH||F4||TRACK||CI

聯鎖表由多條進路組成，每一條進路都可仿照上述思想建立模型，最終所有進路的并發組合就作為聯鎖表邏輯的完整模型，通過對模型正確性的驗證來說明數據的安全邏輯正確性。

2.3.2 模型的驗證

計算機聯鎖表邏輯是行車最基礎的安全保證。從總體驗證思路上，將聯鎖表邏輯的驗證分為功能性驗證和安全性驗證，所謂安全性驗證，主要是滿足列控領域相關要求的特殊屬性。

建模及驗證工具ProB[6]為聯鎖邏輯提供針對不同性質便捷的模型驗證技術，像死鎖、活鎖，可達性，線性時序邏輯（LTL，linear temporal logic）[7]，優化驗證和可能性模型驗證，此工具通過深度和廣度優先搜索，遍歷模型中所有狀態節點，以快速找出存在問題節點的最短路徑。

（1）功能性驗證

功能性驗證主要是從模型性質的角度對系統進行驗證，保證所有節點的狀態轉移

#assert System() deadlockfree;

死鎖狀態是指無法成功終止一個不可動的狀態。#assert System() divergencefree;

活鎖狀態是指給定一個進程，它一直在內部轉換，無法到達有用的事件。

#assert System() deterministic;

確定性是指給定一個進程，如果它是確定性的，那么不論任何狀態，一個事件不會遷移到兩個狀態。

（2）安全性驗證

聯鎖作為安全苛求系統，其中聯鎖表的安全邏輯反應了系統的可靠性和安全性，是安全性驗證的重點。在進路建立的過程中，主要關注以下3方面：進路道岔及防護道岔被鎖閉；進路區段空閑且解鎖；敵對進路未建立。用LTL語言來描述進路需要滿足的安全條件。

a.驗證當進路上所有道岔位置正確且鎖閉時進路才能建立，針對F4～F6進路，即當道岔4、道岔6分別在定位且鎖閉時進路建立，信號機F4才能開放。對應LTL表達式：

G([switch4normal]&[switch6normal]=＞F [F4opened])

b.驗證進路對應區段空閑才能建立進路，進路F4～F6要檢查的區段是20D，相應的LTL表達式：

G([track20Dempty]=＞F[F4opened])

c.要驗證任意兩條敵對進路不能同時建立，容易從聯鎖表中找到進路F4～F6的敵對進路信號為F6，將關系寫成LTL表達式：

notG([F4opened]&[F6open])

在ProB中將聯鎖表中每一條進路按上述安全條件列舉，逐項驗證性質，得到的結果中若沒有反例以證明模型的安全性，從而通過證明模型的正確性追溯到聯鎖表數據安全邏輯的正確性。

（3）結果分析

將亦莊站的聯鎖表中列車進路部分的每一條進路寫成5個對象之間的交互關系，繼而對所有進路用CSP建模，錄入到模型驗證工具ProB中。選擇Verify-＞Model Check，利用自動驗證判斷出模型自身無死鎖、活鎖且滿足確定性斷言。

在ProB中對道岔位置、邏輯區段空閑和敵對進路建立的安全條件逐條檢測，驗證結果沒有反例，說明模型中任意兩條敵對進路都無法建立；進路的道岔與進路開通方向一致且鎖閉，滿足邏輯區段空閑條件時，才可能建立，從而得到安全性方面的模型驗證結果，綜合得出亦莊站的聯鎖表數據邏輯滿足安全性要求的結論。

3 結束語

本文以北京地鐵亦莊站列車進路聯鎖表數據為例，用CSP定義聯鎖表安全邏輯的具體過程。聯鎖表數據安全邏輯CSP模型的應用顯示，該模型不僅能模型化系統對象間的交互過程，還能對聯鎖系統安全性和實時性進行分析，保證聯鎖表安全邏輯的正確性。

[1]宿浩峰.城市軌道交通聯鎖系統建模的研究[D].杭州：浙江大學，2012.

[2]C.A.R.Hoare.Communicating Sequential Processes[Z]. Prentice Hall, Inc., Upper Saddle River, NJ, USA, 1985.

[3]孫 麒，張云華.基于CSP的形式化方法研究[J].浙江理工大學學報，2009，26（4）：557-560.

[4]程 梁.基于UML的聯鎖軟件建模與仿真研究[D].北京：北京交通大學，2007.

[5]屈延文.形式語義學基礎與形式說明[M].北京：科學出版社，2009：418-466.

[6]Michael Leuschel, Michael Butler. ProB: A Model Checker for B[D]. Department of Electronics and Computer Science, University of Southampton, 2014.

[7]趙嶺忠，張 超，等.基于ASP的CSP并發系統驗證研究[J].計算機科學，2012，39（12）：125-132.

責任編輯 陳 蓉

Data safety logic verif i cation method of interlock table for Urban Transit CBTC System

ZHANG Miao, HUANG Youneng, REN Xiaoyu
( State Key Laboratory of Railway Traff i c Control and Safety, Beijing Jiaotong University, Beijing 100044, China )

The interlock safety logic was ref l ected by interlock table. This paper proposed a verif i cation method based on CSP (Communicating Sequential Processes) to solve the data safety logic verif i cation problem of interlock table, modeled data of the interlock table at fi rst, abstracted fi ve processes of dispatchers, switch, signal machine, segment and interlocking controller from the data of interlocking table, and further modeled the processes respectively. The correctness of the model was verif i ed from the functional and safety aspects. At last, an example of data safety logic verif i cation with the interlock table in Yi Zhuang Station of Beijing Metro illustrated the feasibility of the method.

Communication Based Train Control(CBTC); interlock table logic; Communicating Sequential Processes(CSP)

U132.7∶TP39

A

1005-8451（2015）05-0053-05

2014-10-19

北京市科委項目（KWH13001531）；軌道交通北京實驗室項目（W13H100061）。

張 淼，在讀碩士研究生；黃友能，副教授。