基于CSP的CTCS-1級列控系統RDC數據驗證的研究

盧鈴冉，張 勇

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

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

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

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

1 RDC靜態數據分析

1.1 RDC數據總結

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

1.2 RDC數據約束條件分析

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

1.2.1 屬性域值條件

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

1.2.2 拓撲約束條件

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

（1）映射關系

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

（2）關聯關系

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

（3）連續關系

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

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

2 數據約束規則提取

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

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

圖1 RDC靜態數據類圖

（1）區段索引號即為區段編號，應滿足唯一性和連續性，即：

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

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

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

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

Seg_endloc＞Seg_startloc

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

Seg_startloc＞Seg_endloc

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

（7）軌道區段載頻包含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）在規則（3）和（4）滿足的前提下，若為下行線則區段長度為終點和起點公里標之差，即：

Seg_lenght＜Seg_endloc＜Seg_startlo

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

Seg_lenght=Seg_startlo-Seg_endloc

（10）相鄰軌道區段公里標連續，即：

Seg_startloi+1=Seg_endloci

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

3 驗證方法和思路

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

3.1 CSP語義

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

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

3.1.1 前綴進程

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

（1）事件前綴選擇進程

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

（2）輸出前綴選擇進程

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

（3）輸入前綴選擇進程

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

3.1.2 確定性選擇進程

P□Q表示由外界環境決定執行進程P或者Q。

3.1.3 非確定性選擇進程

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

3.1.4 遞歸進程

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

3.2 CSP語義建模和驗證思路

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

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

3.3 規則管理

3.3.1 規則分類

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

3.3.2 規則抽象

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

3.4 CSP建模

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

3.4.1 屬性域值、映射關系和關聯關系CSP模型

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

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

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

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

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

3.4.2 連續關系CSP模型

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

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

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

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

3.5 模型驗證

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

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

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

（1）死鎖

死鎖指系統處于某一狀態時，一直處于等待狀態，無法跳轉到下一狀態，從而導致系統進程無法繼續。

（2）活鎖

活鎖指進程中存在死循環，該現象會導致系統中其他功能無法得到驗證并使系統部分功能缺失。

（3）確定性

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

（4）功能性驗證

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

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

notG([indexerror]&[indexcorrect])

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

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

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

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

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

圖3 LTL語句部分約束規則驗證結果

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

4 結束語

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

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