车站联锁系统行为验证与数据确认的形式化方法

王恪铭 ，王 霞 ，程 鹏 ，刘 宁 ，张传东

（1.西南交通大学信息科学与技术学院，四川 成都 611756；2.西南交通大学系统可信性自动验证国家地方联合工程实验室，四川 成都 610031；3.西南交通大学唐山研究生院，河北 唐山 063000；4.北京和利时系统工程有限公司，北京 100176）

车站联锁系统是典型的安全苛求系统，保障着车站内的行车效率与安全，该系统内在的行为缺陷会对车站的日常运营造成巨大的损失[1].此外，车站联锁系统由联锁表驱动，验证数据的正确性对于该系统的安全运行也至关重要.

形式化方法是提高系统安全可靠性的一种有效方法，当系统的安全完整性等级达到SIL3级及以上时，IEC 61508[2]推荐使用该方法进行系统验证.形式化方法在车站联锁系统中也有应用，如有：文献[3]使用形式化建模工具UPPAAL建立了联锁系统的时间自动机模型，并对安全相关属性进行了验证；文献[4]建立了满足序列释放特性的车站网络联锁系统模型，基于有界模型检验及归纳推理方法，使用SMT（satisfiability modulo theories）求解器进行了验证.

以上研究中都忽略了对联锁数据进行确认，近年来，基于数据视角的系统安全性逐渐被重视，如文献[5]提出了一种用反例引导抽象精化范式的方法对车站联锁数据进行确认，文献[6]中使用ProB证明器确认了联锁数据.

综上所述，目前大多数联锁数据验证研究使用的都是模型检验方法，针对特定对象构建专门的模型.这些方法忽略了不同车站联锁数据确认的通用性.且形式化验证方法可分为模型检验与定理证明两种，后者弥补了模型检验方法只能处理有限状态空间的缺陷，Event-B语言是其中的典型代表，在该语言的支持平台RODIN中，模型检验与定理证明两种方法得到了有机结合[7].基于此，本文分析了联锁系统通用功能需求规范的形式化建模流程，使用Event-B语言描述，基于逐层精化策略建立了一个通用的联锁系统行为模型，并结合车站实例仿真、验收测试，提出了车站联锁系统行为验证与数据确认的形式化方法.

1 基于Event-B语言的形式化建模

Event-B是一种使用一阶、命题逻辑与集合论作为建模符号，描述离散系统的建模语言[1].Event-B模型由两部分组成[1,7]：场景文件（context）和机器文件（machine），其中场景文件定义了系统的静态属性，包括系统的基本组成对象以及运行时必须遵循的准则；机器文件定义了系统运行时的动态属性，由变量（variable）、不变式（invariant，运行过程中应满足的基本原则）、变体（variant）和事件（event）组成.

1.1 规范分析

建模之前需要进行规范分析.首先基于国标规范[8]，将通用联锁系统中的各类属性按照要求分为环境类、功能类和安全类3类，其中环境类属性被用来描述系统中建模的对象[1]，例如ENV_DG1：轨道区段分为道岔区段、无岔区段；功能属性描述系统对象应当具备的基本功能以及其执行条件，例如FUN_SIG1：信号机能正常显示建立进路时应当显示的灯色；安全类属性描述运行过程中保障安全苛求标准应具备的条件，例如SAF_SIG2：如果区段故障占用在信号保持阶段时发生，需要立即关闭信号机，但不能解锁进路.

事件是系统功能在基于安全类属性约束场景中的具体表现.在分析过程中，要得出各个功能对应的基本事件及其执行条件，分解出复杂功能的初始化状态、基本事件组成集合与执行顺序，并构建该功能的所有场景与安全性约束.以上过程中可使用STAMP（system-theoretic accident model and processes）等安全分析方法，并建议使用UML工具辅助构建可视化流程.且由于各属性与事件流程的对应规范文本内容往往数倍于系统需求本身，管理难度加大，可使用相应的需求管理工具（如RODIN平台中的ProR），以保持在修改过程中分析成果与后续模型的逻辑一致性.

1.2 初始模型

车站联锁系统主要是对进路流程进行控制，初始模型设计了进路的建立与解锁.对应场景文件中定义了进路的抽象集合ROUTE；在机器文件中包含两个事件：建立进路lock_route和解锁进路release_route，且定义集合lockedRoute来表示已经建立的进路，r表示进路序号.本文研究的建模过程中，使用了RODIN平台中的iUML-B插件，通过建立环境变量与事件流程UML图（如图1所示），直接生成场景文件与机器文件（如图2所示），提高建模过程的准确性及自动化程度.

图1 初始模型中事件的 UMLFig.1 UML diagram for event of initial model

图2 初始模型中的机器文件Fig.2 Machine file in initial model

1.3 精化策略

精化策略是指在模型建立过程中，将复杂的系统功能进行层次分解的建模策略.即首先建立初始模型，在初始模型得到实现且通过证明后，后续模型扩展的场景文件与精化的机器文件可以继承已被证明的定理、不变式，在此过程中逐步完善系统功能.本文的精化过程如表1所示.

表1 模型各层精化内容Tab.1 Refinement of the model

下文以第1层的Event-B精化模型为例，说明对象的引入与事件的添加过程.

1.3.1 第 1 层精化模型中的场景文件

定义轨道区段集合SECTION、列车的抽象集合TRAIN，EXTRA_TRACK、TRACK分别被定义为站外轨道区段、站内轨道区段，且EXTRA_TRACK⊆SECTION，TRACK⊆SECTION.站外轨道区段与站内轨道区段不能同时包含同一个轨道区段，即有如式（1）所示的公理定义.

用routeTrack表示每一条进路中含有的轨道区段.显然，各个轨道区段可以属于各个不同的进路，每一个进路区段也都可以包含有多条不同的轨道区段，因此routeTrack被定义为

设routeTrackNum为进路中各轨道区段的连接序号，属于ROUTE与轨道区段有序集合TRACK的全函数，其中在轨道区段的有序集合中，使用了不同编号以表示各个轨道区段，轨道区段与编号的关系为单射函数；进路中的轨道区段数量用routeTrack-Count表示，属于ROUTE和整数间的全函数.

用approachSection表示每条进路与其接近区段的映射关系：

1.3.2 第 1 层精化模型中的机器文件

由于加入了轨道区段，第1层精化模型中的机器文件新增了以下两个变量：变量lockedTrack记录锁闭轨道区段的进路，以便在解锁进路时对相应区段进行解锁，因此lockedTrack为TRACK与ROUTE之间的二元关系.进路的状态只有锁闭或解锁状态两类，故将lockedTrack定义为TRACK到ROUTE的部分函数关系；变量train_Pos用于记录站内站外所有列车的位置信息，因此有

本层模型中共有11个事件，以图3中的事件train_into_route为例说明如下：

图3 精化模型一中 train_into_route 事件Fig.3 Event of train_into_route in refined model 1

该事件用于实现车辆由站外区段驶入站内，精化扩展了初始模型中的事件release_route，事件release_route中对站内区段锁闭集合lockedRoute进行过定义.当进路r建立（grd1），且进路r的站外起始区段（比如第1离去区段）有车占用时（grd2），满足触发事件train_into_route执行的条件，车辆可以由这些区段驶入站内.该事件执行后，进路r释放（act1），且站外区段恢复空闲，同时车辆当前位置由站外区段更新为该进路的第1个站内区段，原站外区段恢复空闲（act2）.该事件在之后各层中还将得到精化，如增加车辆初始位置限制，区分列车与调车进路等.

在事件train_into_route执行后，将触发执行车辆前行事件train_move，并正常解锁（分段解锁）道岔、站内区段，直至车辆到达进路r的最末区段，则进路r执行结束.此时进路r虽被释放，但不满足重新建立的条件，如该进路最末区段仍被占用，进路r仍为非空闲状态.最终功能实现可见该模型精化后的最后一层机器文件M6[9-10].

2 系统属性验证

2.1 验证属性的Event-B描述

在场景文件中，集合或常量之间的属性定义为公理（axiom）.基于第1层精化模型中的场景文件，两条属性被定义成如下公理：

1）在任意进路，关系集合routeTrack对应的轨道区段，也会存在于routeTrackNum定义域所包含的轨道区段之中.其Event-B描述对应如下：

式中：符号⇒为蕴含操作符；dom(•)为定义域操作；▷为值域限制操作[7].

2）routeTrack与routeTrackNum不等价.在调车进路当中，如果无岔区段或到发线股道是最末端的轨道区段，则在联锁检查中不需要考虑该区段.routeTrack中定义的关系集合数量与routeTrackNum定义的关系集合数量有差异.即

式中：card(•)为笛卡尔积操作[7].

不变式表示系统的事件在执行过程中应遵守的属性，需保证其在模型执行的过程中始终为真.以精化模型1的机器文件为例，其中两条安全属性被表达成如下不变式：

1）任意两条敌对进路r1、r2不能同时被锁闭，如式（8）.

式中：conflictRoute为敌对进路集合.

2）一个轨道区段最多能被一条进路锁闭，如式（9）.

2.2 证明义务的证明

场景文件中的公理会产生证明义务，对其定义的合理性进行检查，机器文件中的不变式通过对相关事件生成证明义务的形式，实现对事件逻辑状态的检查.

以下是通过添加公理完善模型，使得证明义务得到证明通过的例子.

如对第4层模型中的rotate_switch_complete_2/inv1/INV证明义务进行证明时，加入公理

式中：routeSwitchPos为建立进路r中道岔sw应被锁闭的正确位置；dw为定位；fw为反位.

然后证明义务更新后未通过.分析过程如下：

在场景文件C4中，将routeSwitchPos定义为

式中：SWITCH为道岔的集合；道岔状态SWITCH_POS={dw,fw,null}，null表示道岔处于四开状态.

可 见routeSwitchPos(r→ sw)的 值 可 能 是 null，故以上目标不能得到证明.在C4文件中添加公理，如式（12）.

式中：r_otherSwitchPos为与routeSwitchPos关联的双动道岔另一端的状态.

之后将式（12）添加作为该证明义务的假设，该证明义务得以成立.

本次建立的模型各层文件共计生成了710条证明义务，通过完善模型中的形式表达，结合手动交互式证明策略，最后所有生成的证明义务都证明通过，统计情况如表2所示.

表2 模型证明义务的证明情况统计Tab.2 Proving statistics of model proof obligations 条

从需求文本到形式化模型的逻辑转换跨度较大，且系统规范也可能存在漏洞.所以，证明义务的证明过程是完善系统的设计规范、修正系统属性及形式化模型中潜在缺陷的重要手段[1].

3 数据确认及功能仿真与测试

3.1 基于公理验证的数据确认

以上各类证明义务全部通过，保证了联锁系统功能的可达性与安全性.若要保证实际车站联锁系统的可靠性还需要满足：1）公理的正确性验证.证明义务的证明过程默认公理的正确性，且将其作为证明条件；2）实际车站中联锁数据的安全性确认.联锁数据在人工编制过程中可能会发生错误.

文中设计了如图4所示的技术路线来进行公理验证及数据确认，即基于原模型1，建立一个仅有静态场景文件的新模型2，将所有场景文件进行实例化，即基于具体车站实例数据，对场景文件中的各常量进行赋值，且将除数据定义外的各属性公理设定为定理.该定理在系统中均可以自动生成相应的证明义务，通过证明来保证各公理的正确性.

图4 数据确认的技术方案Fig.4 Technical solution for data validation

本文实例选用的是图5所示的典型三股道车站，编制了对应的联锁表（只列出发车进路6条操作，另有接车进路6条未列出）如表3所示[9].

表3 举例车站联锁表Tab.3 Interlocking table of the example station

图5 举例车站平面布置Fig.5 Layout of an example railway station

证明过程中，C1场景文件中定理routeTrackNum∈ROUTE→(TRACKZ ) 对应的证明义务未被证明通过，其中ROUTE=1，2，···，12，TRACK={IG，IIG，IIIG，1/3DG，2/4DG}，routeTrackNum已被实例化为各条进路中各轨道区段的连接序号.分析得出原因为：此定理为多级函数关系，对应状态空间过大，超出了证明器的最大内存容量占用限制.本文设计了一种等价状态的证明方法如下：

1）定义 4 条公理：ROUTE1={1,2,3}，ROUTE2={4,5,6}，···，ROUTE4={10,11,12}，代替ROUTE=1,2,···,12，同时定义公理：

2）实例化routeTrackNum1，routeTrackNum2，···，routeTrackNum4 为进 路ROUTE1，ROUTE2，···，ROUTE4对应的区段，代替routeTrackNum的实例化数据，同时定义公理：

3）新定义 4 条定理

routeTrackNum1∈ROUTE1→(TRACKZ )，routeTrackNum2∈ROUTE2→(TRACKZ )，··，routeTrackNum4∈ROUTE4→(TRACKZ )，同时增加1条检查定理，检查routeTrackNum1，route-TrackNum2，···，routeTrackNum4 的定义域相互之间不出现重叠；

4）通过证明3）中5个较小状态空间的定理，并将证明通过的定理做为原定理证明中的前提条件，从而实现了对原定理的证明.

上述内容列在文件C1_1中，更改后验证结果如表4所示，可见在文件C1_1中，新增的5条定理和原定理共产生的6条证明义务全部可以证明通过.

表4 公理验证结果Tab.4 Verification of axioms 条

表4中的结果显示，由上述车站编制的联锁数据达到了模型2中所有定理的要求，从而确认了联锁数据，且证明了原模型中公理的正确性.在模型2中已证明所举例车站联锁数据满足原模型中所有公理约束.新建一个模型3，其场景文件从模型2扩展而来，其机器文件由原模型中继承而来.对模型3进行死锁及是否存在违反不变式的情况进行检验，结果显示，模型无死锁且不存在违反不变式的情况.

模型中的所有公理均是开发者根据对需求的分析后而形式化设定的，在分析的过程中可能会存在错误的逻辑描述，或各公理之间可能存在矛盾.数据的可靠性是计算机联锁系统功能实现的基础.本文研究中通过基于公理验证的数据确认方法，检查并确认了公理与数据的正确性.

3.2 验收测试与仿真实验

由于向不同领域的专家解释形式化模型的属性时存在困难，且非形式化研究人员很难确认模型事件的正确性，因此通过验收测试与仿真实验的方式，以说明验证后的模型所能实现的功能.

Cucumber for Event-B[11]允许在 Event-B 模型中建立 Gherkin 场景（Gherkin scenarios），可以被用来编码和执行验收测试.根据所建立模型3，建立一个应用Cucumber测试车站联锁进路场景的例子，如图6所示.其中：route_delay_L为列车进路解锁长延时事件，train_come_L为列车进站事件，train_move_L为列车在进路内行驶事件，train_leave_L为列车离去事件，switch_delay_2为双动道岔转动计时事件；train、train_Pos、train_type分别为列车、列车位置、列车类型，e_t为进站列车所接近的区段，L为列车类型集合.

图6 测试场景的步骤定义Fig.6 Plain step definitions oftest scenario

基于验证后的模型3，使用BMotionWeb插件工具制作一个典型实际车站的执行场景，可仿真不同变量与参数下的模型响应结果，用以对联锁表的数据进行功能确认.其中仿真场景中的灯色、道岔、列车的状态直接与模型中的变量相关联.图7中为演示联锁表中第10条即股道Ⅰ至发车进路S建立的场景，其中发车信号机XI显示为绿色灯光，在仿真执行过程中，车辆、色灯、道岔、进路与区段的状态变化都与设计规范相符.

图7 仿真测试举例Fig.7 Example of simulation testing

按照图5中车站对应的联锁表，在验收测试与可视化仿真环境中逐条建立和解锁进路，系统功能均可正常实现.上述过程对形式化模型进行了功能化的描述，同时还对模型的正确性做出检查，即通过仿真实验和验收测试，可以检测用户场景的集合，为系统行为的可达性提供了明确的说明，可进一步检查模型功能是否正确，与系统设计规范是否一致.

4 结 论

本文建立了基于规范分析得出通用系统形式化描述的过程，提出了一种对系统行为进行验证的方法.基于规范分析得出系统设计的环境属性、功能属性、安全属性与各事件流程，辅助使用UML工具建立初始模型的场景文件与机器文件，描述了各属性与事件流程；对本层的证明义务进行定理证明，基于精化策略，建立了后续各层模型.通过验证各层模型的系统属性，完善了通用功能模型.基于一个实例车站的联锁数据对系统中公理的正确性进行验证，并通过检验是否存在死锁与违反不变式的情况，进一步确认了模型的可靠性.

文中提出了基于通用形式化模型对系统数据进行确认的方法，即将联锁数据注入验证后的模型中，可以有效地进行联锁数据的验证；并通过功能仿真与验收测试技术，直观地展现模型的功能特性，可进一步验证系统行为，并同时对联锁数据的正确性进行了检验.

备注：本文相关的模型文件可在文献[10]的链接中下载.