基于通信顺序进程与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.