基于通信順序進程與B方法的CBTC計算機聯鎖系統的形式化建模與驗證

王 鯤

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

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

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

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

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

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

1 形式化方法

形式化方法是指具有嚴格數學基礎的軟件和系統開發方法，支持計算機系統及軟件的規約、設計、驗證與演化等活動[11]。形式化方法的目標是建立精確的、無二義性的語義，對系統開發各個階段的模型進行有效的描述，使系統結構具有先天的合理性和正確性，良好的維護性，從而較好地滿足用戶需求。眾多的形式化方法中，通信順序進程和B方法是2種基于不同理論基礎的形式化方法。

1.1 通信順序進程

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

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

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

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

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

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

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

1.2 B方法

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

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

MACHINE M(…)

VARIABLES …

INVARIANT …

INITIALISATION …

OPERATIONS …

END

其中1個典型的操作可表述為

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

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

1.3 通信順序進程與B方法的集成

通信順序進程以‘事件驅動’模式對并發系統進行建模與驗證，但不適合于具有復雜狀態空間的軟件系統；B方法側重于對具有復雜狀態空間的軟件系統描述，但不適合描述并發系統的交互行為；因此將這2種方法進行集成，可以用于全面地刻畫具有復雜狀態空間及并發交互行為的軟件系統。

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

圖1 通信順序進程與B方法的集成

2 CBTC聯鎖系統的形式化建模

2.1 CBTC聯鎖系統

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

圖2 CBTC聯鎖系統的用例圖

2.2 CBTC聯鎖系統的形式化模型

CBTC聯鎖系統的邏輯狀態運算行為具有復雜的狀態空間，選用B方法建模，即采用抽象機及其操作進行描述。CBTC聯鎖系統的邏輯狀態運算可分為聯鎖進路控制、站場信號平面圖和聯鎖表3部分，對應地采用B方法分別構建聯鎖進路控制抽象機、信號平面圖抽象機、聯鎖表抽象機。

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

通過映射關系使聯鎖抽象機與外部交互行為進程同步，從而采用集成的形式化方法建立CBTC聯鎖系統的模型如圖3所示。

2.3 實例建模

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

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

進路編號進路名保護進路名排列進路的按鈕主信號級信號開放時的顯示道岔檢查監控邏輯區段CBTC模式非CBTC模式侵限區段*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

續表1 鐘村站聯鎖進路表

表2 鐘村站保護進路表

2.3.1 采用B方法建立CBTC聯鎖邏輯狀態運算抽象機

1)聯鎖進路控制抽象機

聯鎖進路控制抽象機是CBTC聯鎖系統模型的核心，描述了CBTC聯鎖系統的動態行為。由于聯鎖進路控制規則的復雜性，采用分步精化的方式對其進行構建，即先構造初始的聯鎖進路控制抽象機，再逐步增加相關的狀態及操作，使其更加細化、完善。

聯鎖進路的初始控制抽象機CBTCIL中，變量部分描述抽象機操作所涉及的信號機、道岔、區段等設備的內部狀態，如信號機顯示、處于定位或反位的道岔、道岔的鎖閉、區段占用、區段鎖閉等，示例如下。

VARIABLES

signals,

normalPoints,

reversePoints,

unoccupiedTracks,

occupiedTracks,

……

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

INVARIANT

normalPoints 〈: POINT &

reversePoints 〈: POINT &

normalPoints ∧ reversePoints = {} &

normalPoints ∨ reversePoints = POINT &

occupiedTracks 〈: TRACK &

unoccupiedTracks 〈: TRACK &

unoccupiedTracks ∧ occupiedTracks = {} &

unoccupiedTracks ∨ occupiedTracks = POINT &

……

抽象機的初始化部分，對各個變量進行最初的賦值，示例如下。

INITIALISATION

BEGIN

signals := SIGNAL ||

normalPoints := POINT ||

reversePoints := {} ||

……

END

抽象機的操作部分，描述了聯鎖進路控制的動態行為，包括排列進路request、取消進路cancel、解鎖進路release、列車升級upgrade、列車降級degrade、列車移動trainmove等11個操作，用于描述操作執行時相關變量的變化規則。例如，排列進路操作request描述了當CBTC聯鎖收到排列進路route的命令后，其內部的信號機顯示、道岔位置、道岔鎖閉、區段鎖閉等抽象機變量的變化規則，最后輸出進路排列狀態rsp。抽象機中的每1個操作都對應于描述外部交互行為的CSP進程中的1個通信事件，被CSP進程調用。操作部分示例如下。

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)信號平面圖抽象機

信號平面圖描述了站場內各設備的靜態屬性及其之間的連接拓撲關系。信號平面圖抽象機中定義了站場中的存在的設備類型包括軌道區段、信號機、道岔、計軸、站臺門、緊急停車按鈕等；站場中每類設備包含設備的ID和數量；link定義了站場中各設備的線性鏈接關系。對圖4所示的信號平面圖建立的抽象機示例如下。

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)聯鎖表抽象機

聯鎖表結合實際站場的信號平面圖，規定了每條進路控制過程中需要檢查的靜態規則,如道岔位置檢查、CBTC進路的監督區段檢查等。聯鎖表抽象機中定義了聯鎖表、保護進路表中各類設備的邏輯狀態空間，以及相關數據的檢查條件。對表1和表2中的聯鎖表建立的抽象機示例如下。

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 采用通信順序進程建立CBTC聯鎖系統的外部交互進程

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

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聯鎖模型進行分步精化

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

第1步：增加站臺門、緊急停車等設備的狀態變量，補充這些狀態需要滿足的不變式關系，并按照進路檢查規則，將它們的狀態補充到排列進路操作部分。

第2步：結合進路鎖閉的過程，增加已解鎖區段、鎖閉的進路等狀態變量；補充不變式，描述這些狀態之間的固有關系。

第3步：結合進路開放的過程，增加信號機模式等狀態變量；補充相應的不變式關系和操作。

第4步：結合進路關閉的過程，增加封閉信號機等變量；補充相應的不變式關系和操作。

第5步：結合進路解鎖的過程，在解鎖進路操作中增加‘三點檢查’等安全解鎖邏輯規則。

在分步精化的框架下，通過對初始模型進行狀態擴充、場景加強和細化分解，最終得到較成熟的CBTC聯鎖系統模型。

3 CBTC聯鎖系統的形式化驗證

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

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

3.1 安全性驗證

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

〈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〉

通過工具提示的反例路徑進一步分析檢查，發現錯誤的原因是在系統建模時，聯鎖模型中“非CBTC模式下進路監控區段”1項模型數據錯誤所導致的。根據工具提示的信息，針對性地進行了模型調整。如此對模型多次調整后，再對模型進行驗證，驗證時共計對模型的1 816個系統狀態、10 679個狀態遷移進行了100%的覆蓋檢測，結果如圖5所示，表明系統的整個狀態空間中，未發現違反不變式的情況。從而驗證了該模型的安全性滿足要求。

圖5 CBTC聯鎖的模型檢驗結果

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

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

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

圖6 CBTC聯鎖模型的CTL驗證結果

3.2 無死鎖性驗證

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

assert MAIN:[deadlock free]

采用ProB工具對模型的無死鎖性進行驗證，若驗證結果存在死鎖，則通過反例檢查模型的死鎖是如何發生的，對模型做出相應的改動，避免死鎖的發生。CBTC聯鎖模型的無死鎖性驗證結果如圖7所示，可以看出該模型的各進程無死鎖性驗證通過。

圖7 CBTC聯鎖模型的無死鎖性驗證結果

4 結 語

本文將適合于描述系統并發特性的通信順序進程與適合于描述系統狀態的B方法進行集成，即在通信順序進程的通信事件與B方法抽象機的操作之間建立起一對一的映射關系，實現通信事件通過控制抽象機的操作，進而影響抽象機的狀態，這樣，進程與抽象機之間的映射實現了通信順序進程和B方法之間的同步。

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

采用形式化工具ProB，對建立的CBTC聯鎖系統模型的安全性、無死鎖性進行驗證，發現并修改了模型中的不一致、不完全、歧義等錯誤，從而驗證了CBTC聯鎖系統的安全性和無死鎖性，保證了系統的最終實現。

[1] 陳火旺，王戟，董威. 高可信軟件工程技術[J]. 電子學報，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 鐵路應用：通信,信號和處理系統——鐵路控制和防護系統用軟件[S]. 日內瓦：國際電工委員會，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] 陳銘松，鮑勇翔，孫海英,等.基于通信的列車控制系統可信構造：形式化方法綜述[J].軟件學報，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] 張廣泉. 形式化方法導論 [M]. 北京：清華大學出版社，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] 古天龍. 軟件開發的形式化方法 [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.