基于通信順序進(jìn)程與B方法的CBTC計(jì)算機(jī)聯(lián)鎖系統(tǒng)的形式化建模與驗(yàn)證

王 鯤

(1.中國鐵道科學(xué)研究院 通信信號研究所，北京 100081；2.國家鐵路智能運(yùn)輸系統(tǒng)工程技術(shù)研究中心，北京 100081)

在基于通信的列車控制(Communication Based Train Control，CBTC)系統(tǒng)中，計(jì)算機(jī)聯(lián)鎖系統(tǒng)(簡稱CBTC聯(lián)鎖系統(tǒng))是重要的基礎(chǔ)設(shè)備之一。隨著CBTC技術(shù)日趨精密復(fù)雜，CBTC聯(lián)鎖系統(tǒng)不僅需要通過復(fù)雜的邏輯狀態(tài)運(yùn)算以實(shí)現(xiàn)對聯(lián)鎖進(jìn)路、信號機(jī)、道岔、軌道區(qū)段、站臺門、防淹門等的控制，還需要與外部系統(tǒng)進(jìn)行實(shí)時(shí)通信，實(shí)現(xiàn)數(shù)據(jù)交互，而且在進(jìn)行邏輯計(jì)算時(shí)涉及巨大的內(nèi)部狀態(tài)空間，在與外部系統(tǒng)實(shí)時(shí)通信時(shí)引入了大量的并發(fā)性和不確定性，因此該系統(tǒng)是一種典型的復(fù)雜安全苛求系統(tǒng)。同時(shí)，CBTC聯(lián)鎖系統(tǒng)的關(guān)鍵性質(zhì)與其功能性混合在一起，并與軟件開發(fā)的全過程密切相關(guān)，使得這些關(guān)鍵性質(zhì)的獲得和保證變得更加復(fù)雜。因此，如何在CBTC聯(lián)鎖系統(tǒng)軟件的開發(fā)和維護(hù)中保證軟件具有所需的安全性、無死鎖性等關(guān)鍵性質(zhì)，成為了重要的研究方向。

統(tǒng)計(jì)表明，傳統(tǒng)的非形式化的軟件工程技術(shù)對軟件質(zhì)量的保證具有一個(gè)難以逾越的頂點(diǎn)，而形式化方法的實(shí)踐證明形式化方法是提高軟件質(zhì)量的重要途徑[1]。形式化的方法通過嚴(yán)格的數(shù)學(xué)方法，定性定量地描述軟件的行為，建立關(guān)鍵性質(zhì)與軟件行為之間的內(nèi)在聯(lián)系和嚴(yán)格描述，從而設(shè)計(jì)并驗(yàn)證軟件所需的關(guān)鍵性質(zhì)。標(biāo)準(zhǔn)IEC62279：2002《鐵路應(yīng)用：通信、信號、處理系統(tǒng)——鐵路控制和防護(hù)系統(tǒng)軟件》[2]中指出：“在軟件安全完善度等級為4級時(shí)，軟件需求規(guī)格說明書定義、軟件設(shè)計(jì)和實(shí)施、驗(yàn)證和測試等過程中，強(qiáng)力推薦使用形式化方法進(jìn)行描述和設(shè)計(jì)；在對軟件驗(yàn)證和測試時(shí)，強(qiáng)力推薦使用形式化證明技術(shù)”。

國內(nèi)外的學(xué)者們對鐵路聯(lián)鎖系統(tǒng)的形式建模及驗(yàn)證進(jìn)行了研究。Kirsten WINTER[3-4]在聯(lián)鎖軟件分析設(shè)計(jì)的早期，分別采用了通信順序進(jìn)程和符號模型檢驗(yàn)工具進(jìn)行模型檢驗(yàn)，并將其運(yùn)用在昆士蘭鐵路項(xiàng)目中。KIRSTEN Mark Hansen[5]采用基于維也納開發(fā)方法(VDM)，對丹麥鐵路系統(tǒng)中聯(lián)鎖系統(tǒng)進(jìn)行了建模與驗(yàn)證。Vicky Hartonas-Garmhausen[6]等利用符號模型檢驗(yàn)工具(SMV)對鐵路聯(lián)鎖系統(tǒng)的動(dòng)態(tài)行為進(jìn)行建模，研究狀態(tài)空間約簡的方法，發(fā)現(xiàn)了系統(tǒng)中潛在的不安全行為路徑，并提出了系統(tǒng)改進(jìn)的建議。

在城市軌道交通領(lǐng)域，也有一些學(xué)者基于形式化方法進(jìn)行了研究。Thierry Lecomte[7]等提出了基于B方法的城市軌道交通站臺門控制系統(tǒng)的建模和驗(yàn)證，目的在于保證故障模式下系統(tǒng)可以正確地實(shí)現(xiàn)其功能。Robert Abo[8]等采用B方法對CBTC系統(tǒng)的數(shù)據(jù)進(jìn)行確認(rèn)，并糾正了規(guī)約中的一些錯(cuò)誤。陳銘松[9]等提出了以形式化方法為主要技術(shù)切入點(diǎn)的CBTC可信構(gòu)造框架，提供相應(yīng)的形式化方法與工具,支持全生命周期內(nèi)系統(tǒng)功能與非功能屬性的建模與驗(yàn)證。Nazir Ahmad Zafar[10]采用圖論和Z語言方法對移動(dòng)閉塞聯(lián)鎖系統(tǒng)進(jìn)行建模，對其安全屬性進(jìn)行檢驗(yàn)。但是，以上這些研究成果，均采用的是某一種形式化方法，而CBTC聯(lián)鎖系統(tǒng)不僅具有巨大的狀態(tài)空間，還具有并發(fā)的信息交互行為，僅采用單一的形式化方法進(jìn)行建模，難以適用其復(fù)雜系統(tǒng)的多種特性。

為了能夠更加全面、準(zhǔn)確地描述CBTC聯(lián)鎖系統(tǒng)的復(fù)雜性，本文提出將適合于描述系統(tǒng)并發(fā)特性的通信順序進(jìn)程(Communication Sequential Processes，CSP)與適合于描述系統(tǒng)狀態(tài)的B方法兩者集成的形式化方法，對CBTC聯(lián)鎖系統(tǒng)進(jìn)行建模和驗(yàn)證，以保證CBTC聯(lián)鎖系統(tǒng)軟件的安全性和無死鎖性。

1 形式化方法

形式化方法是指具有嚴(yán)格數(shù)學(xué)基礎(chǔ)的軟件和系統(tǒng)開發(fā)方法，支持計(jì)算機(jī)系統(tǒng)及軟件的規(guī)約、設(shè)計(jì)、驗(yàn)證與演化等活動(dòng)[11]。形式化方法的目標(biāo)是建立精確的、無二義性的語義，對系統(tǒng)開發(fā)各個(gè)階段的模型進(jìn)行有效的描述，使系統(tǒng)結(jié)構(gòu)具有先天的合理性和正確性，良好的維護(hù)性，從而較好地滿足用戶需求。眾多的形式化方法中，通信順序進(jìn)程和B方法是2種基于不同理論基礎(chǔ)的形式化方法。

1.1 通信順序進(jìn)程

通信順序進(jìn)程[12]是一種基于進(jìn)程代數(shù)的形式化方法，適合于分布式系統(tǒng)和并發(fā)系統(tǒng)的開發(fā)。該方法的基本原理：提供了描述和分析系統(tǒng)各個(gè)進(jìn)程之間交互的實(shí)體行為的數(shù)學(xué)框架，進(jìn)程內(nèi)部通過信息的交互而相互作用和影響；可對進(jìn)程的各個(gè)階段進(jìn)行精確定義和驗(yàn)證，具有嚴(yán)格的數(shù)學(xué)邏輯；主要通過進(jìn)程事件的集合、進(jìn)程的跡、進(jìn)程間的通信描述進(jìn)程的行為，通過并發(fā)、選擇、遞歸等描述進(jìn)程之間的關(guān)系。該方法的基本概念歸納如下。

(1) 進(jìn)程是指事件或活動(dòng)的序列，設(shè)P是1個(gè)進(jìn)程，該進(jìn)程的第1個(gè)事件是x，且事件x執(zhí)行之后，進(jìn)程P的剩余部分為Q，則進(jìn)程P可表示為x→Q，其中事件x稱為前綴；x∈αΡ，α(x→Q)=αP，其中α為1個(gè)運(yùn)算子，將每一個(gè)進(jìn)程映射為它的事件集。

(2) 進(jìn)程的跡是1個(gè)進(jìn)程所執(zhí)行事件歷史行為的符號記錄。對于進(jìn)程P， 用trace(P)表示進(jìn)程P所有可能跡的集合。

(4) 進(jìn)程之間存在相同事件的交互，這種交互的事件稱為通信事件，記為c.v，其中c為信道名，v為所傳遞的消息值。1個(gè)起始執(zhí)行在信道c上輸出消息v的進(jìn)程可表示為

(c！v→P)=(c.v→P)

1個(gè)起始執(zhí)行從信道c上輸入可通信的消息x， 并接著執(zhí)行P(x)的進(jìn)程，可表示為

(c？x→P(x))=(y：{y|channel(y)=c}→P(message(y)))

1.2 B方法

B方法[13]是一種基于狀態(tài)的形式化方法，通過數(shù)學(xué)的推理或邏輯演算，逐步建立起基于數(shù)學(xué)理論基礎(chǔ)的體系，這個(gè)體系既可以構(gòu)造軟件系統(tǒng)的狀態(tài)和行為特征，如抽象機(jī)、廣義代換語言等，也可以通過類型檢查和證明義務(wù)證明該體系語義語法的正確性，并通過模型精化讓抽象模型變得豐富、具體。

抽象機(jī)是B方法中的基本單元，用于描述軟件系統(tǒng)的1個(gè)子模塊，多個(gè)抽象機(jī)集合組成軟件系統(tǒng)的模型。抽象機(jī)由抽象機(jī)名、變量、不變式、初始化和操作等構(gòu)成，基本形式為：

MACHINE M(…)

VARIABLES …

INVARIANT …

INITIALISATION …

OPERATIONS …

END

其中1個(gè)典型的操作可表述為

output←operate(input)=PRE G THEN S END

該操作中：operate為操作名； output為輸出變量；input為輸入變量；G為前提，用于給出輸入變量的類型或者條件；S為操作的主體。

1.3 通信順序進(jìn)程與B方法的集成

通信順序進(jìn)程以‘事件驅(qū)動(dòng)’模式對并發(fā)系統(tǒng)進(jìn)行建模與驗(yàn)證，但不適合于具有復(fù)雜狀態(tài)空間的軟件系統(tǒng)；B方法側(cè)重于對具有復(fù)雜狀態(tài)空間的軟件系統(tǒng)描述，但不適合描述并發(fā)系統(tǒng)的交互行為；因此將這2種方法進(jìn)行集成，可以用于全面地刻畫具有復(fù)雜狀態(tài)空間及并發(fā)交互行為的軟件系統(tǒng)。

將這2種方法進(jìn)行集成的關(guān)鍵點(diǎn)在于：在通信順序進(jìn)程的通信事件與B方法抽象機(jī)的操作之間建立起一對一的映射關(guān)系，實(shí)現(xiàn)通信事件通過控制抽象機(jī)的操作，進(jìn)而影響抽象機(jī)的狀態(tài)，這樣，進(jìn)程與抽象機(jī)之間的映射實(shí)現(xiàn)了通信順序進(jìn)程和B方法之間的同步。語義上，將抽象機(jī)等同視為1個(gè)通信順序進(jìn)程，從而更加全面、清晰地刻畫軟件系統(tǒng)的行為。圖1示例了通信順序進(jìn)程與B方法集成的邏輯關(guān)系，其中，通信順序進(jìn)程1的2個(gè)通信事件1和2分別控制著B方法抽象機(jī)1的操作1和2的調(diào)用。

圖1 通信順序進(jìn)程與B方法的集成

2 CBTC聯(lián)鎖系統(tǒng)的形式化建模

2.1 CBTC聯(lián)鎖系統(tǒng)

CBTC計(jì)算機(jī)聯(lián)鎖系統(tǒng)是應(yīng)用于城市軌道交通領(lǐng)域的安全苛求系統(tǒng)。它采用計(jì)算機(jī)、通信、控制相結(jié)合的技術(shù)手段，實(shí)現(xiàn)對聯(lián)鎖進(jìn)路、道岔、信號機(jī)、軌道區(qū)段、站臺門、防淹門等設(shè)備的邏輯狀態(tài)運(yùn)算，并通過繼電接口對這些設(shè)備進(jìn)行監(jiān)督和控制，通過安全通信接口與區(qū)域控制中心(ZC)、車載控制器(VOBC)、列車自動(dòng)監(jiān)控系統(tǒng)(ATS)、相鄰聯(lián)鎖系統(tǒng)(NCBI)、線路電子單元(LEU)等外部系統(tǒng)進(jìn)行實(shí)時(shí)通信，實(shí)現(xiàn)數(shù)據(jù)的交互，從而協(xié)同完成列車運(yùn)行的控制，保證列車運(yùn)行安全，有效地提高運(yùn)輸效率和運(yùn)輸自動(dòng)化水平。描述CBTC聯(lián)鎖系統(tǒng)功能行為的用例圖如圖2所示。

圖2 CBTC聯(lián)鎖系統(tǒng)的用例圖

2.2 CBTC聯(lián)鎖系統(tǒng)的形式化模型

CBTC聯(lián)鎖系統(tǒng)的邏輯狀態(tài)運(yùn)算行為具有復(fù)雜的狀態(tài)空間，選用B方法建模，即采用抽象機(jī)及其操作進(jìn)行描述。CBTC聯(lián)鎖系統(tǒng)的邏輯狀態(tài)運(yùn)算可分為聯(lián)鎖進(jìn)路控制、站場信號平面圖和聯(lián)鎖表3部分，對應(yīng)地采用B方法分別構(gòu)建聯(lián)鎖進(jìn)路控制抽象機(jī)、信號平面圖抽象機(jī)、聯(lián)鎖表抽象機(jī)。

CBTC聯(lián)鎖系統(tǒng)與外部系統(tǒng)的交互行為具有并發(fā)性和不確定性，可被視為一些通信順序進(jìn)程的集合，選用通信順序進(jìn)程進(jìn)行建模。與外部系統(tǒng)的交互行為包括：列車位置的變化、列車模式的變化、進(jìn)路控制命令的下達(dá)。對應(yīng)地采用通信順序進(jìn)程分別建立列車移動(dòng)進(jìn)程TRAINMOVE、列車模式變化進(jìn)程TRLEVCHG和進(jìn)路控制命令進(jìn)程ROUTEOP，這些進(jìn)程具有并發(fā)性。

通過映射關(guān)系使聯(lián)鎖抽象機(jī)與外部交互行為進(jìn)程同步，從而采用集成的形式化方法建立CBTC聯(lián)鎖系統(tǒng)的模型如圖3所示。

2.3 實(shí)例建模

以廣州地鐵7號線鐘村站的站場為例，其信號平面圖如圖4所示，部分聯(lián)鎖進(jìn)路見表1和表2。

圖4 鐘村站站場信號平面圖

進(jìn)路編號進(jìn)路名保護(hù)進(jìn)路名排列進(jìn)路的按鈕主信號級信號開放時(shí)的顯示道岔檢查監(jiān)控邏輯區(qū)段CBTC模式非CBTC模式侵限區(qū)段*7S1910_S1901O_S1901S1910,S1901UW1910,W1916,[W1912],[W1914],(W1918)1910-1916DG1910-1916DG,1918DG,1908G<(W1914)>1912-1914DG,<(W1912)>1912-1914DG8S1910_S1903O_S1903S1910,S1903U(W1910),(W1912),[W1914],[W1916],(W1920)1910-1916DG1910-1916DG,1912-1914DG,1920DG,1905G

續(xù)表1 鐘村站聯(lián)鎖進(jìn)路表

表2 鐘村站保護(hù)進(jìn)路表

2.3.1 采用B方法建立CBTC聯(lián)鎖邏輯狀態(tài)運(yùn)算抽象機(jī)

1)聯(lián)鎖進(jìn)路控制抽象機(jī)

聯(lián)鎖進(jìn)路控制抽象機(jī)是CBTC聯(lián)鎖系統(tǒng)模型的核心，描述了CBTC聯(lián)鎖系統(tǒng)的動(dòng)態(tài)行為。由于聯(lián)鎖進(jìn)路控制規(guī)則的復(fù)雜性，采用分步精化的方式對其進(jìn)行構(gòu)建，即先構(gòu)造初始的聯(lián)鎖進(jìn)路控制抽象機(jī)，再逐步增加相關(guān)的狀態(tài)及操作，使其更加細(xì)化、完善。

聯(lián)鎖進(jìn)路的初始控制抽象機(jī)CBTCIL中，變量部分描述抽象機(jī)操作所涉及的信號機(jī)、道岔、區(qū)段等設(shè)備的內(nèi)部狀態(tài)，如信號機(jī)顯示、處于定位或反位的道岔、道岔的鎖閉、區(qū)段占用、區(qū)段鎖閉等，示例如下。

VARIABLES

signals,

normalPoints,

reversePoints,

unoccupiedTracks,

occupiedTracks,

……

抽象機(jī)的不變式部分，通過集合、關(guān)系、函數(shù)等數(shù)學(xué)概念，描述了變量需要滿足的約束關(guān)系。抽象機(jī)的任何操作被執(zhí)行之后，變量應(yīng)始終維持不變式的成立。例如，處于定位的道岔與處于反位的道岔交集應(yīng)為空集，示例如下。

INVARIANT

normalPoints 〈: POINT &

reversePoints 〈: POINT &

normalPoints ∧ reversePoints = {} &

normalPoints ∨ reversePoints = POINT &

occupiedTracks 〈: TRACK &

unoccupiedTracks 〈: TRACK &

unoccupiedTracks ∧ occupiedTracks = {} &

unoccupiedTracks ∨ occupiedTracks = POINT &

……

抽象機(jī)的初始化部分，對各個(gè)變量進(jìn)行最初的賦值，示例如下。

INITIALISATION

BEGIN

signals := SIGNAL ||

normalPoints := POINT ||

reversePoints := {} ||

……

END

抽象機(jī)的操作部分，描述了聯(lián)鎖進(jìn)路控制的動(dòng)態(tài)行為，包括排列進(jìn)路request、取消進(jìn)路cancel、解鎖進(jìn)路release、列車升級upgrade、列車降級degrade、列車移動(dòng)trainmove等11個(gè)操作，用于描述操作執(zhí)行時(shí)相關(guān)變量的變化規(guī)則。例如，排列進(jìn)路操作request描述了當(dāng)CBTC聯(lián)鎖收到排列進(jìn)路route的命令后，其內(nèi)部的信號機(jī)顯示、道岔位置、道岔鎖閉、區(qū)段鎖閉等抽象機(jī)變量的變化規(guī)則，最后輸出進(jìn)路排列狀態(tài)rsp。抽象機(jī)中的每1個(gè)操作都對應(yīng)于描述外部交互行為的CSP進(jìn)程中的1個(gè)通信事件，被CSP進(jìn)程調(diào)用。操作部分示例如下。

OPERATIONS

npos ← trainmove(t,cpos) =

PREt: TRAIN &t: dom(pos) &

{cpos}=dom({pos(t)})

THEN

movedPoints := {} ||

……

END

rsp ← request(r) =

PREr: ROUTE THEN

IF ((normalTable[{r}] 〈: normalPoints ∨ unlockedPoints)

& (reverseTable[{r}] 〈: reversePoints ∨ unlockedPoints))

THEN

……

END;

……

END

2)信號平面圖抽象機(jī)

信號平面圖描述了站場內(nèi)各設(shè)備的靜態(tài)屬性及其之間的連接拓?fù)潢P(guān)系。信號平面圖抽象機(jī)中定義了站場中的存在的設(shè)備類型包括軌道區(qū)段、信號機(jī)、道岔、計(jì)軸、站臺門、緊急停車按鈕等；站場中每類設(shè)備包含設(shè)備的ID和數(shù)量；link定義了站場中各設(shè)備的線性鏈接關(guān)系。對圖4所示的信號平面圖建立的抽象機(jī)示例如下。

ELEMENT={TRACK, SIGNAL, POINT, AC,

PSD, ESB};

TRACK={1906DG, 1907G, …, 1908G, 1910G};

SIGANL={S1904, X1908, …, X1914, S1901};

POINT={W1906, W1908, …, W1918};

AC={JZ1901, JZ1902, …, JZ1936};

PSD={PSD1901, PSD1902} ;

ESB={ESB1901, ESB1902};

link: ELEMENT ? ELEMENT &

link={(JZ1904→S1904),(S1904→W1906), (W1906→

JZ1916), (W1906→JZ1908), …, (1910G→JZ1901)};

……

3)聯(lián)鎖表抽象機(jī)

聯(lián)鎖表結(jié)合實(shí)際站場的信號平面圖，規(guī)定了每條進(jìn)路控制過程中需要檢查的靜態(tài)規(guī)則,如道岔位置檢查、CBTC進(jìn)路的監(jiān)督區(qū)段檢查等。聯(lián)鎖表抽象機(jī)中定義了聯(lián)鎖表、保護(hù)進(jìn)路表中各類設(shè)備的邏輯狀態(tài)空間，以及相關(guān)數(shù)據(jù)的檢查條件。對表1和表2中的聯(lián)鎖表建立的抽象機(jī)示例如下。

TRACKST={occupied, unoccupied};

TRACKLOCK={locked, unlocked};

ASPECT={red, green, yellow, calling_on, atp_proceed, atp_stop };

SIGNALOPST={bar, unbar};

POINTST={normal,reverse};

POINTLOCK={locked, unlocked};

PSDST={open, closed};

ESBST={actived, non_actived};

……

normalTable: ROUTE ? POINT &

reverseTable: ROUTE ? POINT &

clearTrk_CTC: ROUTE → POW(TRACK) &

clearTrk_ITC: ROUTE → POW(TRACK) &

clearTrack_CTC={R7→{1910_1916DG}, R8→{1910_1916DG}, … }&

clearTrack_ITC={R7→{1910_1916DG, 1918DG, 1908G}, R8→{1910_1916DG,1912_1914DG, 1920DG, 1905G}, … } &

clearTrack_Overlap={O_S1901→{1910G}, O_S1910_1 →{1910_1916DG,1918DG}, …,O_S1910_2→{1910_1916DG,1912_1914DG,1920DG}}

2.3.2 采用通信順序進(jìn)程建立CBTC聯(lián)鎖系統(tǒng)的外部交互進(jìn)程

采用通信順序進(jìn)程對CBTC聯(lián)鎖的外部交互行為進(jìn)行建模，描述CBTC聯(lián)鎖系統(tǒng)和外部系統(tǒng)之間的3類交互行為。其中，TRLEVCHG(t)進(jìn)程描述列車t升級和降級的事件，采用選擇進(jìn)程表示事件之間的關(guān)系。ROUTEOP描述進(jìn)路控制命令進(jìn)程，該進(jìn)程由排列進(jìn)路事件request，取消進(jìn)路事件cancel、解鎖進(jìn)路事件release組成的選擇進(jìn)程。TRAINMOVE(t)描述列車移動(dòng)進(jìn)程，采用混合進(jìn)程方式對列車t的移動(dòng)事件進(jìn)行描述。這些進(jìn)程可視為聯(lián)鎖進(jìn)路控制抽象機(jī)上的操作。CSP模型描述的控制機(jī)驅(qū)動(dòng)著列車移動(dòng)、進(jìn)路操作等事件的產(chǎn)生，控制著聯(lián)鎖抽象機(jī)的狀態(tài)變化。CBTC聯(lián)鎖系統(tǒng)的外部交互進(jìn)程示例如下。

TRLEVCHG(t)=

([]t: TRAIN @ upgrade!t?level → TRLEVCHG)

[]

([]t: TRAIN @ degrade!t?level → TRLEVCHG)

ROUTEOP=

([]r: ROUTE @ request!r?rsp → ROUTEOP)

[]

([]r: ROUTE @ cancel!r?rsp → ROUTEOP)

[]

([]r: ROUTE @ release!r?rsp → ROUTEOP)

TRAINMOVE(t)=

[]bPos: BEGIN @ enter!t!bPos → TRAINOP(t,bPos)

……

ALL_TRAINSOP=||| t : TRAIN @ TRAINMOVE(t)

CTRL=ROUTEOP ||| ALL_TRAINSOP ||| TRLEVCHG

MAIN=CTRL

2.3.3 對CBTC聯(lián)鎖模型進(jìn)行分步精化

完成了CBTC聯(lián)鎖系統(tǒng)的初始模型構(gòu)建后，需要將模型進(jìn)一步完善、細(xì)化。以初建的聯(lián)鎖進(jìn)路控制抽象機(jī)為例，通過分析聯(lián)鎖進(jìn)路控制的過程，將聯(lián)鎖進(jìn)路控制分解為進(jìn)路鎖閉、進(jìn)路開放、進(jìn)路關(guān)閉、進(jìn)路解鎖等階段狀態(tài)。針對這些聯(lián)鎖進(jìn)路控制的不同階段，分別引入新的狀態(tài)變量、不變式、操作，使得已開發(fā)出的抽象模型逐步變換到更具體的模型，并逐步生成最終的聯(lián)鎖進(jìn)路控制抽象機(jī)。

第1步：增加站臺門、緊急停車等設(shè)備的狀態(tài)變量，補(bǔ)充這些狀態(tài)需要滿足的不變式關(guān)系，并按照進(jìn)路檢查規(guī)則，將它們的狀態(tài)補(bǔ)充到排列進(jìn)路操作部分。

第2步：結(jié)合進(jìn)路鎖閉的過程，增加已解鎖區(qū)段、鎖閉的進(jìn)路等狀態(tài)變量；補(bǔ)充不變式，描述這些狀態(tài)之間的固有關(guān)系。

第3步：結(jié)合進(jìn)路開放的過程，增加信號機(jī)模式等狀態(tài)變量；補(bǔ)充相應(yīng)的不變式關(guān)系和操作。

第4步：結(jié)合進(jìn)路關(guān)閉的過程，增加封閉信號機(jī)等變量；補(bǔ)充相應(yīng)的不變式關(guān)系和操作。

第5步：結(jié)合進(jìn)路解鎖的過程，在解鎖進(jìn)路操作中增加‘三點(diǎn)檢查’等安全解鎖邏輯規(guī)則。

在分步精化的框架下，通過對初始模型進(jìn)行狀態(tài)擴(kuò)充、場景加強(qiáng)和細(xì)化分解，最終得到較成熟的CBTC聯(lián)鎖系統(tǒng)模型。

3 CBTC聯(lián)鎖系統(tǒng)的形式化驗(yàn)證

形式化驗(yàn)證，即采用形式化的方法驗(yàn)證已有的系統(tǒng)軟件是否滿足其規(guī)約的要求。目前常見的形式驗(yàn)證方法為模型檢驗(yàn)。模型檢驗(yàn)通過搜索待驗(yàn)證系統(tǒng)模型的有窮狀態(tài)空間，來檢驗(yàn)系統(tǒng)的行為是否具備預(yù)測屬性的一種自動(dòng)驗(yàn)證技術(shù)[14]。目前，模型檢驗(yàn)方法被廣泛應(yīng)用于計(jì)算機(jī)硬件、通信協(xié)議、安全認(rèn)證協(xié)議、控制系統(tǒng)等方面的分析和驗(yàn)證中，已經(jīng)成為形式驗(yàn)證的核心方法。

國內(nèi)外很多研究機(jī)構(gòu)和大學(xué)都開發(fā)了實(shí)用的模型檢驗(yàn)工具。ProB[15]是一個(gè)支持B，CSP，Z和TLA+等多種模型的形式驗(yàn)證工具，并能支持對CSP和B的集成模型進(jìn)行驗(yàn)證。它能遍歷模型的狀態(tài)空間，記錄下每個(gè)狀態(tài)變遷，并加以圖形顯示。通過模型行為的圖形化分析、模型檢驗(yàn)、一致性驗(yàn)證等方法來驗(yàn)證模型是否滿足所期望的屬性，或給出違反系統(tǒng)期望屬性的反例，從而幫助設(shè)計(jì)者追蹤到出錯(cuò)的地方。本文采用ProB工具對建立的CBTC聯(lián)鎖系統(tǒng)模型的安全性和無死鎖性進(jìn)行驗(yàn)證，從而保證CBTC聯(lián)鎖系統(tǒng)的安全性和無死鎖性。

3.1 安全性驗(yàn)證

CBTC聯(lián)鎖系統(tǒng)模型的安全功能，是通過B抽象機(jī)中的不變式加以約束定義的。通過ProB工具對模型的整個(gè)狀態(tài)空間進(jìn)行遍歷搜索，檢測是否存在違反不變式的情況。當(dāng)發(fā)現(xiàn)有違反不變式的情況時(shí)，ProB工具自動(dòng)給出其路徑，幫助確定是模型數(shù)據(jù)的錯(cuò)誤還是性質(zhì)描述的錯(cuò)誤。 在對鐘村站初期的CBTC聯(lián)鎖模型進(jìn)行驗(yàn)證時(shí)，驗(yàn)證結(jié)果自動(dòng)演示出1條違反安全性的反例路徑。通過查看該反例路徑得知，存在下列反例導(dǎo)致違反不變式的情況出現(xiàn)：當(dāng)列車TrainA位于區(qū)段1918DG上時(shí)，由于進(jìn)路R7開放前沒能檢查1918DG的占用狀態(tài)，進(jìn)路可以開放黃燈信號，列車TrainB會前行與列車TrainA發(fā)生追尾，示例如下。

〈enter.TrainA.1918DG,

enter.TrainB.1904DG,

request.R7.true,

nextSignal.TrainB.yellow,

move.TrainB.1904G.1910_1916DG,

nextSignal.TrainB.none,

move.TrainB.1910_1916DG.1918DG〉

通過工具提示的反例路徑進(jìn)一步分析檢查，發(fā)現(xiàn)錯(cuò)誤的原因是在系統(tǒng)建模時(shí)，聯(lián)鎖模型中“非CBTC模式下進(jìn)路監(jiān)控區(qū)段”1項(xiàng)模型數(shù)據(jù)錯(cuò)誤所導(dǎo)致的。根據(jù)工具提示的信息，針對性地進(jìn)行了模型調(diào)整。如此對模型多次調(diào)整后，再對模型進(jìn)行驗(yàn)證，驗(yàn)證時(shí)共計(jì)對模型的1 816個(gè)系統(tǒng)狀態(tài)、10 679個(gè)狀態(tài)遷移進(jìn)行了100%的覆蓋檢測，結(jié)果如圖5所示，表明系統(tǒng)的整個(gè)狀態(tài)空間中，未發(fā)現(xiàn)違反不變式的情況。從而驗(yàn)證了該模型的安全性滿足要求。

圖5 CBTC聯(lián)鎖的模型檢驗(yàn)結(jié)果

CBTC聯(lián)鎖模型的安全性驗(yàn)證，還可進(jìn)一步通過ProB工具的計(jì)算樹邏輯(Computation Tree Logic,CTL)斷言檢查功能來實(shí)現(xiàn)。為了驗(yàn)證模型中描述的collision和derailment等進(jìn)程事件是否出現(xiàn)，在ProB工具中輸入下列CTL表達(dá)式：

AG(not(e(collision))& not (e(derailment)) & not(e(runthrough)))

其中路徑量詞AG代表‘對于所有路徑，命題永遠(yuǎn)為真’；路徑量詞e代表‘至少某1條路徑，命題為真’。結(jié)果顯示CTL表達(dá)式為真，驗(yàn)證通過，如圖6所示。

圖6 CBTC聯(lián)鎖模型的CTL驗(yàn)證結(jié)果

3.2 無死鎖性驗(yàn)證

無死鎖性表示系統(tǒng)不會在某個(gè)狀態(tài)上無限停留，即無論系統(tǒng)處于哪一個(gè)狀態(tài)，總有確定的下一步狀態(tài)可以被執(zhí)行。無死鎖性的線性時(shí)序邏輯(Linear Temporal Logic，LTL)表達(dá)式為

assert MAIN:[deadlock free]

采用ProB工具對模型的無死鎖性進(jìn)行驗(yàn)證，若驗(yàn)證結(jié)果存在死鎖，則通過反例檢查模型的死鎖是如何發(fā)生的，對模型做出相應(yīng)的改動(dòng)，避免死鎖的發(fā)生。CBTC聯(lián)鎖模型的無死鎖性驗(yàn)證結(jié)果如圖7所示，可以看出該模型的各進(jìn)程無死鎖性驗(yàn)證通過。

圖7 CBTC聯(lián)鎖模型的無死鎖性驗(yàn)證結(jié)果

4 結(jié) 語

本文將適合于描述系統(tǒng)并發(fā)特性的通信順序進(jìn)程與適合于描述系統(tǒng)狀態(tài)的B方法進(jìn)行集成，即在通信順序進(jìn)程的通信事件與B方法抽象機(jī)的操作之間建立起一對一的映射關(guān)系，實(shí)現(xiàn)通信事件通過控制抽象機(jī)的操作，進(jìn)而影響抽象機(jī)的狀態(tài)，這樣，進(jìn)程與抽象機(jī)之間的映射實(shí)現(xiàn)了通信順序進(jìn)程和B方法之間的同步。

CBTC聯(lián)鎖系統(tǒng)是一種典型的復(fù)雜安全苛求系統(tǒng)，既具有復(fù)雜的內(nèi)部狀態(tài)空間，又具有并發(fā)的外部交互行為。采用B方法對CBTC聯(lián)鎖系統(tǒng)的邏輯狀態(tài)運(yùn)算建立抽象機(jī)，采用通信順序進(jìn)程對CBTC聯(lián)鎖系統(tǒng)與外部系統(tǒng)的并發(fā)交互行為建立進(jìn)程，并通過映射關(guān)系將聯(lián)鎖抽象機(jī)與外部交互行為進(jìn)程進(jìn)行同步，由此建立了基于CSP和B方法的CBTC聯(lián)鎖系統(tǒng)的形式化模型。

采用形式化工具ProB，對建立的CBTC聯(lián)鎖系統(tǒng)模型的安全性、無死鎖性進(jìn)行驗(yàn)證，發(fā)現(xiàn)并修改了模型中的不一致、不完全、歧義等錯(cuò)誤，從而驗(yàn)證了CBTC聯(lián)鎖系統(tǒng)的安全性和無死鎖性，保證了系統(tǒng)的最終實(shí)現(xiàn)。

[1] 陳火旺，王戟，董威. 高可信軟件工程技術(shù)[J]. 電子學(xué)報(bào)，2003，31 (12A): 1933-1938.

(CHEN Huowang，WANG Ji，DONG Wei. High Confidence Software Engineering Technologies[J]. Acta Electronica Sinica，2003，31(12A)：1933-1938. in Chinese)

[2] 國際電工委員會. IEC 62279—2002 鐵路應(yīng)用：通信,信號和處理系統(tǒng)——鐵路控制和防護(hù)系統(tǒng)用軟件[S]. 日內(nèi)瓦：國際電工委員會，2002.

(International Electrotechnical Commission. IEC 62279—2002 Railway Applications—Communications, Signalling and Processing Systems—Software for Railway Control and Protection Systems[S]. Geneva: International Electrotechnical Commission，2002.in Chinese)

[3] WINTER K. Model Checking Railway Interlocking Systems [C]//Proceedings of the 25th Austral-Asian Conference on Computer Sciences. Melbourne：Australian Computer Science Communications, 2002:303-310.

[4] WINTER K. Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings [C]// 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Berlin：Lecture Notes in Computer Science, 2012: 246-260.

[5] KIRSTEN Mark Hansen. Modeling Railway Interlocking Systems [EB/OL]. Available via ftp from ftp.ifad.dk, directory /pub/vdm/examples, 1994.

[6] VICKY Hartonas-Garmhausen, EDMUND Clarke, SERGIO Campos, et al. Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints [J]. Science of Computer Programming, 2000, 36(1): 53-64.

[7] THIERRY Lecomte. Safe and Reliable Metro Platform Screen Doors Control/Command System [C] //Proceedings of the 15th International Symposium on Formal Methods. Berlin：Springer-Verlag，2008：430-434.

[8] ABO Rober，VOISIN Laurent. Formal Implementation of Data Validation for Railway Safety-Related Systems with OVADO[C]// International Conference on Software Engineering & Formal Methods.Madrid:Lecture Notes in Computer Science,2013:221-236.

[9] 陳銘松，鮑勇翔，孫海英,等.基于通信的列車控制系統(tǒng)可信構(gòu)造：形式化方法綜述[J].軟件學(xué)報(bào)，2017,28(5)：1183-1203.

(CHEN Mingsong，BAO Yongxiang，SUN Haiying, et al. Survey on Formal Method of Trustworthy Construction for Communication-Based Train Control Systems[J]，Journal of Software, 2017,28(5)：1183-1203. in Chinese)

[10] ZAFAR Nazir Ahmad, KHAN Sher Afzal, ARAKI Keijiro.Towards the Safety Properties of Moving Block Railway Interlocking System[J].International Journal of Innovative Computing Information & Control，2012,8(8):5677-5690.

[11] 張廣泉. 形式化方法導(dǎo)論 [M]. 北京：清華大學(xué)出版社，2015.

[12] HOARE C A R. Communicating Sequential Processes [M]. London：Prentice Hall International, 1985.

[13] ABRIAL J R. The B-Book: Assigning Programs to Meaning [M]. London: Cambridge University Press, 1996: 156-257.

[14] 古天龍. 軟件開發(fā)的形式化方法 [M].北京：高等教育出版社，2005.

[15] LEUSCHEL Michael, BUTLER Michael. ProB: an Automated Analysis Toolset for the B Method [J]. International Journal on Software Tools for Technology Transfer, 2008,10(2):185-203.