盧鈴冉，張 勇

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

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

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

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

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

1.1 RDC數(shù)據(jù)總結(jié)

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

1.2 RDC數(shù)據(jù)約束條件分析

RDC數(shù)據(jù)庫(kù)中的每個(gè)數(shù)據(jù)都并非單獨(dú)的個(gè)體，都有其空間物理意義，這些數(shù)據(jù)共同構(gòu)成了整個(gè)線路的拓?fù)浣Y(jié)構(gòu)。數(shù)據(jù)約束條件即數(shù)據(jù)應(yīng)滿足的條件，在數(shù)據(jù)驗(yàn)證過(guò)程中應(yīng)該圍繞數(shù)據(jù)的約束條件進(jìn)行驗(yàn)證。通過(guò)對(duì)RDC數(shù)據(jù)進(jìn)行分析，歸納出以下幾個(gè)方面的數(shù)據(jù)約束條件。

1.2.1 屬性域值條件

RDC數(shù)據(jù)庫(kù)中的數(shù)據(jù)表現(xiàn)形式為數(shù)據(jù)表格，每個(gè)數(shù)據(jù)對(duì)象都填寫(xiě)在相應(yīng)的數(shù)據(jù)表中，每個(gè)數(shù)據(jù)對(duì)象都有若干個(gè)實(shí)體屬性，比如取值范圍、精度、數(shù)據(jù)格式等。

1.2.2 拓?fù)浼s束條件

數(shù)據(jù)間的拓?fù)潢P(guān)系指空間上各個(gè)數(shù)據(jù)描述對(duì)象間的相鄰和連接關(guān)系。空間的地理特性通過(guò)數(shù)據(jù)的公里標(biāo)、道岔定反位等信息來(lái)體現(xiàn)。拓?fù)浼s束條件分為以下3個(gè)方面。

（1）映射關(guān)系

映射關(guān)系指軌旁設(shè)備映射在軌道區(qū)段上的位置關(guān)系。軌旁設(shè)備的屬性字段中包含了所屬軌道區(qū)段一項(xiàng)，因此軌旁設(shè)備的位置應(yīng)在其所在區(qū)段的始末端點(diǎn)公里標(biāo)之間。除了軌旁設(shè)備之外，道岔的岔尖里程也應(yīng)在其所在軌道區(qū)段的范圍內(nèi)。

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

RDC數(shù)據(jù)在對(duì)線路和軌旁設(shè)備進(jìn)行描述時(shí)，各個(gè)數(shù)據(jù)并不是單獨(dú)存在的，具有一定的關(guān)聯(lián)性。一個(gè)數(shù)據(jù)項(xiàng)的屬性值可以推導(dǎo)出另外一個(gè)與之相關(guān)聯(lián)的數(shù)據(jù)屬性值。

（3）連續(xù)關(guān)系

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

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

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

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

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

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

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

（2）信號(hào)機(jī)類型和信號(hào)點(diǎn)類型只包含沒(méi)有信號(hào)機(jī)、進(jìn)站信號(hào)機(jī)、通過(guò)信號(hào)機(jī)、進(jìn)路信號(hào)機(jī)、調(diào)車(chē)信號(hào)機(jī)、出站口、出站信號(hào)機(jī)、容許信號(hào)機(jī)、預(yù)告信號(hào)機(jī)9種類型，記為{1，2，3，4，5，6，7，8，9}。

（3）起點(diǎn)公里標(biāo)和終點(diǎn)公里標(biāo)的取值都為非負(fù)整數(shù)。

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

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

Seg_endloc＞Seg_startloc

若線別為上行線，則終點(diǎn)公里標(biāo)滿足：

Seg_startloc＞Seg_endloc

（6）道岔數(shù)量可能為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）岔尖里程數(shù)必須在起點(diǎn)公里標(biāo)和終點(diǎn)公里標(biāo)之間，即：

Seg_startlo＜Seg_swiloc＜Seg_endloc

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

Seg_lenght＜Seg_endloc＜Seg_startlo

若為上行線則區(qū)段長(zhǎng)度為起點(diǎn)和終點(diǎn)公里標(biāo)之差，即：

Seg_lenght=Seg_startlo-Seg_endloc

（10）相鄰軌道區(qū)段公里標(biāo)連續(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 驗(yàn)證方法和思路

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

3.1 CSP語(yǔ)義

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

進(jìn)程（Process）是CSP方法的基本要素之一，其基本結(jié)構(gòu)包括前綴進(jìn)程、確定性選擇、非確定性選擇、遞歸4部分。

3.1.1 前綴進(jìn)程

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

（1）事件前綴選擇進(jìn)程

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

（2）輸出前綴選擇進(jìn)程

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

（3）輸入前綴選擇進(jìn)程

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

3.1.2 確定性選擇進(jìn)程

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

3.1.3 非確定性選擇進(jìn)程

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

3.1.4 遞歸進(jìn)程

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

3.2 CSP語(yǔ)義建模和驗(yàn)證思路

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

圖2 RDC數(shù)據(jù)驗(yàn)證流程建模與驗(yàn)證框圖

3.3 規(guī)則管理

3.3.1 規(guī)則分類

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

3.3.2 規(guī)則抽象

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

3.4 CSP建模

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

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

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

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

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

（3）若線別數(shù)據(jù)為下行線數(shù)據(jù)，則UORD進(jìn)程通過(guò)通道chU2E將線別數(shù)據(jù)發(fā)送給END進(jìn)程，然后END進(jìn)程接收總進(jìn)程SECTION通過(guò)通道chSS2E發(fā)送來(lái)的檢查終點(diǎn)公里標(biāo)請(qǐng)求，若Seg_endloc＞Seg_startloc，即endmorethanstart事件發(fā)生，說(shuō)明終點(diǎn)公里標(biāo)數(shù)據(jù)正確，遞歸到進(jìn)程END，對(duì)終點(diǎn)公里標(biāo)的驗(yàn)證流程結(jié)束；若endpointother事件發(fā)生，則說(shuō)明數(shù)據(jù)錯(cuò)誤，進(jìn)入進(jìn)程ERROR，終止判斷。上行線情況與下行線類似，不再贅述。

用CSP語(yǔ)義對(duì)上述驗(yàn)證流程建模如下：

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

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

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

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

用CSP語(yǔ)義對(duì)上述驗(yàn)證流程建模如下：

3.5 模型驗(yàn)證

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

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

ProB平臺(tái)可自動(dòng)驗(yàn)證模型的死鎖、活鎖和確定性斷言。模型驗(yàn)證主要從以下幾個(gè)方面進(jìn)行。

（1）死鎖

死鎖指系統(tǒng)處于某一狀態(tài)時(shí)，一直處于等待狀態(tài)，無(wú)法跳轉(zhuǎn)到下一狀態(tài)，從而導(dǎo)致系統(tǒng)進(jìn)程無(wú)法繼續(xù)。

（2）活鎖

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

（3）確定性

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

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

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

a.在驗(yàn)證屬性域值性質(zhì)時(shí)，如INDEX進(jìn)程處于indexerror狀態(tài)則說(shuō)明該項(xiàng)數(shù)據(jù)錯(cuò)誤，不能直接跳轉(zhuǎn)到進(jìn)程INDEX，且該狀態(tài)不能與indexcorrect同時(shí)存在。因此需要將該約束條件寫(xiě)成LTL表達(dá)式：

notG([indexerror]&[indexcorrect])

b.在數(shù)據(jù)間有交互作用的驗(yàn)證過(guò)程中，比如驗(yàn)證END進(jìn)程時(shí)，首先要保證startpointcorrect和upordowncorrect，才能進(jìn)行驗(yàn)證，因此需要將該約束條件寫(xiě)成LTL表達(dá)式如下：

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

c.在每一個(gè)進(jìn)程檢查過(guò)程中若出現(xiàn)數(shù)據(jù)錯(cuò)誤，則相應(yīng)的進(jìn)程進(jìn)入ERROR，如檢查INDEX2進(jìn)程中出現(xiàn)index1error則進(jìn)入ERROR進(jìn)程，表示數(shù)據(jù)驗(yàn)證錯(cuò)誤。相應(yīng)的LTL表達(dá)式為：

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

在ProB檢查器中需要通過(guò)LTL語(yǔ)句一一驗(yàn)證模型是否滿足數(shù)據(jù)的約束條件，得到的結(jié)果正確才能說(shuō)明該模型正確，部分驗(yàn)證結(jié)果如圖3所示。

圖3 LTL語(yǔ)句部分約束規(guī)則驗(yàn)證結(jié)果

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

4 結(jié)束語(yǔ)

本文通過(guò)對(duì)RDC數(shù)據(jù)進(jìn)行歸納分析，將實(shí)體數(shù)據(jù)需滿足的約束條件總結(jié)為屬性域值和拓?fù)潢P(guān)系兩方面。以軌道區(qū)段數(shù)據(jù)為例，總結(jié)軌道區(qū)段數(shù)據(jù)應(yīng)滿足的約束規(guī)則，并對(duì)規(guī)則進(jìn)行分類和抽象，再將每個(gè)數(shù)據(jù)字段抽象為獨(dú)立的進(jìn)程，將數(shù)據(jù)約束規(guī)則加入驗(yàn)證流程，以終點(diǎn)公里標(biāo)和索引號(hào)數(shù)據(jù)驗(yàn)證流程為例，利用形式化方法CSP語(yǔ)義對(duì)驗(yàn)證流程進(jìn)行建模，并驗(yàn)證了該模型不存在死鎖、活鎖，滿足確定性的要求，將數(shù)據(jù)約束條件表示成LTL語(yǔ)句加入驗(yàn)證器，得到驗(yàn)證結(jié)果正確，表明該驗(yàn)證流程

滿足數(shù)據(jù)約束規(guī)則，可用于RDC數(shù)據(jù)的驗(yàn)證。本文的研究成果確定了RDC數(shù)據(jù)驗(yàn)證的流程，為下一步RDC數(shù)據(jù)自動(dòng)化驗(yàn)證工具的開(kāi)發(fā)奠定了基礎(chǔ)。