張 淼，黃友能，任嘯宇

（北京交通大學(xué) 軌道交通控制與安全國家重點(diǎn)實(shí)驗(yàn)室, 北京 100044）

城軌CBTC系統(tǒng)聯(lián)鎖表數(shù)據(jù)安全邏輯驗(yàn)證方法研究

張 淼，黃友能，任嘯宇

（北京交通大學(xué) 軌道交通控制與安全國家重點(diǎn)實(shí)驗(yàn)室, 北京 100044）

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

CBTC；聯(lián)鎖表邏輯；CSP

基于無線通信的列車自動(dòng)控制系統(tǒng)（CBTC）是保證列車安全運(yùn)行的關(guān)鍵系統(tǒng)。計(jì)算機(jī)聯(lián)鎖設(shè)備作為該系統(tǒng)中一個(gè)重要的組成部分，主要實(shí)現(xiàn)站臺和道岔區(qū)段信號機(jī)、道岔和進(jìn)路之間的轉(zhuǎn)換與解鎖。

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

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

1 CSP定義及特點(diǎn)

CSP語法中，具體刻畫某一客體相關(guān)全體事件名稱的集合叫做這個(gè)客體的字母表，用進(jìn)程代表客體的行為，并規(guī)定這些客體的行為是能用組成客體字母表的事件的有限集合來說明的。對象狀態(tài)的轉(zhuǎn)移實(shí)質(zhì)就是行為的樹狀示意圖中樹根到該節(jié)點(diǎn)沿途遇到的標(biāo)記序列。

CSP是一種研究與并發(fā)性相關(guān)的理論問題的優(yōu)秀工具，它可以提供并發(fā)系統(tǒng)的形式化研究所需的所有機(jī)制[3]。作為一種形式化方法，不僅形象直觀而且有數(shù)學(xué)理論支持，側(cè)重研究系統(tǒng)間的交互通信，具有遍歷節(jié)點(diǎn)的驗(yàn)證特性，能全面證明聯(lián)鎖表數(shù)據(jù)的安全邏輯。本文著重分析聯(lián)鎖表安全邏輯，用UML分析5個(gè)對象的交互關(guān)系，重點(diǎn)闡述聯(lián)鎖表邏輯的形式化建模與驗(yàn)證方法。主要研究路線如圖1所示。

圖1 主要研究路線

2 聯(lián)鎖表安全邏輯建模與驗(yàn)證

2.1 聯(lián)鎖表中的聯(lián)鎖邏輯

聯(lián)鎖表包含進(jìn)路、信號機(jī)、道岔及區(qū)段等信息，從進(jìn)路選排到進(jìn)路防護(hù)信號機(jī)開放主要經(jīng)過操作、選路、道岔轉(zhuǎn)動(dòng)、進(jìn)路鎖閉和信號開放5個(gè)階段。

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

圖2 F4～F6進(jìn)路示意圖

對應(yīng)以上進(jìn)路的聯(lián)鎖表信息如表1所示。

表1 亦莊站部分聯(lián)鎖表

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

2.2 UML順序圖描述聯(lián)鎖表邏輯信息

2.2.1 UML順序圖介紹

順序圖主要用二維圖來描述系統(tǒng)運(yùn)行時(shí)各對象之間的交互時(shí)序關(guān)系，可以實(shí)現(xiàn)用例的邏輯建模。主要由4個(gè)標(biāo)記符構(gòu)成：對象、生命線、消息和激活。縱向是時(shí)間軸，時(shí)間沿著生命線向下延伸，橫向則代表參與相互作用的對象。消息由一個(gè)對象的生命線指向另一個(gè)對象的生命線的直線箭頭來表示，上面注明發(fā)送的消息名。

2.2.2 聯(lián)鎖表邏輯的UML順序圖模型

由2.1聯(lián)鎖表邏輯過程分析，可以將參與聯(lián)鎖表邏輯的對象抽象為：調(diào)度員、道岔、信號機(jī)、區(qū)段和聯(lián)鎖控制器；對象之間的邏輯關(guān)系由系統(tǒng)對象間交互信息來表達(dá)。這樣就可以將聯(lián)鎖表安全邏輯轉(zhuǎn)化成在滿足約束條件關(guān)系的前提下進(jìn)行狀態(tài)轉(zhuǎn)移的關(guān)系。

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

圖3 進(jìn)程F4-F6內(nèi)部的消息傳遞示意圖

2.3 聯(lián)鎖表邏輯的CSP模型及驗(yàn)證

在用CSP對系統(tǒng)建模過程中，將每個(gè)對象的操作稱為一個(gè)進(jìn)程。因此聯(lián)鎖表邏輯被看作5個(gè)進(jìn)程間的并發(fā)交互過程。對象之間需要通過通道進(jìn)行信息交互，狀態(tài)轉(zhuǎn)換用基于CSP語義模型[5]中的跡圖表示。

2.3.1 聯(lián)鎖表邏輯的模型化

聯(lián)鎖表邏輯可以表達(dá)成5個(gè)對象之間的信息交互過程。下面分別對不同對象的動(dòng)作進(jìn)行分析，并用CSP對其建模。

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

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

同理對于信號機(jī)F4來說，接收到聯(lián)鎖控制器發(fā)來的openF4信息后開放信號機(jī)，繼而通過chS2R通道將狀態(tài)信息反饋給CI進(jìn)程。F4進(jìn)程的CSP語義描述為：

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

圖4 USER和信號機(jī)F4進(jìn)程跡圖

SWITCH進(jìn)程通過chC2S通道收到聯(lián)鎖檢查4號道岔和6號道岔的要求，操作過程中并不關(guān)注具體的時(shí)序關(guān)系，所以將道岔分別處理并看作兩個(gè)進(jìn)程，只有當(dāng)這兩個(gè)進(jìn)程都滿足條件時(shí)才能開放進(jìn)路。在CSP中可以用并發(fā)來表達(dá)嚴(yán)格同步的兩事件構(gòu)成整個(gè)系統(tǒng)的行為，并同時(shí)參與到公共事件上。

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

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

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

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

只有當(dāng)上述兩個(gè)進(jìn)程進(jìn)行到公共事件，openF4才可以發(fā)生，滿足案例的實(shí)際需求，道岔進(jìn)程的CSP最終表達(dá)式如下：

SWITCH= SWITCH4|| SWITCH6

對應(yīng)跡圖如圖5所示。

圖5 SWITCH進(jìn)程跡圖

道岔鎖閉之后，要對區(qū)段出清以及敵對進(jìn)路未建立做進(jìn)一步的確認(rèn)。這就要對Track20D對象進(jìn)行分析建模。Track20D通過chC2S通道接收聯(lián)鎖控制器發(fā)來的檢查軌道區(qū)段狀態(tài)的命令，分別檢查20D是否空閑以及敵對信號F6是否開放，對應(yīng)的CSP模型表達(dá)如下：

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

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

圖6 TRACK進(jìn)程跡圖

圖7 CI部分進(jìn)程跡圖

綜上所述，進(jìn)路F4～F6的行為就是5個(gè)對象的行為的并發(fā)組合：

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

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

2.3.2 模型的驗(yàn)證

計(jì)算機(jī)聯(lián)鎖表邏輯是行車最基礎(chǔ)的安全保證。從總體驗(yàn)證思路上，將聯(lián)鎖表邏輯的驗(yàn)證分為功能性驗(yàn)證和安全性驗(yàn)證，所謂安全性驗(yàn)證，主要是滿足列控領(lǐng)域相關(guān)要求的特殊屬性。

建模及驗(yàn)證工具ProB[6]為聯(lián)鎖邏輯提供針對不同性質(zhì)便捷的模型驗(yàn)證技術(shù)，像死鎖、活鎖，可達(dá)性，線性時(shí)序邏輯（LTL，linear temporal logic）[7]，優(yōu)化驗(yàn)證和可能性模型驗(yàn)證，此工具通過深度和廣度優(yōu)先搜索，遍歷模型中所有狀態(tài)節(jié)點(diǎn)，以快速找出存在問題節(jié)點(diǎn)的最短路徑。

（1）功能性驗(yàn)證

功能性驗(yàn)證主要是從模型性質(zhì)的角度對系統(tǒng)進(jìn)行驗(yàn)證，保證所有節(jié)點(diǎn)的狀態(tài)轉(zhuǎn)移

#assert System() deadlockfree;

死鎖狀態(tài)是指無法成功終止一個(gè)不可動(dòng)的狀態(tài)。#assert System() divergencefree;

活鎖狀態(tài)是指給定一個(gè)進(jìn)程，它一直在內(nèi)部轉(zhuǎn)換，無法到達(dá)有用的事件。

#assert System() deterministic;

確定性是指給定一個(gè)進(jìn)程，如果它是確定性的，那么不論任何狀態(tài)，一個(gè)事件不會遷移到兩個(gè)狀態(tài)。

（2）安全性驗(yàn)證

聯(lián)鎖作為安全苛求系統(tǒng)，其中聯(lián)鎖表的安全邏輯反應(yīng)了系統(tǒng)的可靠性和安全性，是安全性驗(yàn)證的重點(diǎn)。在進(jìn)路建立的過程中，主要關(guān)注以下3方面：進(jìn)路道岔及防護(hù)道岔被鎖閉；進(jìn)路區(qū)段空閑且解鎖；敵對進(jìn)路未建立。用LTL語言來描述進(jìn)路需要滿足的安全條件。

a.驗(yàn)證當(dāng)進(jìn)路上所有道岔位置正確且鎖閉時(shí)進(jìn)路才能建立，針對F4～F6進(jìn)路，即當(dāng)?shù)啦?、道岔6分別在定位且鎖閉時(shí)進(jìn)路建立，信號機(jī)F4才能開放。對應(yīng)LTL表達(dá)式：

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

b.驗(yàn)證進(jìn)路對應(yīng)區(qū)段空閑才能建立進(jìn)路，進(jìn)路F4～F6要檢查的區(qū)段是20D，相應(yīng)的LTL表達(dá)式：

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

c.要驗(yàn)證任意兩條敵對進(jìn)路不能同時(shí)建立，容易從聯(lián)鎖表中找到進(jìn)路F4～F6的敵對進(jìn)路信號為F6，將關(guān)系寫成LTL表達(dá)式：

notG([F4opened]&[F6open])

在ProB中將聯(lián)鎖表中每一條進(jìn)路按上述安全條件列舉，逐項(xiàng)驗(yàn)證性質(zhì)，得到的結(jié)果中若沒有反例以證明模型的安全性，從而通過證明模型的正確性追溯到聯(lián)鎖表數(shù)據(jù)安全邏輯的正確性。

（3）結(jié)果分析

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

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

3 結(jié)束語

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

[1]宿浩峰.城市軌道交通聯(lián)鎖系統(tǒng)建模的研究[D].杭州：浙江大學(xué)，2012.

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

[3]孫 麒，張?jiān)迫A.基于CSP的形式化方法研究[J].浙江理工大學(xué)學(xué)報(bào)，2009，26（4）：557-560.

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

[5]屈延文.形式語義學(xué)基礎(chǔ)與形式說明[M].北京：科學(xué)出版社，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并發(fā)系統(tǒng)驗(yàn)證研究[J].計(jì)算機(jī)科學(xué)，2012，39（12）：125-132.

責(zé)任編輯 陳 蓉

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

北京市科委項(xiàng)目（KWH13001531）；軌道交通北京實(shí)驗(yàn)室項(xiàng)目（W13H100061）。

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