第39卷，第3期
2 0 1 8年5月c中酬!m d Vol. 39 No.
3 M ay, 2018
文章编号：1001-4632 (2018) 03-00101-09
基于通信顺序进程与B方法的C B T C计算机
联锁系统的形式化建模与验证
王鲲1>2
(1.中国铁道科学研究院通信信号研究所，北京100081;
2.国家铁路智能运输系统工程技术研究中心，北京100081)
摘要：针对CBTC联锁系统的复杂性，提出一种基于通信顺序进程（CSP)与B方法集成的形式化方法，即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系，实现通信事件通过控制抽 象机的操作、进而影响抽象机状态的目标，从而实现通信顺序进程和B方法之间的同步。以1个实际站
场为例，采用B方法对具有复杂状态空间的CBTC联锁系统的逻辑状态运算建立抽象机，采用通信顺序进程对CBTC联 锁系统与外部系统的并发交互行为建立进程，并通过映射关系使CBTC联锁系统的抽象机与外部交互行为进程 同步，由此建立基于通信顺序进程与B方法的CBTC联锁系统的形式化模型。采用ProB工具对建立的CBTC联 锁系统模型的安全性、无死锁性进行验证。发现并修改模型中的不一致、不完全、歧义等错误，从而验证了 CBTC联锁系统的安全性和无死锁性，保证了系统的最终实现。
关键词：城市轨道交通；C B T C；计算机联锁系统；形式化方法；通信顺序进程；B方法
中图分类号：U284 文献标识码：A doi：10. 3969/j. issn. 1001-4632. 2018. 03.14
在基于通信的列车控制（Communication Based Train Control, C B T C)系统中，计算机联锁系统（简称C B T C联锁系统）是重要的基础设备之一。随着C B T C技术日趋精密复杂，C B T C联锁系统不仅需要通过复杂的逻辑状态运算以实现对联锁进路、信号机、道岔、轨道区段、站台门、防淹门等的控制，还需要与外部系统进行实时通信，实现数据交互，而且在进行逻辑计算时涉及巨大的内部状态空间，在与外部系统实时通信时引入了大量的并发性和不确定性，因此该系统是一种典型的复杂安全苛求系统。同时，C B T C联锁系统的关键性质与其功能性混合在一起，并与软件开发的全过程密切相关，使得这些关键性质的获得和保证变得更加复杂。因此，如何在C B T C联锁系统软件的开发和维护中保证软件具有所需的安全性、无死锁性等关键性质，成为了重要的研究方向。
统计表明，传统的非形式化的软件工程技术对软件质量的保证具有一个难以逾越的顶点，而形式化方法的实践证明形式化方法是提高软件质量的重要途径[1]。形式化的方法通过严格的数学方法，定性定量地描述软件的行为，建立关键性质与软件行为之间的内在联系和严格描述，从而设计并验证软件所需的关键性质。标准IEC62279: 2002《铁路应用：通信、信号、处理系统——铁路控制和防护系统软件》[2]中指出：“在软件安全完善度等级为4级时，软件需求规格说明书定义、软件设计和实施、验证和测试等过程中，强力推荐使用形式化方法进行描述和设计；在对软件验证和测试时，强力推荐使用形式化证明技术”。
国内外的学者们对铁路联锁系统的形式建模及验证进行了研究。Kirsten W I N T E R S在联锁软件分析设计的早期，分别采用了通信顺序进程和符号模型检验工具进行模型检验，并将其运用在昆士兰铁路项目中。K IR ST E N Mark Hansen[5]采用基于维也纳开发方法（V D M)，对丹麦铁路系统中联锁系统进行了建模与验证。Vicky Hartonas-Garm-hausen™等利用符号模型检验工具（S M V)对铁路联锁系统的动态行为进行建模，研究状态空间约
收稿日期：2017-08-20；修订日期：2017-12-13
基金项目：中国铁路总公司科技研究开发计划项目（J2016X001)；中国铁道科学研究院行业服务技术创新项目（2016YJ053) 第一作者：王餛（1977—），男，河南焦作人，副研究员。E-mail: wk@rails
102中国铁道科学第39卷
简的方法，发现了系统中潜在的不安全行为路径，并提出了系统改进的建议。
在城市轨道交通领域，也有一些学者基于形式化方法进行了研究。Thierry Lecomte[7]等提出了基于B方法的城市轨道交通站台门控制系统的建模和验证，目的在于保证故障模式下系统可以正确地实现其功能。Robert A bo[8]等采用B方法对C B T C系统的数据进行确认，并纠正了规约中的一些错误。陈铭松[9]等提出了以形式化方法为主要技术切入点的C B T C可信构造框架，提供相应的形式化方法与工具，支持全生命周期内系统功能与非功能属性的建模与验证。Nazir Ahmad Zafar[1°]采用图论和Z语言方法对移动闭塞联锁系统进行建模，X才其安全属性进行检验。但是，以上这些研究成果，均采用的是某一种形式化方法，而CBTC 联锁系统不仅具有巨大的状态空间，还具有并发的信息交互行为，仅采用单一的形式化方法进行建模，难以适用其复杂系统的多种特性。
为了能够更加全面、准确地描述C B T C联锁系统的复杂性，本文提出将适合于描述系统并发特性的通信顺序进程（Communication Sequential Processes, C S P)与适合于描述系统状态的B方法两者集成的形式化方法，对C B T C联锁系统进行建模和验证，以保证C B T C联锁系统软件的安全性和无死锁性。
1形式化方法
形式化方法是指具有严格数学基础的软件和系统开发方法，支持计算机系统及软件的规约、设计、验证与演化等活动[11]。形式化方法的目标是建立精确的、无二义性的语义，对系统开发各个阶段的模型进行有效的描述，使系统结构具有先天的合理性和正确性，良好的维护性，从而较好地满足用户需求。众多的形式化方法中，通信顺序进程和B方法是2种基于不同理论基础的形式化方法。1.1通信顺序进程
通信顺序进程[12]是一种基于进程代数的形式化方法，适合于分布式系统和并发系统的开发。该方法的基本原理：提供了描述和分析系统各个进程之间交互的实体行为的数学框架，进程内部通过信息的交互而相互作用和影响；可对进程的各个阶段进行精确定义和验证，具有严格的数学逻辑；主要通过进程事件的集合、进程的迹、进程间的通信描述进程的行为，通过并发、选择、递归等描述进程
之间的关系。该方法的基本概念归纳如下。
(1)进程是指事件或活动的序列，设P是1进程，该进程的第1个事件是心且事件:c执行之后，进程P的剩余部分为Q，则进程P可表示为I—Q，其中事件工称为前缀；工6o P，  a (1 —Q) =a_P，其中《为1个运算子，将每一个进程映
射为它的事件集。
(2)进程的迹是1个进程所执行事件历史行的符号记录。对于进程P，用表示进程P
所有可能迹的集合。
(3)进程之间可以通过运算操作进行复合，而实现对复杂问题的描述。运算操作包括：并发进
程P I I Q、或进程P「l Q、选择进程？□0、屏蔽进
程P/Q、混合进程P I I I Q、顺序进程p; Q等。
(4)进程之间存在相同事件的交互，这种交的事件称为通信事件，记为c.w，其中c为信道名，U为所传递的消息值。1个起始执行在信道C上输
出消息t；的进程可表示为
(c!v^~P) =ic.v^P)
1个起始执行从信道C上输入可通信的消息T，并接着执行P(I)的进程，可表示为
(c?x^-P(x))=i y：{y I ch an n e liy) =c} ^
P{message Cy)))
1.2 B方法
B方法[13]是一种基于状态的形式化方法，通
过数学的推理或逻辑演算，逐步建立起基于数学理
论基础的体系，这个体系既可以构造软件系统的状
态和行为特征，如抽象机、广义代换语言等，也可
以通过类型检查和证明义务证明该体系语义语法的
正确性，并通过模型精化让抽象模型变得丰富、具体。
抽象机是B方法中的基本单元，用于描述软
件系统的1个子模块，多个抽象机集合组成软件系
统的模型。抽象机由抽象机名、变量、不变式、初
始化和操作等构成，基本形式为：
MACHINE M (•••)
VARIABLES —
INVARIANT -
INITIALISATION …
OPERATIONS -
END
其中1个典型的操作可表述为
output—operate (input) =PRE G THEN S END
该操作中：operate为操作名；ou tp u t 为输出
第3期基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证103
变量；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 C B T C联锁系统的形式化建模
2. 1C B T C联锁系统
CBTC计算机联锁系统是应用于城市轨道交通 领域的安全苛求系统。它采用计算机、通信、控制 相结合的技术手段，实现对联锁进路、道岔、信号 机、轨道区段、站台门、防淹门等设备的逻辑状态 运算，并通过继电接口对这些设备进行监督和控 制，通过安全通信接口与区域控制中心（ZC)、车 载控制器（
VOBC)、列车自动监控系统（A T S)、相邻联锁系统（NCBI)、线路电子单元（LEU)等外部系统进行实时通信，实现数据的交互，从而 协同完成列车运行的控制，保证列车运行安全，有 效地提高运输效率和运输自动化水平。描述CBTC 联锁系统功能行为的用例图如图2所示。
图2 CBTC联锁系统的用例图
2.2C B T C联锁系统的形式化模型
CB TC联锁系统的逻辑状态运算行为具有复杂 的状态空间，选用B方法建模，即采用抽象机及 其操作进行描述。CBTC联锁系统的逻辑状态运算 可分为联锁进路控制、站场信号平面图和联锁表3 部分，对应地采用B方法分别构建联锁进路控制 抽象机、信号平面图抽象机、联锁表抽象机。
CBTC联锁系统与外部系统的交互行为具有并 发性和不确定性，可被视为一些通信顺序进程的集 合，选用通信顺序进程进行建模。与外部系统的交 互行为包括：列车位置的变化、列车模式的变化、进路控制命令的下达。对应地采用通信顺序进程分 别建立列车移动进程TRAINMOVE、列车模式变 化进程T R L E V C H G和进路控制命令进程ROUTEOP，这些进程具有并发性。
通过映射关系使联锁抽象机与外部交互行为进 程同步，从而采用集成的形式化方法建立CBTC 联锁系统的模型如图3所示。
图3采用集成形式化方法建立的CBTC
联锁系统模型
2.3实例建模平面图如图4所示，部分联锁进路见表1和表2。
以广州地铁7号线钟村站的站场为例，其信号
104 中国铁道科学第39卷
表1钟村站联锁进路表
进路编号
主信号级监控逻辑区段
进路名保护进路名排列进路的按钮信号开放
时的显示
道岔检查CBTC模式非CBTC模式侵限区段*
7S1910_S1901O_S1901S1910，S1901U W1910,W1916,[W1912],
[W1914],(W1918)
1910-1916D G
1910-1916D G,
1918DGJ908G
((W1914))1912-1914D G,
<(W1912)>1912-1914D G
8S1910_S1903O_S1903S1910,S1903U
(W1910), (W1912 ),
[W1914],
[W1916],(W1920)
1910-1916D G
1910-1916D G,
1912-1914D G,
1920DGJ905G 续表1钟村站联锁进路表
进路编号进路名紧停按钮屏蔽门防淹门敌对信号
敌对保护进路
未锁闭
互斥进路接近锁闭区段
引导检
查区段
延时解
锁时间
跨区
进路
其他
联锁
7S1910_S1901E S B1902_E S B1904P S D1902X1914,
X2007V
0_X1914_2X1904
<(W1902)>1902G_H,1902G_1,
1902D G,1904D G,1904G
1904G60S N
8S1910_S1903E S B1901_E S B1903P S D1901X1916,
X2002
0_X1916_3X1906
((W1902))1902G_H,1902G_I,
1902D G,1904D G,1904G
1904G60S N 表2钟村站保护进路表
保护进路编号保护进路
名称
起始信号区段侵限区段道岔敌信号敌路
站台保护区段强制解锁时间
(列车压入站台后）
其他
联锁
22 23〇_S1901
〇_S1903
S1901
S1903
1910G
1930G
X2007V
X2002
40S
40S
2.3.1采用B方法建立CB T C联锁逻辑状态运算
抽象机
1)联锁进路控制抽象机
联锁进路控制抽象机是C B T C联锁系统模型 的核心，描述了 C B T C联锁系统的动态行为。由于联锁进路控制规则的复杂性，采用分步精化的方 式对其进行构建，即先构造初始的联锁进路控制抽 象机，再逐步增加相关的状态及操作，使其更加细 化、完善。
联锁进路的初始控制抽象机C B T C IL中，变 量部分描述抽象机操作所涉及的信号机、道岔、区 段等设备的内部状态，如信号机显示、处于定位或 反位的道岔、道岔的锁闭、区段占用、区段锁闭 等，示例如下。
VARIABLES
signals，
normalPoints，
reversePoints,
unoccupiedT r acks,
occupiedT r acks,
抽象机的不变式部分，通过集合、关系、函数 等数学概念，描述了变量需要满足的约束关系。抽 象机的任何操作被执行之后，变量应始终维持不变 式的成立。例如，处于定位的道岔与处于反位的道 岔交集应为空集，示例如下。
INVARIANT
normalPoints <：POINT &
reversePoints <：POINT &
normalPoints 八reversePoints ={} &
normalPoints V reversePoints =POINT
&
第3期基于通信顺序进程与B方法的C B T C计算机联锁系统的形式化建模与验证105
occupiedTracks〈：TRACK
unoccupiedTracks (：TRACK &*
unoccupiedTracks A occupiedTracks ={} &
unoccupiedTracks V 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 (i, epos)=
PRE t：TRAIN & t：dom (pos) &.
{epos} =dom ( {pos (/)})
THEN
movedPoints ：={} ||
END
rsp — request (r)=
PRE r：ROUTE THEN
IF ((normalTable [{r}] <：normalPoints V unlockedPoints) &. (reverseTable [ {r}]〈：reversePoints V unlocked­
Points) )
THEN
END；
END
2)信号平面图抽象机
信号平面图描述了站场内各设备的静态属性及 其之间的连接拓扑关系。信号平面图抽象机中定义 了站场中的存在的设备类型包括轨道区段、信号机、道岔、计轴、站台门、紧急停车按钮等；站场 中每类设备包含设备的I D和数量；lin k定义了站 场中各设备的线性链接关系。对图4所示的信号平 面图建立的抽象机示例如下。
ELEMENT={TRACK, SIGNAL, POINT, AC,
PSD, ESB}；
TRACK= {1906DG, 1907G, *•*, 1908G, 1910G}；
SIGANL= {S1904, X1908, X1914, S1901}；
POINT= {W1906, W1908,…，W1918};
A C= {JZ1901, JZ1902,…，JZ1936};
PSD= {PSD1901, PSD1902}；
ESB= {ESB1901, ESB1902}；
link：ELEMENT ELEMENT &
link={ (JZ1904^S1904), (S1904-^W1906), (W1906^ JZ1916), (W1906—JZ1908)，•••，（19100+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_ Overlaps {0_ SI901-*- {1910G}, O _ S1910 _ 1
—{1910 _ 1916DG, 1918DG}，…，
O_S1910_2 ^{1910 _ 1916DG,
1912_1914DG, 1920DG}}
2. 3. 2采用通信顺序进程建立C B T C联锁系统的
外部交互进程
采用通信顺序进程对C B T C 联锁的外部交互

版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。