程 鵬，王恪銘, ，王 崢，姚文華，韓 程,

（1．西南交通大學(xué)系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室，成都 610031；2．西南交通大學(xué)計算機與人工智能學(xué)院，成都 614202；3．北京全路通信信號研究設(shè)計院集團有限公司，北京 100070；4．通號粵港澳(廣州)交通科技有限公司，廣州 511400）

1 概述

在軌道交通運輸業(yè)中，軌道交通控制系統(tǒng)[1]的作用類似于神經(jīng)中樞，其正常運行依賴于正確的配置數(shù)據(jù)，使用有效方法保證軌道交通控制系統(tǒng)配置數(shù)據(jù)的正確性十分必要。在目前的實踐應(yīng)用中，對配置數(shù)據(jù)的驗證方式著重于如下兩種手段。

1）靜態(tài)檢測

根據(jù)數(shù)據(jù)的編寫特征進行掃描，對數(shù)據(jù)進行靜態(tài)檢測。

優(yōu)點：運行速度快，可較好地發(fā)現(xiàn)數(shù)據(jù)的完整性問題，如是否空值、長度與結(jié)構(gòu)是否完整等。

缺點：需要人工設(shè)計檢查規(guī)則和檢查辦法，通過代碼的形式，編寫專用工具實現(xiàn)檢查過程，忽略了如果需要修改或擴充規(guī)則，就需要重新修改軟件代碼，而使得工具的可擴展性和可維護性不強，即編寫和修改規(guī)則不靈活。

2）功能測試

對數(shù)據(jù)進行功能性測試，依據(jù)設(shè)計規(guī)范，檢查數(shù)據(jù)流在系統(tǒng)中是否觸發(fā)相應(yīng)的操作。

優(yōu)點：測試過程直觀，可發(fā)現(xiàn)數(shù)據(jù)錯誤導(dǎo)致的問題等。

缺點：嚴重依賴于測試案例的完整程度和覆蓋面，很難遍歷所有數(shù)據(jù)及其組合情況。

綜上所述，在目前的研究應(yīng)用中，更需要找到一種靈活性好、安全可靠性高的方法，即形式化方法[2]。形式化方法是基于嚴格數(shù)學(xué)基礎(chǔ)，對計算機軟件系統(tǒng)進行描述、開發(fā)和驗證的技術(shù)。該方法能夠基于形式規(guī)約語言，建立系統(tǒng)數(shù)據(jù)靜態(tài)規(guī)則原型，使用邏輯驗證方法，窮盡數(shù)據(jù)集，驗證所有數(shù)據(jù)及其組合情況是否滿足所定義的規(guī)則，從而檢查數(shù)據(jù)的完整性和正確性。近10年來，使用形式化方法實現(xiàn)對配置數(shù)據(jù)的正確性驗證，受到了國內(nèi)外研究者的關(guān)注，特別是使用基于一階邏輯和集合論基礎(chǔ)的B方法實現(xiàn)對配置數(shù)據(jù)的正確性驗證。

文獻[3-4]展示了自2009年來，各家世界信號行業(yè)巨頭廠商阿爾斯通(Alstom)、泰雷茲(Thales)、西門子(Siemens)和ProB[5]開發(fā)團隊以及Atelier B建模平臺合作，實現(xiàn)世界各地地鐵線路配置數(shù)據(jù)的形式化驗證的工業(yè)應(yīng)用。

文獻[6-8]描述英國紐卡斯?fàn)柎髮W(xué)的形式化開發(fā)小組開發(fā)SafeCap鐵路站場拓撲形式化設(shè)計驗證平臺，其內(nèi)部機制是利用Eclipse Modeling Framework, 定義各個鐵路站場型信號設(shè)備數(shù)據(jù)的數(shù)據(jù)結(jié)構(gòu)。通過利用Eclipse開發(fā)環(huán)境，生成各個信號設(shè)備數(shù)據(jù)，并在該平臺內(nèi)部定義數(shù)據(jù)靜態(tài)規(guī)則，通過支持將數(shù)據(jù)及其規(guī)則轉(zhuǎn)換為B機器文件格式的腳本，結(jié)合ProB模型檢驗器，實現(xiàn)全自動化判定數(shù)據(jù)是否滿足所定義的規(guī)則。

文獻[9]對CTCS-1級列控系統(tǒng)線路數(shù)據(jù)進行形式化驗證，其過程也類似。首先需要定義數(shù)據(jù)所需滿足的靜態(tài)規(guī)則，然后使用NUSMV模型檢驗器實現(xiàn)數(shù)據(jù)驗證。

上述文獻聚焦于高鐵、地鐵、磁浮拓撲線路配置數(shù)據(jù)的形式化驗證技術(shù)路線的實現(xiàn)上，與本文不同之處在于研究應(yīng)用對象不同，本文的應(yīng)用案例為城市軌道交通列車控制系統(tǒng)[10]配置數(shù)據(jù)的形式化驗證。

軌道交通控制系統(tǒng)作為一類安全苛求系統(tǒng)，任何潛在的系統(tǒng)缺陷都可能會給行車運營安全帶來巨大風(fēng)險。因此，基于各個控制系統(tǒng)配置數(shù)據(jù)的數(shù)據(jù)結(jié)構(gòu)，定義配置數(shù)據(jù)需要滿足的規(guī)則，使用B語言，將已生成的各個配置數(shù)據(jù)和定義好的規(guī)則形式化，以建立配置數(shù)據(jù)的靜態(tài)規(guī)則模型，利用ProB模型檢驗工具驗證靜態(tài)規(guī)則模型，從而驗證所有的配置數(shù)據(jù)及其組合情況是否滿足給定的規(guī)則，以達到驗證配置數(shù)據(jù)正確性的目的。同時，使用形式化語言對規(guī)則進行定義時，能夠靈活的修改、擴充規(guī)則。

2 配置數(shù)據(jù)的數(shù)據(jù)結(jié)構(gòu)

以一個實際的城市軌道交通[11]站場拓撲的數(shù)據(jù)為案例，介紹配置數(shù)據(jù)的數(shù)據(jù)結(jié)構(gòu)。

如圖1所示，這是一個簡化的站場拓撲，只考慮站場拓撲中的道岔對象P（P0-Pn），軌道區(qū)段對象(簡稱區(qū)段，section)和信號機對象S（S0-Sn），以及所生成的進路對象，為方便后續(xù)的驗證工作，整個站場拓撲的編號描述如表1所示。

圖1 站場拓撲Fig.1 Station topology graph

表1 信號設(shè)備對象編號Tab.1 Signaling equipment object number

從圖1中可以看出，這些信號設(shè)備對象之間存在一定的關(guān)系。基于圖1給出的簡化站場拓撲，給出信號設(shè)備對象的數(shù)據(jù)結(jié)構(gòu)。

2.1 道岔設(shè)備數(shù)據(jù)結(jié)構(gòu)

在本案例的道岔數(shù)據(jù)結(jié)構(gòu)中，考慮道岔的3種鏈接關(guān)系：第一種是道岔編號和區(qū)段編號之間的鏈接關(guān)系；第二種是道岔編號和道岔位置之間的關(guān)系；第三種是進路編號和道岔編號之間的關(guān)系。道岔編號和區(qū)段編號之間的鏈接關(guān)系如圖2所示。

圖2 道岔編號Fig.2 Turnout number

圖2中，P1為道岔編號，section0、section1、section2為區(qū)段編號，section0是P1的岔尖區(qū)段編號，section1是P1的定位區(qū)段編號，section2是P1的反位區(qū)段編號。

對于道岔編號和道岔位置間的關(guān)系，同進路編號一起組裝為一個二次關(guān)系，即進路編號-道岔編號-道岔位置。由于每一個進路編號最少有1個道岔編號與之對應(yīng)，故將進路編號和道岔編號之間的關(guān)系組裝為一個二次關(guān)系，即進路編號-道岔序號-道岔編號，道岔序號可以記錄該進路編號有多少個道岔編號。

2.2 區(qū)段設(shè)備數(shù)據(jù)結(jié)構(gòu)

在本案例的區(qū)段數(shù)據(jù)結(jié)構(gòu)中，考慮區(qū)段有6種鏈接關(guān)系，取圖1中的區(qū)段編號section1，section1的6種鏈接關(guān)系，如圖3所示。

圖3 區(qū)段設(shè)備數(shù)據(jù)關(guān)系Fig.3 Section equipment data relationships

2.3 信號機設(shè)備數(shù)據(jù)結(jié)構(gòu)

在本案例的信號機數(shù)據(jù)結(jié)構(gòu)中，考慮信號機編號和區(qū)段編號之間的兩種關(guān)系。每一條進路都有一個始端信號機，而在圖1中可以看出，每一個始端信號機都對應(yīng)一個區(qū)段。

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

基于上文分析，進路數(shù)據(jù)共有3種鏈接關(guān)系，分別是進路編號-道岔序號-道岔編號、進路編號-道岔編號-道岔位置和進路編號-信號機編號。除這3種關(guān)系外，本案例還考慮進路編號-進路方向編號關(guān)系。

3 配置數(shù)據(jù)需要滿足規(guī)則的自然語言描述

根據(jù)道岔設(shè)備、區(qū)段、信號機數(shù)據(jù)結(jié)構(gòu)的定義可知，進路數(shù)據(jù)關(guān)系與這些數(shù)據(jù)結(jié)構(gòu)有關(guān)。本文只對進路數(shù)據(jù)需要滿足的規(guī)則進行自然語言的描述。設(shè)計3種類型的規(guī)則，以驗證進路數(shù)據(jù)的正確性，這3種規(guī)則分別有如下驗證目的：1）判斷進路編號所對應(yīng)的信號機編號，該信號機編號所對應(yīng)的區(qū)段編號是否通過道岔設(shè)備和區(qū)段設(shè)備數(shù)據(jù)關(guān)系推理得到的區(qū)段編號一致；2）判斷進路編號中的道岔編號是否正確，即進路編號中的道岔編號是相鄰的；3）判斷進路編號對應(yīng)的進路方向編號是否和通過道岔設(shè)備和區(qū)段設(shè)備數(shù)據(jù)關(guān)系推理得到的進路方向編號一致。如表2所示，規(guī)則1-6的進路數(shù)據(jù)滿足第一種類型規(guī)則，且將進路編號-進路方向編號的完整性規(guī)則包含在內(nèi)。規(guī)則7-8的進路數(shù)據(jù)滿足第二種類型規(guī)則。規(guī)則9-10的進路數(shù)據(jù)滿足第三種類型規(guī)則。

表2 進路數(shù)據(jù)需要滿足的3種類型規(guī)則Tab.2 Three types of rules to be met by route data

對于第二種類型的規(guī)則，進路的道岔編號相鄰連續(xù)指的是在物理世界里相鄰連續(xù)，換言之，列車完整通過該進路時，物理空間所經(jīng)過的道岔編號和數(shù)據(jù)中的道岔編號是一致的。如圖4所示，就是進路中道岔編號不連續(xù)的情況，該進路編號包含道岔編號P1和道岔編號P2以及4個互不相同的區(qū)段編號，正確的情況是經(jīng)過依次區(qū)段編號section1至section4，但實際卻經(jīng)過如圖4虛線所示的部分，因此該進路的道岔編號不是相鄰連續(xù)的。

圖4 進路和區(qū)段數(shù)據(jù)關(guān)系Fig.4 Data relationship between route and section

如圖5（a）所示，當(dāng)某進路只經(jīng)過1個道岔時，由道岔設(shè)備的數(shù)據(jù)結(jié)構(gòu)決定，可以推斷出該進路的區(qū)段編號一定相鄰且連續(xù)。

當(dāng)任意2個道岔編號所連接的4個區(qū)段編號出現(xiàn)重疊時，如圖5（b）所示，道岔編號P1和道岔編號P2存在相同的區(qū)段編號section2，這種情況也一定相鄰且連續(xù)。

圖5 進路和道岔數(shù)據(jù)關(guān)系Fig.5 Data relationship between route and turnout

4 配置數(shù)據(jù)及其需要滿足規(guī)則的形式化定義

4.1 B方法介紹

基于本節(jié)第2、3節(jié)內(nèi)容和B方法規(guī)則[12]，完成配置數(shù)據(jù)及其規(guī)則的形式化定義。一個完整的B開發(fā)相當(dāng)于生成一個B項目，一個B項目包含很多B模塊。每一個B模塊由一些B組件構(gòu)成，這些B組件包含3種類型：B抽象機器、B精化機器和B實現(xiàn)機器3種。本文在抽象機器中實現(xiàn)對規(guī)則的形式化定義。集合論和一階邏輯賦予B方法精確的定義和嚴格的規(guī)范形式。

4.2 配置數(shù)據(jù)的形式化定義

對于已生成數(shù)據(jù)的形式化考慮兩種形式化表達：1）針對各個信號設(shè)備對象，分別定義不同的抽象數(shù)據(jù)類型，每一種抽象數(shù)據(jù)類型都用一種抽象集合來指代，根據(jù)信號設(shè)備對象的編號，實例化抽象集合，每一個編號都是一個集合元素。2）針對各個信號設(shè)備對象的數(shù)據(jù)關(guān)系，分別定義不同的常量，而后對常量賦值。

1）針對各個信號設(shè)備對象的形式化定義

道岔對象的抽象數(shù)據(jù)類型定義為POINT的抽象集合，實例化后，得到P1至Pn的道岔編號，n為正整數(shù)，如公式（1）所示。

信號機對象的抽象數(shù)據(jù)類型定義為SIGNAL的抽象集合，實例化后，得到S1至Sn的信號機編號，n為正整數(shù)，如公式（2）所示。

進路對象的抽象數(shù)據(jù)類型定義為ROUTE的抽象集合。實例化后，得到R1至Rn的進路編號，n為正整數(shù)，如公式（3）所示。

由于區(qū)段編號需要劃分為4種類型，比如左鏈接為區(qū)段編號、右鏈接為道岔編號等4種類型，故區(qū)段設(shè)備的形式化定義使用常量賦值。

2）針對各個信號設(shè)備數(shù)據(jù)關(guān)系的形式化定義

道岔設(shè)備的數(shù)據(jù)結(jié)構(gòu)考慮3種鏈接關(guān)系，第一種是進路與道岔的關(guān)系，即進路編號-道岔序號-道岔編號，定義常量ROUTE_POINT表示這種關(guān)系，該常量的賦值如公式（4）所示，n為正整數(shù)。

第二種是進路、道岔和道岔位置的關(guān)系，即進路編號-道岔編號-道岔位置，道岔位置反位用0表示，定位用1表示，定義常量ROUTE_POINT_POS表示這種關(guān)系，該常量的賦值如公式（5）所示，其中n為正整數(shù)，p為0或1。

第三種是道岔與區(qū)段的鏈接關(guān)系，為了簡化鏈接關(guān)系復(fù)雜度，分為道岔編號-岔尖編號-定位編號和道岔編號-岔尖編號-反位編號兩種情況，這兩種情況的道岔編號相同。分別定義常量point_left_link和point_right_link表示。這兩個常量的賦值如公式（6）所示，其中n為正整數(shù)，sec1，sec2，sec3，sect4，sec5，sec6為任取的區(qū)段編號，sec1和sec3是岔尖編號，sec2和sec4是定位編號，sec5和sec6是反位編號。

區(qū)段設(shè)備的數(shù)據(jù)結(jié)構(gòu)考慮6種鏈接關(guān)系。將左鏈接為盡頭、右鏈接為區(qū)段編號的關(guān)系，左鏈接為區(qū)段編號、右鏈接為盡頭的關(guān)系，以及左右鏈接均為區(qū)段編號的關(guān)系，合并為左右鏈接均為區(qū)段編號關(guān)系。合并之后，就只有4種鏈接關(guān)系，分別定義常量section_all_section表示左右鏈接均為區(qū)段編號的區(qū)段編號鏈接關(guān)系，section_left_section左鏈接為區(qū)段編號、右鏈接為道岔編號的區(qū)段編號鏈接關(guān)系，section_right_section表示左鏈接為道岔編號、右鏈接為區(qū)段編號的區(qū)段編號鏈接關(guān)系，section_null_section表示左右鏈接均為道岔編號的區(qū)段編號鏈接關(guān)系。對這4個常量賦值如公式（7）所示，seca，secd為任意的區(qū)段編號，secb，secc，sece，secf為任意的區(qū)段編號或盡頭，pointa，pointb，pointc，pointd為任意的道岔編號。

根據(jù)信號機設(shè)備數(shù)據(jù)結(jié)構(gòu)的定義，考慮信號機的兩種鏈接關(guān)系，進路編號-信號機編號和信號機編號-區(qū)段編號，分別用常量ROUTE_SINGAL和SIGNAL-SECTION記錄，對這兩個常量的賦值如公式（8）所示，n為正整數(shù)，Sa，Sb為任意的信號機編號，seca，secb為任意的區(qū)段編號。

除了道岔、區(qū)段、信號機設(shè)備的數(shù)據(jù)關(guān)系外，本案例還考慮了進路編號-進路方向編號關(guān)系，定義常量ROUTE_DIRECTION來記錄，進路方向編號只有0或1，該常量賦值如公式（9）所示，a和b為0或1。

4.3 配置數(shù)據(jù)需要滿足規(guī)則的形式化定義

在完成已生成的數(shù)據(jù)對象形式化后，這個階段需要考慮之前定義的數(shù)據(jù)所要滿足的規(guī)則形式化。這個過程簡單描述為，將每一條自然語言的規(guī)則描述為具有邏輯真假性的謂詞表達式，其判定問題屬于約束可滿足求解問題。約束可滿足問題(Constraint Satisfaction Problem，CSP )[13]的定義是，它由一個三元組組成，其中X是變量的集合，D是變量的取值域，C是約束的結(jié)合，X中的每一個變量都對應(yīng)D中的一個取值域，C中的每一個約束都是由X的子集和一個不相容賦值集合組成。這里的變量集合X可以看成是道岔、信號機、區(qū)段設(shè)備對象、道岔、信號機、區(qū)段設(shè)備數(shù)據(jù)結(jié)構(gòu)包含的關(guān)系。取值域D為這些信號設(shè)備對象所定義的抽象集合的實例化、其數(shù)據(jù)結(jié)構(gòu)所定義的常量的賦值如公式（10）所示。

每一個約束C就是一個自然語言描述的規(guī)則，這個規(guī)則包含部分信號設(shè)備對象的描述，對應(yīng)變量集合X的子集。一般情況下，一個CSP的求解是一個NP-完全問題。若求解的邏輯值為真，則可說明數(shù)據(jù)滿足所定義的規(guī)則。反之則不滿足。

進路數(shù)據(jù)需要滿足的規(guī)則，根據(jù)第3節(jié)分析，進路數(shù)據(jù)需要滿足的規(guī)則除了進路編號-進路方向編號外，分為3種類型，這3種類型定義了8種規(guī)則，從規(guī)則編號3至規(guī)則編號10。

首先，如公式（11）所示給出規(guī)則編號1和規(guī)則編號2的形式化表達式。

1）第一種類型規(guī)則

在規(guī)則編號3的描述中，需要基于道岔設(shè)備、區(qū)段設(shè)備數(shù)據(jù)結(jié)構(gòu)的定義，來獲取某進路編號所對應(yīng)的第一個區(qū)段編號，在本案例站場拓撲結(jié)構(gòu)中，進路編號的第一區(qū)段編號分為如圖6所示的3種情況。

圖6 規(guī)則編號3的三種情況Fig.6 Three cases of rule number 3

如圖6所示，由于這類規(guī)則描述過于復(fù)雜，為簡化形式化表達，特定義道岔位置和道岔數(shù)據(jù)結(jié)構(gòu)之間的關(guān)系，用常量point_link表示，其賦值情況如公式（12）所示。

道岔位置處于反位由0表示，道岔位置在定位由1表示，point_right_link和point_left_link為之前定義的常量。有了以上的鋪墊說明之后，由于規(guī)則編號4和規(guī)則編號3是一種類型，現(xiàn)給出規(guī)則編號3的形式化表達式，如圖7所示。

圖7 規(guī)則編號3的形式化Fig.7 Formalization of rule number 3

在規(guī)則編號3的形式化表達中，量詞xx表示進路編號，量詞bb表示xx的第一個道岔編號的岔尖區(qū)段編號，量詞cc表示xx的第一個道岔編號的定位或反位區(qū)段編號，具體是定位、反位區(qū)段編號，取決于xx。由于考慮進路方向是0，在本案例的站場拓撲中，方向是從右到左，因而bb和cc究竟誰是xx的信號機編號所對應(yīng)的區(qū)段編號，取決于bb和cc誰是左鏈接為道岔編號、右鏈接為區(qū)段編號的區(qū)段編號。若bb是，那么cc一定不會是，因為cc的右鏈接一定是道岔編號，這是由站場拓撲結(jié)構(gòu)所決定的。反之亦然。規(guī)則編號5、6和規(guī)則編號3、4類似。

2）第二種類型規(guī)則

規(guī)則編號7和規(guī)則編號8屬于第二種類型規(guī)則，如圖8所示給出規(guī)則編號7的形式化表達式。

圖8 規(guī)則編號7的形式化Fig.8 Formalization of rule number 7

在規(guī)則編號7的形式化中，量詞xx表示進路編號，由于對xx所包含的道岔進行了排序，量詞yy表示xx所包含的除最后一個序號的道岔編號。bb表示區(qū)段編號，在任意兩個有序的道岔編號中，量詞bb是排序靠前的道岔編號的岔尖區(qū)段編號，量詞cc表示排序靠前的道岔編號的定位或反位的區(qū)段編號，是定位還是反位取決于該條進路編號。量詞dd表示區(qū)段編號，在任意兩個有序的道岔編號中，dd是排序靠后的道岔編號的岔尖區(qū)段編號。量詞ee表示排序靠后的道岔編號的定位或反位的區(qū)段編號，和cc一樣，也取決于進路編號。由于要滿足bb,cc,dd,ee互不相同，而再由站場拓撲道岔數(shù)據(jù)結(jié)構(gòu)所決定，所以如果bb,cc,dd,ee是連續(xù)的，那么集合{bb,cc}中任意一個元素一定與集合{dd,ee}中任意一個元素相鄰，因此集合{bb,cc}中一定有一個元素，即，該區(qū)段編號一定是左鏈接為區(qū)段編號、右鏈接為道岔編號的數(shù)據(jù)結(jié)構(gòu)，且該區(qū)段編號的左鏈接區(qū)段編號一定是dd或ee。

3）第三種類型規(guī)則

在第一種和第二種類型規(guī)則中，其整個形式化表達式的前件，都有使用謂詞表達進路方向。而根據(jù)霍爾邏輯，前件中所有謂詞的布爾值若為假，那么整個表達式為真，因此需要將進路編號所對應(yīng)的進路方向編號描述在后件中，以驗證進路方向編號是否正確，故引入第三種類型規(guī)則，編號10與編號9的表達類似。如圖9所示，給出了規(guī)則編號9形式化表達。

圖9 規(guī)則編號9的形式化Fig.9 Formalization of rule number 9

在規(guī)則編號9的形式化中，量詞xx表示進路編號，yy表示區(qū)段編號，在xx包含的所有道岔編號中，順序為第一個道岔編號，其岔尖區(qū)段編號為yy，量詞zz表示區(qū)段編號，是第一個道岔編號的定位或反位區(qū)段編號，其定、反位取決于xx。根據(jù)站場拓撲結(jié)構(gòu)，進路方向為0的進路編號，其包含的第一個區(qū)段編號一定是左鏈接為道岔編號、右鏈接為區(qū)段編號，根據(jù)此性質(zhì)，驗證了進路編號-進路方向編號數(shù)據(jù)。

5 配置數(shù)據(jù)的形式化驗證

5.1 驗證原理

在本文第4節(jié)中，定義了很多數(shù)據(jù)需要滿足的規(guī)則，對每一個規(guī)則的驗證都可以看作一個約束可滿足求解，每一個規(guī)則的形式化表達式可抽象為如公式（13）所示的表達式

公式（13）中，A1，B1是謂詞，故蘊含符號的前件可由n個謂詞表達式組成，后件也可由n個謂詞表達式組成，n為正整數(shù)。對這樣一個形式化表達式的求解，可轉(zhuǎn)化為如公式（14）所示的表達式。

表達式F的數(shù)學(xué)邏輯意義為析取范式F，故對形式化表達式的邏輯真假值的求解就轉(zhuǎn)化為對析取范式F的邏輯真假值的求解，這就是自動化約束求解工具的內(nèi)部求解原理。本文選取的ProB模型檢驗器(也是約束求解器)，將每一個規(guī)則的形式化表達式中的關(guān)鍵量詞實例化，實例化后的量詞，會給出析取范式的真假值，這樣可進一步準(zhǔn)確分析錯誤源，進而修正錯誤。

5.2 驗證結(jié)果及分析

將本文表1實例化后，信號對象如表3所示。

表3 實例化后的表1Tab.3 Instantiated table 1

表3給出本實際案例中的各個信號設(shè)備對象的個數(shù)，本案例共描述49個形式化表達式，在ProB 1.9.3版本運行結(jié)束后，驗證報錯。經(jīng)過檢查，錯誤進路編號-信號機編號27-64中，信號機編號為24，27，30號所對應(yīng)的區(qū)段編號有錯誤，與現(xiàn)場數(shù)據(jù)設(shè)計人員反饋后，實際情況是在驗證規(guī)則中沒有考慮到區(qū)段偏移。

修正后，再次運行驗證，又發(fā)現(xiàn)錯誤，如圖10所示。經(jīng)過檢查，發(fā)現(xiàn)在Excel表中編寫的進路編號-進路方向編號中的進路方向編號有誤，與現(xiàn)場數(shù)據(jù)設(shè)計人員反饋后，實際上1-27號進路還沒有開通，進路編號為14-16所對應(yīng)的進路方向編號有誤。

圖10 進路方向編號有誤Fig.10 The route direction number is incorrect

修正后再次運行驗證，結(jié)束后，如圖11所示，沒有再發(fā)現(xiàn)錯誤。驗證所有的形式化表達式的邏輯值都為真，至此，數(shù)據(jù)的靜態(tài)正確性檢測已完成。

圖11 正確的驗證結(jié)果Fig.11 Correct verification results

5.3 驗證小結(jié)

基于本文的設(shè)計、定義、驗證、分析過程，總結(jié)數(shù)據(jù)的形式化驗證方案有如下優(yōu)點。

1）驗證嚴謹：使用無歧義的數(shù)學(xué)邏輯符號描述數(shù)據(jù)靜態(tài)規(guī)則；

2）規(guī)則可維護性和可擴展性好：編寫修改靈活，如果更換開發(fā)人員，只要理解形式化數(shù)學(xué)符號，就能看懂規(guī)則；

3）驗證分析過程的直觀性好：利用ProB模型檢驗器，能夠直觀的定位到錯誤的位置；

4）驗證成本低：體現(xiàn)在驗證速度非?？?。

6 結(jié)論

本文以軌道交通控制系統(tǒng)配置數(shù)據(jù)為例，基于B方法建立配置數(shù)據(jù)靜態(tài)規(guī)則原型，并進行形式化驗證。本方法有助于發(fā)現(xiàn)并糾正軌道交通控制系統(tǒng)配置數(shù)據(jù)存在的錯誤，減少因配置數(shù)據(jù)錯誤而引發(fā)系統(tǒng)缺陷，驗證后的配置數(shù)據(jù)可以作為系統(tǒng)正常運行的基礎(chǔ)，減少了數(shù)據(jù)測試階段的成本投入。未來的研究方向可以考慮針對數(shù)據(jù)關(guān)系更為復(fù)雜的配置數(shù)據(jù)，研究基于一階邏輯和集合論的B語言如何實現(xiàn)對其的描述，以及考慮更多場景的應(yīng)用。