基于CSP的CTCS-1級列控系統(tǒng)RDC數據驗證的研究

盧鈴冉，張 勇

（北京交通大學 電子信息工程學院，北京 100044）

近年來，隨著我國鐵路運行控制系統(tǒng)（CTCS）的高速發(fā)展，速度在200 km/h以上高速列車的CTCS-2與CTCS-3級列控系統(tǒng)已日臻完善，對于提高列車運行自動化水平，保證行車安全發(fā)揮了重要作用。據統(tǒng)計，我國鐵路運營里程中普速線路（既有線）占總里程數的70%，而既有線對應的CTCS-0級列控系統(tǒng)存在諸多安全問題。為此，鐵路總公司組織開展了“CTCS-1級列控系統(tǒng)關鍵技術的研究”工作[1]。

CTCS-1級列控系統(tǒng)由車載設備和地面設備構成。其中，車載設備包括車載安全計算機、軌道電路信息接收單元、無線通信單元、應答器信息接收單元等；地面設備包括區(qū)域列控數據中心（RDC，Regional Data Center ）、軌道電路、無線通信接口設備以及應答器等[1]。RDC作為CTCS-1級列控系統(tǒng)的地面核心設備，實時為列車提供行車數據、進路信息、臨時限速信息。RDC數據的正確性對列車運行具有極其重要的意義。目前，RDC基礎數據主要根據工程數據表、CAD設計圖進行純手工編制，編制完成后需要人工校核比對，數據的正確性難以保證。因此，亟需一種對RDC數據進行自動化驗證的方法。

目前，針對列控系統(tǒng)數據驗證的研究較少，并沒有系統(tǒng)化的研究成果。文獻[2-3]分析了列控系統(tǒng)對數據的安全苛求，從數據管理的角度提出提升數據準確性的方法。Michael Huber等人[4]聯(lián)合開發(fā)了工具gdlSMV直接讀取聯(lián)鎖地理數據并通過符號模型檢查內置算法對數據進行自動化驗證，但該方法建立在程序級別，很難驗證數據的耦合性問題。文獻[5]對基于通信的列車運行控制系統(tǒng)（CBTC）靜態(tài)數據先用SAT方法進行處理，然后提出采用基于通信順序進程（CSP，Communicating Sequential Processes）的方法對數據進行驗證，并以地面電子單元（LEU）碼位表中的數據是否與聯(lián)鎖邏輯匹配為例，結合具體場景來說明該方法的可行性，但該研究過程并未對數據實體應滿足的規(guī)則進行歸納和模型驗證。因此，本文在對RDC靜態(tài)數據（簡稱：RDC數據）內容和約束條件進行歸納的基礎上，以車站軌道區(qū)段數據為例，歸納出實體數據應滿足的規(guī)則，將數據驗證規(guī)則加入數據驗證流程，利用CSP形式化方法對RDC數據的驗證流程進行建模，并利用驗證工具—RroB對該模型的死鎖、活鎖、確定性、功能性特性進行自動化驗證，驗證結果表明該模型可應用于RDC數據驗證，為自動化數據驗證工具的開發(fā)奠定了基礎。

1 RDC靜態(tài)數據分析

1.1 RDC數據總結

RDC包含獨立的線路數據庫，用于存儲當前RDC所管轄范圍內全部線路的靜態(tài)數據。RDC根據當前列車的位置信息、軌道電路占用情況從數據庫中讀取線路數據并按照一定的規(guī)則組織數據，同時結合車站聯(lián)鎖發(fā)來的進路信息與臨時限速服務器發(fā)來的臨時限速信息，通過無線通信方式發(fā)送給車載設備。RDC數據庫中線路數據包括：軌道區(qū)段數據、道岔數據、應答器數據、線路限速數據、坡度數據以及進路數據。

1.2 RDC數據約束條件分析

RDC數據庫中的每個數據都并非單獨的個體，都有其空間物理意義，這些數據共同構成了整個線路的拓撲結構。數據約束條件即數據應滿足的條件，在數據驗證過程中應該圍繞數據的約束條件進行驗證。通過對RDC數據進行分析，歸納出以下幾個方面的數據約束條件。

1.2.1 屬性域值條件

RDC數據庫中的數據表現(xiàn)形式為數據表格，每個數據對象都填寫在相應的數據表中，每個數據對象都有若干個實體屬性，比如取值范圍、精度、數據格式等。

1.2.2 拓撲約束條件

數據間的拓撲關系指空間上各個數據描述對象間的相鄰和連接關系?？臻g的地理特性通過數據的公里標、道岔定反位等信息來體現(xiàn)。拓撲約束條件分為以下3個方面。

（1）映射關系

映射關系指軌旁設備映射在軌道區(qū)段上的位置關系。軌旁設備的屬性字段中包含了所屬軌道區(qū)段一項，因此軌旁設備的位置應在其所在區(qū)段的始末端點公里標之間。除了軌旁設備之外，道岔的岔尖里程也應在其所在軌道區(qū)段的范圍內。

（2）關聯(lián)關系

RDC數據在對線路和軌旁設備進行描述時，各個數據并不是單獨存在的，具有一定的關聯(lián)性。一個數據項的屬性值可以推導出另外一個與之相關聯(lián)的數據屬性值。

（3）連續(xù)關系

連續(xù)關系表現(xiàn)在兩個方面：（1）各個數據索引號的連續(xù)關系；（2）相鄰區(qū)段的里程數連續(xù)，符合此連續(xù)關系的數據有：軌道區(qū)段、線路限速、坡度信息。

綜上所述，RDC數據庫所包含的靜態(tài)數據以及數據之間的關系可用如圖1所示類圖表示。

2 數據約束規(guī)則提取

RDC實體數據應滿足的約束規(guī)則是基于《列車運行監(jiān)控裝置（LKJ）數據文件編制規(guī)范（V1.0）》[6]和RDC靜態(tài)數據庫的數據結構以及數據編制經驗得到，通過對各個數據字段的分析整理可得到完備的數據驗證規(guī)則。

以車站軌道區(qū)段數據為例，軌道區(qū)段Section數據是一個十一元組，可以描述為＜Seg_index, Seg_sigpointtype, Seg_startloc, Seg_sigtype, Seg_endloc,Seg_frequency, Seg_length, Seg_upordown, Seg_swinum, Seg_swiloc＞，分別代表區(qū)段索引號、信號點類型、起點公里標、信號機類型、終點公里標、軌道區(qū)段載頻、軌道區(qū)段長度、線別、道岔數量、岔尖里程。車站軌道區(qū)段數據應滿足的具體規(guī)則如下。

圖1 RDC靜態(tài)數據類圖

（1）區(qū)段索引號即為區(qū)段編號，應滿足唯一性和連續(xù)性，即：

（2）信號機類型和信號點類型只包含沒有信號機、進站信號機、通過信號機、進路信號機、調車信號機、出站口、出站信號機、容許信號機、預告信號機9種類型，記為{1，2，3，4，5，6，7，8，9}。

（3）起點公里標和終點公里標的取值都為非負整數。

（4）線別只包含上行線和下行線2種類型，記為{0,1}。

（5）在規(guī)則（3）和（4）滿足的前提下，若線別為下行線情況，則終點公里標滿足：

Seg_endloc＞Seg_startloc

若線別為上行線，則終點公里標滿足：

Seg_startloc＞Seg_endloc

（6）道岔數量可能為0、1、2的3種類型，記為{0,1,2}。

（7）軌道區(qū)段載頻包含0、1 700 Hz、2 000 Hz、2 300 Hz、2 600 Hz5種類型，分別記為{1,2,3,4,5}。

（8）岔尖里程數必須在起點公里標和終點公里標之間，即：

Seg_startlo＜Seg_swiloc＜Seg_endloc

（9）在規(guī)則（3）和（4）滿足的前提下，若為下行線則區(qū)段長度為終點和起點公里標之差，即：

Seg_lenght＜Seg_endloc＜Seg_startlo

若為上行線則區(qū)段長度為起點和終點公里標之差，即：

Seg_lenght=Seg_startlo-Seg_endloc

（10）相鄰軌道區(qū)段公里標連續(xù)，即：

Seg_startloi+1=Seg_endloci

（11）在規(guī)則（4）和（7）滿足的前提下，下行線載頻只包含0、1 700 Hz和2 300 Hz3種情況，上行線載頻只包含0、2 000 Hz和2 600 Hz3種情況。

3 驗證方法和思路

確立數據約束規(guī)則后，需將數據約束規(guī)則加入數據驗證流程，并利用形式化方法CSP語義對數據驗證流程建模并驗證，以得到正確的數據驗證流程。

3.1 CSP語義

CSP是一種針對并發(fā)系統(tǒng)的代數理論，該方法可以精確地描述由多進程構成的系統(tǒng)，進程內部通過消息交互來推動事件的發(fā)生和狀態(tài)的轉移。CSP語義模型具有可遍歷所有事件和狀態(tài)的特點，可以完整地驗證所有情況，因此本文采取該方法對數據驗證流程進行建模。

進程（Process）是CSP方法的基本要素之一，其基本結構包括前綴進程、確定性選擇、非確定性選擇、遞歸4部分。

3.1.1 前綴進程

x→P或P=STOP，表示一個有限行為進程，進程名通常用大寫字母表示，STOP代表終止進程，執(zhí)行到該進程后不再進行任何操作。常用的前綴進程包括以下幾種：

（1）事件前綴選擇進程

（?x:→P），若A為一事件集合，即A?∑，則進程？x:→P(x)代表當執(zhí)行任意動作x∈A時，下一動作執(zhí)行進程P，執(zhí)行后的狀態(tài)為P(x)，即x為是否執(zhí)行進程P的判斷條件。

（2）輸出前綴選擇進程

（C!x:→P），其中C為進程間通信的通道，C!x:→P(x)表示在通道C上輸出x后，執(zhí)行進程P(x)。

（3）輸入前綴選擇進程

（C?x:→P），C為進程間通信的通道，A?∑，則進程C?x:→P(x)表示通過通道C接收輸入x∈A后執(zhí)行進程P(x)。

3.1.2 確定性選擇進程

P□Q表示由外界環(huán)境決定執(zhí)行進程P或者Q。

3.1.3 非確定性選擇進程

P∏Q表示該進程是任意的，不受外界環(huán)境影響，可選擇P或者Q。

3.1.4 遞歸進程

遞歸是用短得多的記法來刻畫重復的行為。若X和P代表進程， ?P表示P的字母表， P(X)代表進程X的衛(wèi)式， 即P(X)服從?→X， 若X為不可終止進程， 則X=P(X)代表遞歸進程， 可以表示無窮進程。

3.2 CSP語義建模和驗證思路

采用CSP語義對RDC數據驗證流程進行建模，首先需要將數據約束條件加入數據驗證流程，本文將每個數據字段抽象為單獨的進程，數據間的相互聯(lián)系通過相應的通道進行信息交互來實現(xiàn)。由于CSP語義是一種抽象化描述方式，因此需要對規(guī)則進行管理和抽象化描述，建模和驗證流程分為規(guī)則管理、建立模型、模型驗證3個階段，具體流程如圖2所示。

圖2 RDC數據驗證流程建模與驗證框圖

3.3 規(guī)則管理

3.3.1 規(guī)則分類

根據本文1.2節(jié)中對約束條件的歸納總結，將規(guī)則（1）～（11）進行分類：屬性域值、映射關系和關聯(lián)關系規(guī)則針對的是單個數據字段應滿足的屬性規(guī)則和數據字段間的相互約束關系，在數據表中體現(xiàn)為橫向數據驗證；而連續(xù)關系體現(xiàn)的是同一數據字段相鄰數據間的關系以及不同字段間的連續(xù)關系，在數據表中體現(xiàn)為縱向數據驗證。因此將每個字段抽象為單獨的進程，將規(guī)則分為橫向驗證和縱向驗證，分別對不同的字段的驗證流程進行建模，可以使得驗證過程條理更加清晰。

3.3.2 規(guī)則抽象

為避免狀態(tài)爆炸，CSP語義不可能分析驗證對象具體的屬性值，只能在不影響所驗證規(guī)則的基礎上將數據取值進行抽象，比如線別Seg_upordown字段的值只能為上行線0和下行線1，其他取值都不合法，因此將該字段取值抽象為upordown0、upordown1和upordownother3種類型，分別代表取值為下行線、上行線和錯誤類型。

3.4 CSP建模

將抽象后的數據約束規(guī)則加入數據驗證流程，對每個字段的數據驗證流程用CSP形式化方法進行描述，其具體建模過程如下。

3.4.1 屬性域值、映射關系和關聯(lián)關系CSP模型

以體現(xiàn)上述約束關系的典型字段——終點公里標為例對驗證過程進行建模。終點公里標需滿足的屬性域值條件對應規(guī)則（3）,需滿足的映射關系和關聯(lián)關系條件對應規(guī)則（4）。將規(guī)則（3）和（4）加入數據驗證流程，即：

（1）終點公里標進程END向起點公里標進程START通過通道chE2S發(fā)送檢查請求，START進程接收到請求后檢查起點公里標是否滿足規(guī)則，若起點公里標數據正確則START將起點公里標的值通過通道chE2S發(fā)送給END，反之進入錯誤進程ERROR，終止判斷。

（2）END進程獲得起點公里標的值后，通過通道chE2U向線別進程UORD發(fā)送檢查線別數據請求，UORD收到請求后檢查線別數據，若數據為upordown0或upordown1，分別代表下行線或上行線，說明數據正確進入下一進程E2或E3，若數據為upordownother，代表其他類型數據，說明線別數據錯誤，進入錯誤進程ERROR，終止判斷。

（3）若線別數據為下行線數據，則UORD進程通過通道chU2E將線別數據發(fā)送給END進程，然后END進程接收總進程SECTION通過通道chSS2E發(fā)送來的檢查終點公里標請求，若Seg_endloc＞Seg_startloc，即endmorethanstart事件發(fā)生，說明終點公里標數據正確，遞歸到進程END，對終點公里標的驗證流程結束；若endpointother事件發(fā)生，則說明數據錯誤，進入進程ERROR，終止判斷。上行線情況與下行線類似，不再贅述。

用CSP語義對上述驗證流程建模如下：

3.4.2 連續(xù)關系CSP模型

以體現(xiàn)連續(xù)關系的典型字段—區(qū)段索引號為例對驗證過程建模。索引號Seg_index連續(xù)關系需滿足規(guī)則（10），定義進程INDEX1代表Seg_indexi，進程INDEX2代表Seg_indexi+1，將規(guī)則（10）加入驗證流程，即：

（1）檢查Seg_indexi+1數據是否滿足連續(xù)性，首先需要保證Seg_indexi取值正確，即INDEX2進程通過通道chSS2I2向INDEX1發(fā)送檢查請求，若Seg_indexi取值正確則進入進程I1，反之進入錯誤進程ERROR。

（2）INDEX2通過通道chI12I2得到Seg_indexi的值后，接收總進程SECTION通過通道chSS2I2發(fā)送的檢查命令，檢查Seg_indexi+1是否滿足等式Seg_indexi+1=Seg_indexi+1，若滿足即事件i2equi1p1發(fā)生，即說明索引號數據正確，遞歸到進程INDEX2，反之說明數據錯誤，進入ERROR進程。

用CSP語義對上述驗證流程建模如下：

3.5 模型驗證

將CSP語義模型代碼導入模型驗證工具，并將數據約束規(guī)則用線性時序邏輯（LTL，Linear Temporal Logic）語句來刻畫，將兩部分共同作為ProB模型驗證器的輸入，對模型的正確性和有效性進行驗證并對結果進行分析。若出現(xiàn)錯誤則可根據反例對錯誤進行定位和追蹤，從而發(fā)現(xiàn)模型中的錯誤并進行修改和重驗。

其他數據字段的建模過程與3.4節(jié)中示例類似，將所有數據字段的驗證流程建模完成后，將各進程的CSP語義模型先轉換為CSPM語言，即機器可讀語言，將其加載到ProB平臺[8]對各模型進行檢驗，部分程序如下所示。

ProB平臺可自動驗證模型的死鎖、活鎖和確定性斷言。模型驗證主要從以下幾個方面進行。

（1）死鎖

死鎖指系統(tǒng)處于某一狀態(tài)時，一直處于等待狀態(tài)，無法跳轉到下一狀態(tài)，從而導致系統(tǒng)進程無法繼續(xù)。

（2）活鎖

活鎖指進程中存在死循環(huán)，該現(xiàn)象會導致系統(tǒng)中其他功能無法得到驗證并使系統(tǒng)部分功能缺失。

（3）確定性

確定性指對于所建模型各狀態(tài)的轉移是確定的而且可以進行直接觀測或者間接描述。

（4）功能性驗證

功能性驗證即驗證模型是否滿足約束規(guī)則。將數據應滿足的約束規(guī)則通過LTL表達式表示出來，與模型共同作為驗證器的輸入，若驗證通過則說明所建立的模型滿足約束條件，若驗證不通過則可以給出反例，可定位模型的錯誤之處并進行修改。由于模型待驗證的約束規(guī)則過多，因此本文給出以下示例進行介紹。

a.在驗證屬性域值性質時，如INDEX進程處于indexerror狀態(tài)則說明該項數據錯誤，不能直接跳轉到進程INDEX，且該狀態(tài)不能與indexcorrect同時存在。因此需要將該約束條件寫成LTL表達式：

notG([indexerror]&[indexcorrect])

b.在數據間有交互作用的驗證過程中，比如驗證END進程時，首先要保證startpointcorrect和upordowncorrect，才能進行驗證，因此需要將該約束條件寫成LTL表達式如下：

G([startpointcorrect]&[upordowncorrect])=＞F([checkendpoint])

c.在每一個進程檢查過程中若出現(xiàn)數據錯誤，則相應的進程進入ERROR，如檢查INDEX2進程中出現(xiàn)index1error則進入ERROR進程，表示數據驗證錯誤。相應的LTL表達式為：

G([index1error])=＞F([dataerror])

在ProB檢查器中需要通過LTL語句一一驗證模型是否滿足數據的約束條件，得到的結果正確才能說明該模型正確，部分驗證結果如圖3所示。

圖3 LTL語句部分約束規(guī)則驗證結果

圖3驗證結果表明，該模型滿足數據的約束規(guī)則和無死鎖、活鎖等要求，本文提出的數據驗證流程可用于RDC數據驗證。

4 結束語

本文通過對RDC數據進行歸納分析，將實體數據需滿足的約束條件總結為屬性域值和拓撲關系兩方面。以軌道區(qū)段數據為例，總結軌道區(qū)段數據應滿足的約束規(guī)則，并對規(guī)則進行分類和抽象，再將每個數據字段抽象為獨立的進程，將數據約束規(guī)則加入驗證流程，以終點公里標和索引號數據驗證流程為例，利用形式化方法CSP語義對驗證流程進行建模，并驗證了該模型不存在死鎖、活鎖，滿足確定性的要求，將數據約束條件表示成LTL語句加入驗證器，得到驗證結果正確，表明該驗證流程

滿足數據約束規(guī)則，可用于RDC數據的驗證。本文的研究成果確定了RDC數據驗證的流程，為下一步RDC數據自動化驗證工具的開發(fā)奠定了基礎。