城軌計算機聯(lián)鎖的數(shù)據(jù)安全性驗證

周 果，趙會兵

(北京交通大學(xué) 電子信息工程學(xué)院，北京 100044)

數(shù)據(jù)是關(guān)系信號系統(tǒng)安全性的關(guān)鍵因素之一。以“4·28”事故[1]為例，由于安全數(shù)據(jù)沒有被嚴格跟蹤保護和驗證，包括線路限速信息和關(guān)鍵調(diào)度命令在內(nèi)的靜態(tài)安全關(guān)鍵數(shù)據(jù)沒有依據(jù)嚴格的規(guī)程在系統(tǒng)中傳遞，而是被錯誤修改或漏發(fā)，最終導(dǎo)致脫軌相撞事故的發(fā)生。而在“7·23”事故[2]中，由于列控中心軌道電路狀態(tài)采集器中表征軌道占用狀態(tài)的動態(tài)安全關(guān)鍵數(shù)據(jù)在雷擊故障后繼續(xù)保持了錯誤的且未更新的占用狀態(tài)數(shù)據(jù)，加之調(diào)度人員的失誤，使得后方的D301次列車無法得知前方D3115次列車的占用情況，最終導(dǎo)致追尾事故的發(fā)生。由以上事故可見，數(shù)據(jù)安全性是信號系統(tǒng)安全保障中的關(guān)鍵任務(wù)。

城軌計算機聯(lián)鎖是典型的數(shù)據(jù)驅(qū)動信號系統(tǒng)，以傳統(tǒng)系統(tǒng)安全理念來看，需要對聯(lián)鎖軟件和硬件及它們的集成分別進行安全性分析和驗證才能證明系統(tǒng)的安全完整性，數(shù)據(jù)安全并不是以一個完整的領(lǐng)域任務(wù)呈現(xiàn)在系統(tǒng)安全的工作中，而是零散地融合在軟件、硬件和系統(tǒng)的安全工程中。由于城軌聯(lián)鎖數(shù)據(jù)種類的多樣性和邏輯關(guān)系的復(fù)雜性，且數(shù)據(jù)安全尚沒有成熟完整的理論支撐，也沒有支撐實際工程應(yīng)用的工具，使得對數(shù)據(jù)安全性進行系統(tǒng)化的建模和驗證變得更加困難，這種數(shù)據(jù)安全驗證任務(wù)在系統(tǒng)安全工程中的缺失很可能會帶來不可接受的風(fēng)險[3]。

1 信號系統(tǒng)的數(shù)據(jù)安全

由于技術(shù)演進的歷史原因，信號系統(tǒng)的信息化水平得到快速發(fā)展，業(yè)內(nèi)主要投入資源在裝備研發(fā)方面的這種現(xiàn)狀是可以理解的。相應(yīng)的，對信號系統(tǒng)安全性的關(guān)注則仍然拘泥于傳統(tǒng)系統(tǒng)安全工程中軟硬件系統(tǒng)工程的框架內(nèi)，業(yè)界剛剛關(guān)注到數(shù)據(jù)安全性需求方面的迫切性。在《列控數(shù)據(jù)管理暫行辦法》[4]中規(guī)范了各類數(shù)據(jù)管理的責(zé)任分工，并提出以工作表方式管理數(shù)據(jù)，但并未從整體上提出具體的技術(shù)層面理論指導(dǎo)。

數(shù)據(jù)安全是指數(shù)據(jù)的創(chuàng)造、維護、使用和保護不會帶來不可接受的風(fēng)險。由于信號系統(tǒng)數(shù)據(jù)驅(qū)動的特點越來越明顯，學(xué)界提出了數(shù)據(jù)安全性的概念，與既有的傳統(tǒng)系統(tǒng)安全概念體系形成補充。雖然在行業(yè)標(biāo)準EN 50128[5]中都將數(shù)據(jù)作為軟件需要關(guān)注的項提出，并要求驗證數(shù)據(jù)的正確性和完整性，但未給出如何開展數(shù)據(jù)安全工程的技術(shù)指導(dǎo)。在SCSC組織提出的數(shù)據(jù)安全指南[3]中首次系統(tǒng)性地建立了數(shù)據(jù)安全工程的概念體系，該指南指出，數(shù)據(jù)安全性與軟件和硬件的安全性同樣是系統(tǒng)安全的重要組成部分。

數(shù)據(jù)安全性由于數(shù)據(jù)作用的不同，其驗證手段亦不同。信號系統(tǒng)的數(shù)據(jù)按照它們在系統(tǒng)中的作用可總結(jié)為以下4類：

(1)環(huán)境數(shù)據(jù)：用來提供系統(tǒng)運行環(huán)境中的各種信息，如線路拓撲信息、工務(wù)線路數(shù)據(jù)、車載設(shè)備配置信息、車輛信息等。

(2)運營數(shù)據(jù)：用來記錄和規(guī)劃系統(tǒng)運營任務(wù)和運營狀態(tài)，如時刻表數(shù)據(jù)、信號集中監(jiān)測數(shù)據(jù)、運營維護記錄等。

(3)狀態(tài)數(shù)據(jù)：用來表征系統(tǒng)運行的實時動態(tài)狀態(tài)，如列車位置和速度、MA的生成、進路、軌道占用狀態(tài)、無線通信實時時間等。

(4)干預(yù)數(shù)據(jù)：用來干預(yù)特殊需求時的列車運行，如臨時限速信息、無線調(diào)車命令、降級服務(wù)時的電話閉塞、人工參與的模式轉(zhuǎn)換命令等。

信號系統(tǒng)是典型的大規(guī)模復(fù)雜系統(tǒng)，需要依賴系統(tǒng)工程方法指導(dǎo)系統(tǒng)的研發(fā)、應(yīng)用和維護，對信號系統(tǒng)中的眾多數(shù)據(jù)進行生成、配置、變更和銷毀，數(shù)據(jù)安全性應(yīng)與信號系統(tǒng)全生命周期相適應(yīng)。作為典型的信號系統(tǒng)，計算機聯(lián)鎖的數(shù)據(jù)安全性研究需求更為迫切。文獻[6]論述了信號系統(tǒng)中典型的數(shù)據(jù)錯誤及數(shù)據(jù)安全對信號系統(tǒng)的重要性。文獻[7]應(yīng)用高階邏輯的方法證明聯(lián)鎖數(shù)據(jù)的正確性。歐盟眾多研究機構(gòu)參與研究統(tǒng)一鐵路系統(tǒng)數(shù)據(jù)存儲格式并提出以XML為基礎(chǔ)擴展的鐵路系統(tǒng)數(shù)據(jù)交互語言RailML，文獻[8]以荷蘭某典型車站的聯(lián)鎖系統(tǒng)RailML數(shù)據(jù)庫為例進行了安全性實例驗證。文獻[9]對聯(lián)鎖線路中的所有元素進行了分類，并將多種元素模型統(tǒng)一到節(jié)點的聯(lián)通關(guān)系中，以關(guān)聯(lián)矩陣算法進行進路數(shù)據(jù)安全性驗證。文獻[10]以點集拓撲學(xué)為基礎(chǔ)，對列車經(jīng)過的線路信號元素進行模塊化建模，定義獨立單元標(biāo)準占用狀態(tài)的狀態(tài)變量，證明了行車許可動態(tài)數(shù)據(jù)生成算法的正確性。文獻[11]以CBTC系統(tǒng)為例，以SAT形式化模型為手段，驗證了線路數(shù)據(jù)連通性關(guān)系的安全性。以上研究通過建模雖然減弱了線路數(shù)據(jù)的復(fù)雜性，但均未明確闡述聯(lián)鎖中各類數(shù)據(jù)之間的關(guān)系模型，且主要的驗證均局限于數(shù)據(jù)生成過程中的一致性，未對數(shù)據(jù)間的相互交叉約束關(guān)系進行驗證。

本文在環(huán)境數(shù)據(jù)即線路數(shù)據(jù)建模的基礎(chǔ)上，提出以城軌聯(lián)鎖進路中元素之間的相互交叉約束關(guān)系為對象，以圖搜索算法和內(nèi)積法為手段的聯(lián)鎖數(shù)據(jù)安全驗證方法，技術(shù)組成如圖1所示。首先，對數(shù)據(jù)模型進行建模，定義線路數(shù)據(jù)的存儲方式，以此為基礎(chǔ)建立線路數(shù)據(jù)表。其次，定義三類數(shù)據(jù)關(guān)系，以點點關(guān)系和點線關(guān)系為基礎(chǔ)，定義道岔和閉塞分區(qū)在進路中的連通關(guān)系，并作為線線關(guān)系規(guī)則的輸入，定義進路與進路之間的敵對約束關(guān)系。第三，針對三類關(guān)系，以進路方向分類分步驗證數(shù)據(jù)的安全性。

圖1 聯(lián)鎖數(shù)據(jù)安全性驗證框架

2 城軌計算機聯(lián)鎖數(shù)據(jù)的建模

2.1 各類聯(lián)鎖相關(guān)數(shù)據(jù)

在基于通信的列控系統(tǒng)CBTC中，線路數(shù)據(jù)Layout是開發(fā)城軌計算機聯(lián)鎖應(yīng)用的環(huán)境數(shù)據(jù)輸入，根據(jù)線路數(shù)據(jù)設(shè)計聯(lián)鎖進路，并以聯(lián)鎖數(shù)據(jù)表或進路圖的形式表示出來。線路數(shù)據(jù)包含的數(shù)據(jù)眾多，其中與聯(lián)鎖相關(guān)的部分有節(jié)點Node、道岔Switch、區(qū)段Segment、閉塞分區(qū)Block、軌道Track、計軸Axle Counter、區(qū)域控制器Zone Controller、信號機Signal、里程Chainage等信息。本文以典型雙開道岔組成的城軌線路為例，首先定義在驗證算法中涉及的各類數(shù)據(jù)模型，如圖2所示。

圖2 線路數(shù)據(jù)關(guān)鍵信息

定義1：節(jié)點集合Node中的元素是一個十一元組，其中：

(1)Nod表示線路中的節(jié)點的名稱；

(2)T表示節(jié)點的類型，節(jié)點為道岔時取為0，為軌道盡頭時取為1；

(3)SW表示道岔名稱，當(dāng)T=0時，SW≠null，當(dāng)T=1時，SW=null；

(4)ZCN表示節(jié)點所在的區(qū)域控制器；

(5)Ori表示道岔岔尖的方向類型，當(dāng)T=0時，Ori≠null，此時沿道岔岔尖觀察道岔，如果定位和反位翼軌端點里程坐標(biāo)相對岔尖軌端點里程坐標(biāo)增加，則為上行道岔，取值為Ori=0，反之為下行道岔，取值為Ori=1；當(dāng)T=1時，Ori=null，如圖2中道岔①為下行道岔，道岔②為上行道岔；

(6)Dir表示道岔翼軌方向類型，當(dāng)T=0時，Dir≠null，此時如果道岔翼軌處在定位時，取值為tangent，處于反位時，取值為turnout；當(dāng)T=1時，Ori=null；

(7)ToeSeg、 TanSeg、 TurSeg分別表示岔尖軌、定位翼軌、反位翼軌所在的區(qū)段，當(dāng)T=1時，ToeSeg、TanSeg、TurSeg=null；

(8)CoN表示節(jié)點的里程坐標(biāo)；

(9)B表示道岔所在的閉塞分區(qū)，當(dāng)T=1時，B=null。

定義2：區(qū)段集合Segment中的元素是一個三元組，其中：

(1)Seg表示區(qū)段的名稱；

(2)StaN、EndN∈Node分別表示區(qū)段起點節(jié)點和終點節(jié)點。

定義3：閉塞分區(qū)集合Block中的元素是一個六元組，其中：

(1)Blo表示閉塞分區(qū)的名稱；

(2)StaAC和EndAC分別表示閉塞分區(qū)中處于直向軌道上的兩個端點計軸；

(3)TurAC1和TurAC2分別表示閉塞分區(qū)中處于側(cè)向軌道上的端點計軸，當(dāng)閉塞分區(qū)中不包含任何道岔時，TurAC1、TurAC2=null；當(dāng)閉塞分區(qū)中包含一個道岔時，TurAC1≠null，TurAC2=null；當(dāng)閉塞分區(qū)中包含兩個道岔時，TurAC1、TurAC2≠null；

(4)ZCB表示閉塞分區(qū)所在的區(qū)域控制器。

定義4：信號機集合Signal中的元素是一個五元組，其中：

(1)Sig∈Signal表示信號機名稱；

(2)AC表示信號機對應(yīng)的計軸點；

(3)SegIn∈Segment表示信號機所在的軌道區(qū)段；

(4)ZCS表示信號機所在的區(qū)域控制器；

(5)CoS表示信號機所在的里程位置。

以上信息元素正是構(gòu)成線路數(shù)據(jù)的基本元素，而計算機聯(lián)鎖使用的進路是線路數(shù)據(jù)的子集，包括主體進路和防護進路兩部分，主體進路是一條從起點信號機到終點信號機的通路。固定閉塞模式下防護進路由若干閉塞分區(qū)組成，這些閉塞分區(qū)的總長足以保證列車過沖主體進路終點信號機時列車可安全停在防護進路范圍之內(nèi)。移動閉塞模式下不設(shè)置防護進路。進路信息構(gòu)成包括：

(1)進路名稱：信號機到信號機(例X1403-X1401R)，覆蓋主體進路和防護進路(固定閉塞模式下)。

(2)信號機：起點信號機和終點信號機對應(yīng)主體進路的起點和終點。

(3)防護進路：為防護列車以最差情況過沖終點信號機所設(shè)置的進路。

(5)主體進路和防護進路道岔位置：定位(Tangent，Normal)和反位(Turnout，Reverse)。

(6)主體進路和防護進路的側(cè)防道岔位置：定位和反位。

(7)主體進路和防護進路側(cè)防道岔的解鎖條件：進路識別中由道岔或渡線引入的側(cè)向危險，找到它們對應(yīng)的主體進路覆蓋的閉塞分區(qū)，這些閉塞分區(qū)需出清。

(8)主體進路和防護進路覆蓋的閉塞分區(qū)：由計軸分隔的軌道空間。

以上數(shù)據(jù)的構(gòu)成決定了進路對線路數(shù)據(jù)的存儲和訪問方式，由于道岔中岔尖軌和翼軌只能以非銳角夾角通過，因此根據(jù)圖論中的定義，線路圖是以道岔或軌道端點為節(jié)點，以區(qū)段為邊組成的有向圖，對進路做如下定義。

定義5：進路集合Route中的元素是一個十一元組，其中：

(1)m_StaSig、m_EndSigSignal分別表示主體進路的起點信號機和終點信號機,m_StaSig≠m_EndSig；

(2)RD表示進路的方向，RD=0時表示上行，RD=1時表示下行；

舟曲特大泥石流因其規(guī)模之巨、傷亡之大，已成為人類地質(zhì)災(zāi)害史上的重大事件，從公共危機管理的角度如何預(yù)防泥石流災(zāi)害很值得反思。

(3)m_S?Node和m_FlankS?Node分別表示主體進路中道岔的集合和主體進路側(cè)防道岔的集合；

(4)o_S?Node和o_FlankS?Node分別表示防護進路中道岔的集合和防護進路側(cè)防道岔的集合；

(5)m_FSR?Block和o_FSR?Block分別表示主體進路側(cè)防道岔解鎖需出清閉塞分區(qū)集合和防護進路側(cè)防道岔解鎖需出清閉塞分區(qū)集合；

(6)m_Block?Block和o_Block?Block分別表示主體進路和防護進路覆蓋的閉塞分區(qū)集合。

2.2 數(shù)據(jù)關(guān)系模型

僅僅定義數(shù)據(jù)結(jié)構(gòu)模型是不夠的，還需定義數(shù)據(jù)之間的關(guān)系，數(shù)據(jù)在關(guān)系中形成約束是設(shè)計算法的基礎(chǔ)。因此，對進路信息進行分類，數(shù)據(jù)關(guān)系可分為3類，見表1。

表1 進路數(shù)據(jù)關(guān)系

“點點關(guān)系”指進路信息中數(shù)據(jù)的連通關(guān)系，以及實現(xiàn)這種連通性需要的各種條件，如道岔位置和進路的方向，這是進路的本質(zhì)，即在平面上兩點之間通過何種方式連通，屬于拓撲關(guān)系。該關(guān)系以進路包含的信息為主體(此處將“主體進路”和“防護進路”統(tǒng)稱為“進路”)，如圖3(a)所示，在圖中紅色箭頭表示進路，黑色節(jié)點表示道岔，注意圖中并不是針對某一特定道岔位置而形成的進路，只表示連通關(guān)系，進路不一定是直向的。由此定義關(guān)系規(guī)則如下。

圖3 數(shù)據(jù)關(guān)系模型

關(guān)系1：點點關(guān)系規(guī)定了線路布局中起止信號機之間的聯(lián)鎖進路有且只有一條，進路定義后，進路中所有信息唯一確定。

“點線關(guān)系”指非進路經(jīng)過的節(jié)點與進路之間的關(guān)系，該關(guān)系的主體是側(cè)面防護信息，即側(cè)面的潛在威脅道岔及其位置，該關(guān)系的本質(zhì)是至少存在一條區(qū)段與進路相交，屬于幾何關(guān)系。該關(guān)系中包括信息為相交區(qū)段的端點即道岔及其所在的防護位置。關(guān)系圖如圖3(b)所示,由此定義關(guān)系規(guī)則如下。

關(guān)系2：點線關(guān)系規(guī)定了進路如果存在由區(qū)段相交引入的進路側(cè)防信息，則該信息唯一確定。

“線線關(guān)系”指進路與進路之間的關(guān)系，該關(guān)系的主體是進路與進路之間是否存在道岔位置敵對和進路方向敵對，屬于條件關(guān)系。道岔位置敵對進路的本質(zhì)是滿足以下兩個條件：兩進路主體或防護部分所經(jīng)過的道岔或側(cè)防道岔組成的道岔集合之間存在交集；該交集內(nèi)的道岔在兩進路的主體或防護部分的“點點關(guān)系”和“點線關(guān)系”數(shù)據(jù)中不一致。線路方向敵對進路的本質(zhì)是滿足以下3個條件：兩進路方向數(shù)據(jù)不等；兩進路主體或防護部分覆蓋的閉塞分區(qū)數(shù)據(jù)存在交集；進路中道岔和側(cè)防道岔均不存在道岔位置沖突。關(guān)系圖如圖3(c)所示,進路1對道岔1的位置要求在反位，而進路2對道岔1的位置要求在定位，進路1對道岔2的位置要求在反位，而進路2對道岔2的位置要求在定位(側(cè)防)，因此進路1和2構(gòu)成位置敵對關(guān)系。由此定義關(guān)系規(guī)則如下。

關(guān)系3：線線關(guān)系規(guī)定了進路之間位置敵對和方向敵對關(guān)系存在且唯一確定。

3 三類關(guān)系的安全性驗證算法

數(shù)據(jù)安全驗證的目的是檢查由聯(lián)鎖設(shè)計導(dǎo)出的進路數(shù)據(jù)及它們之間關(guān)系的正確性和完整性。正確性是指數(shù)據(jù)中是否存在設(shè)計進路信息錯誤，或進路信息和線路信息不一致；完整性是指數(shù)據(jù)中是否存在信息的遺漏。因此，為克服人工數(shù)據(jù)驗證的巨大工作量和易錯的缺點，設(shè)計算法過程中需兼顧正確性和完整性。注意，由于防護進路與主體進路驗證方法類似，下行進路與上行進路驗證方法類似，進路閉塞分區(qū)和進路道岔的驗證方法類似，本文不再做重復(fù)論述。

3.1 “點點關(guān)系”的安全性驗證關(guān)鍵算法

算法1

輸入：rou.m_StaSig,rou.m_EndSig，其中rou∈m_Route；

輸出：rou.RD,rou.m_S.SW (進路方向及進路上的所有道岔);//判斷進路方向

If SearchSignal(rou.m_StaSig).CoS-SearchSignal(rou.m_EndSig).CoS>0 then

rou.RD←1 else rou.RD←0

//搜索進路經(jīng)過的道岔，以上行進路為例，下行進路及防護進路算法類似

If rou.RD =0 then

If SearchSignal(rou.m_StaSig).SegIn=SearchSignal(rou.m_EndSig).SegIn then

rou.m_S←null

else

StartNodeInR,EndNodeInR∈Node

StartNodeInR←SearchSignal(rou.m_StaSig).SegIn.EndN

EndNodeInR←SearchSignal(rou.m_EndSig).SegIn.StaN

CurrentNode(0)← StartNodeInR

Stack(0) ← empty

Do until Stack(k) =null

If SearchNode(CurrentNode(i).Nod).T =switch & CurrentNode(i).Ori=0 then

AdjacentNode(0)←SeachSegment(CurrentNode(i).TanSeg).EndN

AdjacentNode(1)←SeachSegment(CurrentNode(i).TurSeg).EndN

If SearchNode(CurrentNode(i).Nod).T=switchAnd CurrentNode(i).Ori=1 then

AdjacentNode(0)←SeachSegment(CurrentNode(i).ToeSeg).EndN

AdjacentNode(1)←null

If CurrentNode(i).ZCN≠StartNodeInR.ZCN Or Accessed (i)=1 then

AdjacentNode(0)←null,AdjacentNode(1)←null

If AdjacentNode(1)≠null thenk++,Stack(k)←AdjacentNode(1)

If CurrentNode(i).Nod=EndNodeInR then Exit Do

else

if adjacentNode(0) ≠null theni++

CurrentNode(i).Nod←adjacentNode(0)

else CurrentNode(i).Nod←Stack(k),i←k,k--

Accessed(i)←1

Loop

rou.m_S←CurrentNode(i)

證明：當(dāng)SearchSignal(rou.m_StaSig).SegIn=SearchSignal(rou.m_EndSig).SegIn時，起止信號機之間的通路不經(jīng)過任何節(jié)點，即與道岔和側(cè)防道岔相關(guān)的數(shù)據(jù)rou.m_S為空。

以上行進路為例，當(dāng)起止信號機所在的區(qū)段不同時，對CurrentNode(i)，當(dāng)i=0時，CurrentNode(0)= StartNodeInR，顯然為進路經(jīng)過的第一個道岔。

假設(shè)當(dāng)i=n，n∈N時，CurrentNode(n)是進路經(jīng)過的道岔；當(dāng)i=n+1時，對非本ZC內(nèi)的節(jié)點、已搜索過的節(jié)點和非道岔節(jié)點均置空。

如果CurrentNode(n+1)=EndNodeInR，即為進路的終節(jié)點，則關(guān)系1可知i=n+1時圖搜索路徑唯一，算法成立。如果CurrentNode(n+1)≠EndNodeInR，且定位股所在區(qū)段的終點非空，則CurrentNode(n+1)=AdjacentNode(0)；如果此時定位股所在區(qū)段的終點為空，則取堆棧模擬數(shù)組中的最后一個元素，即CurrentNode(n+1)=Stack(k),為最后一個反位股終點節(jié)點，算法可不重復(fù)遍歷所有本ZC內(nèi)的節(jié)點，CurrentNode(n)為進路上的道岔，則直向相鄰節(jié)點AdjacentNode(0)和數(shù)組Stack(k)中的側(cè)向節(jié)點必存在進路上的節(jié)點，即由關(guān)系1可知i=n+1時圖搜索路徑唯一，算法成立。

因此，由歸納法可知CurrentNode(i)即為進路上的所有道岔集合，算法成立。

對下行進路證明類似，在得到進路上的所有道岔后，可依據(jù)道岔之間的連接關(guān)系判斷各道岔的位置，進路經(jīng)過的閉塞分區(qū)的搜索算法思路與道岔的搜索類似，不再敖述。

3.2 “點線關(guān)系”的安全性驗證關(guān)鍵算法

“點線關(guān)系”規(guī)定了側(cè)向危險以交叉的方式與進路發(fā)生沖撞的關(guān)系，這種關(guān)系的本質(zhì)是在本ZC中存在一條或多條與進路相交的區(qū)段，相交方式分為道岔引入和渡線引入兩類，首先給出如下定理。

定理1：某道岔對進路構(gòu)成側(cè)向危險的充要條件是該道岔的岔尖軌或翼軌所在區(qū)段必與進路相交，且交點必在道岔點上或渡線交點上。

證明：充分性。進路由線段組成，線段的端點包括起止信號機和道岔點。對上行進路中的任意一段進路RouteSeg(i)而言，如果區(qū)域中存在與進路相交的區(qū)段，則：

當(dāng)交點位于RouteSeg(i)端點上時，設(shè)進路經(jīng)過道岔SW(i)，設(shè)道岔的岔尖股為SW(i).ToeSeg，定位股和反位股為SW(i).TanSeg和SW(i).TurSeg。此時如果進路中道岔位置為SW(i).Pos=tangent，即進路占據(jù)tangent方向的股道，則危險必由turnout引入，此時SW(i).TurSeg與進路相交且交點在道岔SW(i)上，因此端點SW(i).TurSeg.StaN(下行道岔)或SW(i).TurSeg.EndN(上行道岔)對應(yīng)的道岔為側(cè)防道岔。此時如果進路中道岔位置為SW(i).Pos=turnout，即進路占據(jù)turnout方向的股道，則危險必由tangent引入，此時SW(i).TanSeg與進路相交且交點在道岔SW(i)上，因此端點SW(i).TanSeg.StaN(下行道岔)或SW(i).TanSeg.EndN(上行道岔)對應(yīng)的道岔為側(cè)防道岔。

當(dāng)交點位于RouteSeg(i)之間時，設(shè)與其相交的區(qū)段為SegCross(i)，由于區(qū)段的定義，區(qū)段內(nèi)部無節(jié)點，即此時交點不是節(jié)點，而是交叉渡線的交點，此時區(qū)段端點SegCross(i).StaN和SegCross(i).EndN對應(yīng)的道岔均為側(cè)防道岔。對下行進路證明類似。

必要性。不論進路方向如何，若道岔m_FlankS(i)是某進路的側(cè)防道岔，即其他列車可經(jīng)過該道岔與當(dāng)前進路相沖撞，顯然該道岔的岔尖股或定位股或反位股與進路相交。由區(qū)段的定義可知，區(qū)段內(nèi)無節(jié)點，則交點必在區(qū)段端點上，或區(qū)段內(nèi)非道岔的交點即交叉渡線交點上。

由定理1的證明可知，側(cè)向危險由兩類相交引入，即道岔引入和渡線引入，本質(zhì)都為存在與進路相交的軌道區(qū)段，區(qū)別只在于交點落在何處。因此，檢查“點線關(guān)系”時，算法設(shè)計應(yīng)分別對兩類相交進行驗證。由于道岔引入判交算法，只需沿進路經(jīng)過的道岔依次搜索，先判斷出該道岔在進路中的位置要求，確定其相斥道岔位置，搜索在該相斥道岔位置對應(yīng)的股道所連接的道岔即可，該算法較為簡單，這里不再論述，只對渡線引入的側(cè)防判決算法做如下論述。

算法2

輸入：rou.m_S (算法1的輸出CurrentNode(i))，RouteSeg(進路線段集合)，SegInZC(區(qū)域內(nèi)所有區(qū)段集合)；

輸出：rou.m_FlankS (進路中由渡線交叉引入的側(cè)防道岔) ；

// 設(shè)RouteSeg(i)為進路的一段，以上行進路為例，下行進路及防護進路算法類似

If rou.RD=0 then

If SearchSignal(rou.m_StaSig).SegIn=SearchSignal(rou.m_EndSig).SegIn then

rou.m_FlankS←null,rou.m_FSR←null

else

Do until routeSeg(i)=null

Do until SegInZC(j)=null

a1←Vector(SegInZC(j).StaN,SegInZC(j).EndN)×

Vector(SegInZC(j).StaN,RouteSeg(i).StaN)

a2←Vector(SegInZC(j).StaN,SegInZC(j).EndN)×

Vector(SegInZC(j).StaN,RouteSeg(i).EndN)

b1←Vector(RouteSeg(i).StaN,RouteSeg(i).EndN)×Vector(RouteSeg(i).StaN,SegInZC(j).StaN)

b2←Vector(RouteSeg(i).StaN,RouteSeg(i).EndN)×Vector(RouteSeg(i).StaN,SegInZC(j).EndN)

Ifa1·a2<0 Andb1·b2<0 then

SegInZC(j).StaN,SegInZC(j).EndN ∈rou.m_FlankS

j++

Loop

i++

Loop

證明：已知側(cè)向危險為交叉渡線引入，設(shè)進路分段集合RouteSeg(i)表示由起止信號機和進路中道岔組成的進路線段，SegInZC(j)表示本ZC中所有區(qū)段集合。對任意一條進路線段RouteSeg(i)和任意一條區(qū)段SegInZC(j)，設(shè)向量

r1=(SegInZC(j).StaN,SegInZC(j).EndN)

r2=(SegInZC(j).StaN,RouteSeg(i).StaN)

r3= (SegInZC(j).StaN,RouteSeg(i).EndN)

因此，渡線引入的側(cè)防判決算法成立。

圖4 線段判交算法

3.3 “線線關(guān)系”的安全性驗證關(guān)鍵算法

“線線關(guān)系”規(guī)定了敵對進路的類型，即道岔位置敵對和進路方向敵對。在經(jīng)過3.1節(jié)和3.2節(jié)中的算法驗證后，以正確的進路數(shù)據(jù)為基礎(chǔ)，作為本算法的輸入，驗證進路之間的敵對關(guān)系數(shù)據(jù)是否正確。

算法3

輸入：rouRoute；m_S,m_FlankS,m_FSR,o_S,o_FlankS,o_FSR,m_Block,o_Block；

輸出：PosConfRou(位置敵對進路集合)，DirConfRou(方向敵對進路集合)；

Do until rou(i)=null

Do until rou(j)=null

If rou(j).RD= rou(i).RD then

If rou(j).m_S.Dir≠rou(i).m_S.Dir Or

rou(j).m_FlankS.Dir≠rou(i).m_FlankS.Dir Or rou(j).o_S.Dir≠rou(i).o_S.Dir Or

rou(j).o_FlankS.Dir≠rou(i).o_FlankS.Dir then rou(j) ∈PosConfRou

j++

else

If (rou(j).m_Block∪rou(i).o_Block)∩

(rou(j).m_Block∪rou(i).m_Block)≠? then rou(j) ∈DirConfRou

j++

Loop

i++

Loop

算法根據(jù)定義設(shè)計，顯然成立，證明略。

4 南京城軌某線聯(lián)鎖數(shù)據(jù)安全驗證

根據(jù)以上建模和算法，以VBA和VC++兩種方式開發(fā)了驗證工具，以表形式存儲數(shù)據(jù)，依據(jù)標(biāo)準EN 50128[5]中的要求，對南京城軌某線聯(lián)鎖數(shù)據(jù)進行安全性交叉驗證。

開發(fā)自動化工具的目的是為了克服人工檢查工作效率過低且會導(dǎo)致檢查遺漏和錯誤的不足，軟件設(shè)計依據(jù)需求分析、架構(gòu)設(shè)計、詳細設(shè)計、代碼實現(xiàn)和驗證測試的軟件工程過程開展，軟件命名為進路數(shù)據(jù)安全驗證工具RDSV(Route Data Safety Verifier)，對線路原始數(shù)據(jù)進行轉(zhuǎn)換和存儲，識別數(shù)據(jù)之間的邏輯制約關(guān)系，建立數(shù)據(jù)與數(shù)據(jù)之間的約束規(guī)則，尋找判斷三類關(guān)系的充分必要條件，自動化地遍歷所有的數(shù)據(jù)，實現(xiàn)安全驗證的功能。

RDSV總體任務(wù)框架如圖5所示，針對任務(wù)不同階段分為4步完成。

步驟1數(shù)據(jù)讀取與預(yù)處理。任務(wù)：生成主體進路名和防護進路名。

步驟2生成進路信息及側(cè)防信息。任務(wù)：生成主體進路和防護進路的道岔及道岔位置，進路覆蓋的區(qū)間信息；生成主體進路和防護進路的側(cè)防道岔及道岔位置，側(cè)防道岔解鎖條件。

步驟3生成敵對進路信息。任務(wù)：生成道岔位置敵對進路和線路方向敵對進路信息。

步驟4結(jié)果比對。任務(wù)：生成自動計算結(jié)果與設(shè)計輸出的進路表之間的差異，并區(qū)別顯示。

南京城軌某線包含了典型的站場設(shè)計，道岔均為雙開道岔，線路中包含8個ZC，21個車站，160個信號機，65個道岔，全線設(shè)計進路約300條，包括固定閉塞進路和移動閉塞進路，采用人工方式進行聯(lián)鎖進路數(shù)據(jù)的驗證，效率低下且容易出錯。

首先使用工具RDSV對南京城軌某線聯(lián)鎖進路數(shù)據(jù)進行數(shù)據(jù)生成和錯誤搜索。在本文中預(yù)先將一些典型的數(shù)據(jù)故意修改為錯誤數(shù)據(jù)，注入到原本正確的已經(jīng)過嚴格檢查的進路數(shù)據(jù)表中，這樣就可以對錯誤數(shù)據(jù)進行搜索并區(qū)別顯示在結(jié)果中，工具搜索實驗結(jié)果如圖6所示，實驗結(jié)果表明自動搜索結(jié)果與預(yù)先注入的錯誤數(shù)據(jù)位置一致。

以圖7典型線路中的3條進路為例，說明數(shù)據(jù)關(guān)系。進路①中終點信號機X1509與起點信號機X1503的里程差值為37 684.073 m-37 429.690 m=254.383 m>0，進路①是一條上行進路。進路經(jīng)過的道岔為道岔SW1501，道岔位置為定位，主體進路覆蓋閉塞分區(qū)(GD1501,G1507)。防護進路覆蓋閉塞分區(qū)(GD1509,G1511)，防護進路經(jīng)過道岔SW1509，道岔位置為定位。主體進路側(cè)防道岔為道岔SW1503、SW1506、SW1505，其中SW1503可由岔尖股引入側(cè)面危險，無論設(shè)定為定位還是反位都不能防護，所以這種情況統(tǒng)一設(shè)定為定位，此時對SW1506設(shè)置為定位，SW1505設(shè)置為反位。防護進路側(cè)防道岔為SW1507，設(shè)置為定位。

圖6 RDSV搜索試驗結(jié)果

圖7 進路數(shù)據(jù)關(guān)系舉例

進路②中終點信號機X1504與起點信號機X1507的里程差值為37 301.510 m-37 544.105 m=-242.595 m<0，進路②是一條下行進路。進路中經(jīng)過的道岔為道岔SW1505、SW1504、SW1502，道岔位置均為反位，主體進路覆蓋閉塞分區(qū)(GD1503-1505,GD1504-1506,GD1502,G1504)。主體進路側(cè)防道岔為道岔SW1503、SW1506、SW1501，由于交叉渡線的存在，道岔SW1503和SW1506不論設(shè)定為定位還是反位都無法防護側(cè)面危險，所以這種情況統(tǒng)一設(shè)定為定位，此時對SW1503和SW1506均設(shè)置為定位；道岔SW1501在道岔SW1503所在閉塞分區(qū)的相鄰閉塞分區(qū)內(nèi)，由于SW1503已經(jīng)不能實現(xiàn)側(cè)向防護，此時SW1501應(yīng)設(shè)置為定位。

進路③與進路②雖然明顯進路方向相反，但根據(jù)敵對進路判斷規(guī)則，應(yīng)首先判斷道岔位置敵對。進路②對道岔SW1502的設(shè)定在反位，而進路③對道岔SW1502的設(shè)定在定位，構(gòu)成位置敵對，因此進路②與進路③是一對敵對進路。

應(yīng)用RDSV對南京城軌某線進行自動化數(shù)據(jù)生成和危險數(shù)據(jù)搜索。采用人工方式尋找聯(lián)鎖進路數(shù)據(jù)中的危險數(shù)據(jù)，效率低下且容易出錯，經(jīng)過統(tǒng)計，人工方式全線數(shù)據(jù)檢查耗時96個工時。而采用RDSV可對全線數(shù)據(jù)大批量快速檢查，搜索出所有危險數(shù)據(jù)，僅需要3個工時，其中程序運行時間10 s左右(Inter i3/3.50 GHz/4 G RAM/Windows7)，同時輸出經(jīng)過驗證的數(shù)據(jù)包括進路名稱、進路方向、起止信號機、經(jīng)過道岔及方向、側(cè)防道岔及方向、側(cè)防道岔解鎖條件閉塞分區(qū)和防護進路相關(guān)的所有信息，搜索結(jié)果包括所有人工注入的實驗錯誤數(shù)據(jù)。在修改危險錯誤數(shù)據(jù)后再次使用工具搜索，結(jié)果證明不再存在錯誤和遺漏，保證了正確性和完整性，提高了危險數(shù)據(jù)搜索驗證的效率。

5 結(jié)論

本文在論述信號系統(tǒng)中數(shù)據(jù)安全問題的基礎(chǔ)上，以計算機聯(lián)鎖為研究對象，提出聯(lián)鎖數(shù)據(jù)的建模方法，創(chuàng)新性地提出三類數(shù)據(jù)關(guān)系和對應(yīng)的數(shù)據(jù)安全驗證算法，并進行嚴格的算法證明，在實際工程中得到了良好的驗證，方法正確可行，可提高工程效率，為信號系統(tǒng)數(shù)據(jù)安全驗證提供理論基礎(chǔ)和工具支持。

對數(shù)據(jù)安全性的研究可在此基礎(chǔ)上進一步深入，研究關(guān)鍵點在于：

(1)動態(tài)數(shù)據(jù)安全性的驗證。這類數(shù)據(jù)安全性驗證在車載系統(tǒng)中有集中體現(xiàn)，主要是如何驗證實時信息(包括速度、位置、模式等)在信號系統(tǒng)中形成的數(shù)據(jù)流其安全性。

(2)利用監(jiān)測數(shù)據(jù)提高系統(tǒng)安全性。這類數(shù)據(jù)的安全性是大數(shù)據(jù)思想在信號集中監(jiān)測中的體現(xiàn)，主要是利用實時監(jiān)測數(shù)據(jù)與歷史數(shù)據(jù)相結(jié)合，挖掘并預(yù)警，提前防護，保證列車運行安全。

以上兩個方面分別從數(shù)據(jù)的內(nèi)部特性和外部共性研究數(shù)據(jù)安全，值得深入探討。

參考文獻：

[1]國家質(zhì)量技術(shù)監(jiān)督局.“4·28” 膠濟鐵路特別重大交通事故調(diào)查報告[EB/OL].http://www.docin.com/p-1275 716537.html,2016.

[2]國家安全生產(chǎn)監(jiān)督管理總局.“7·23”甬溫線特別重大鐵路交通事故調(diào)查報告[EB/OL].http://www.chinasafety.gov.cn/newpage/Contents/Channel_21679/2011/1228/244874/content_244874.htm,2016.

[3]Safety Critical System Club.Data Safety by the SCSC Data Safety Initiative Working Group[EB/OL].http://scsc.org.uk/paper_128/Data%20Safety%20%28Version% 201.2%29.pdf?pap=958.

[4]中國鐵路總公司.鐵總運〔2014〕246號文件:列控數(shù)據(jù)管理暫行辦法[Z].2014.

[5]CENELEC.EN 50128 Railway Applications-Communication,Signaling and Processing Systems-Software for Railway Control and Protection Systems:BSI[S].2011.

[6]FAULKNER A,STOREY N.The Role of Data in Safety-related Railway Control Systems[C]//Proceedings International Systems Safety Conference,2001.

[7]MORLEY M J.Safety in Railway Signalling Data:a Behavioural Analysis[C]//Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications.London:Springer-Verlag,1993:464-474.

[8]BOSSCHAART M,QUAGLIETTA E,JANSSEN B,et al.Efficient Formalization of Railway Interlocking Data in RailML[J].Information Systems,2015,49(C):126-141.

[9]WANG D,CHEN X,HUANG H.A Graph Theory-based Approach to Route Location in Railway Interlocking[J].Computers & Industrial Engineering,2013,66(4):791-799.

[10]WANG H,SCHMID F,CHEN L,et al.A Topology-based Model for Railway Train Control Systems[J].IEEE Transactions on Intelligent Transportation Systems,2013,14(2):819-827.

[11]黃友能.城軌CBTC系統(tǒng)數(shù)據(jù)的安全處理與驗證方法研究[D].北京:北京交通大學(xué),2014.