基于形式化方法的道口控制系统规范建模与验证

王恪铭 ，王 峥

（1.西南交通大学信息科学与技术学院，四川 成都 611756；2.西南交通大学系统可信性自动验证国家地方联合工程实验室，四川 成都 610031）

道路与铁路的平面交汇形成了铁路道口，目前铁路道口数量多，且由于公路方向上的行人、车辆与列车通行存在矛盾的客观性，使得铁路道口隐藏着潜在的事故风险.近年来我国铁路道口平交改立交取得了成效，但数量依然庞大，仅正线上全国铁路的道口就有数千处（2013年底为7 519 处）[1].最新调查数据显示：欧盟28 国中有114 580 道口，平均每10 km的线路上就有5 处道口（2014年）[2]；2015年中道口事故占全部铁道事故的比例约为25.9%（469/1 808），道口事故造成的受伤人员比例为38.6%（264/684），死亡人员占比为30.7%（296/963）[3].可见，改善铁路道口的安全状况对于减少人员伤亡与财产损失，提高行车效率有着重要意义.

近年来道口安全研究引起了学者们的重视，影响道口安全的因素中，除了涉及行人、车辆、环境、道口特性等之外，还包含道口管理及其安全防护装置等因素[4].目前在相关道口控制系统的研究中，主要体现在对不同种类道口设备的可靠性分析[5]，增加传感器、视频分析等新道口装置的研究[6-7].

道口控制系统的研发是基于设计规范进行的，使用形式化方法可以检查系统规范，完善设计模型，且可大幅减少后续测试阶段发现的错误，显著提升工程质量与开发效率[8].当系统的安全完整性水平（safety integrity level，SIL）要求达到3 级及以上时，IEC61508 标准强烈建议使用形式化方法对系统进行验证[9].不同于具体功能算法测试后所得的指标比较[10]，形式化方法强调对系统设计中逻辑流程的验证[8].以上研究中，都忽略了道口规范可能存在缺陷及规范理解不全面对系统可靠性的影响；文献[5]使用了Petri 网、文献[6]使用了UPPAAL 时间自动机的形式化分析方法，但这些形式化方法缺少定理证明的能力，通过验证的模型不能直接用于生成系统的初始代码.

道口控制系统作为一类安全苛求系统，任何潜在的系统缺陷都可能会给道口运营安全带来巨大风险.据统计显示，系统中1/3 左右的祸根都是在需求分析阶段埋下的，但其纠正成本要占整体纠正费用的70%以上[11].因此，在设计研发阶段检查规范缺陷，对于保证系统功能的安全性、可靠性和完备性尤为重要.本文基于道口管理规范，分析得出道口管理的场景、功能、安全属性，建立事件逻辑流程，使用形式化方法及逐层精化策略建立了包含道口控制系统主要功能的系统原型，并基于Event-B 语言描述了系统验证特性，通过证明过程，检查了系统的安全与时间特性，完善了功能模型，通过系统设计原型的建立过程 ，揭示了目前管理规范中的不足，改进了系统设计并进行了验证确认，得出了对系统的功能规范进行建模与验证的形式化流程与方法.

1 功能规范分析

本文研究的是一个安装有自动防护装置的道口控制系统（有人值守），道口公路方向有可升降的栏门（或栏杆），系统示意如图1所示.道口来车方向设置有两个接近区段，列车驶向道口前在点A（接近点）与点C（逼近点）处发送预警信息.根据规范要求，A的位置应设置在接近通知时间不小于40 s 处（即列车从该处到达道口的时间，上限为90 s，按列车通过最大时速120 km/h 计算），C距离道口不小于列车的最大制动距离，并考虑适当的安全冗余.其中T1为列车从A至C的时间、T2为列车从C至道口的时间.

图1 铁路道口控制系统示意Fig.1 Schematic diagram of control system for railway level crossings

对道口控制系统的验证需要确认系统在通用标准及管理规范的约束下能否正确运行.首先需要深入解读道口规范的文本内容，析取各个功能事件的逻辑流程，分析得出系统的环境属性、功能属性、安全属性，构建好形式化描述的对象.

1.1 事件流程

基于平交铁路道口的管理规范，归纳得出道口控制系统的基本需求为：列车、道路上的行人与车辆可以分别安全地通过道口[12-13].具体的实现规范为：避免铁路上列车与道路上行人、车辆交通的冲突，即当列车即将通过前，行人与车辆应当出清，栏门及时关闭；列车驶离道口后，栏门及时开放，道路上的行人与车辆可以安全通过.析取出相应的流程如下：当系统检测到列车已到达接近点A，给出接近报警信号，同时信号灯转变成红灯并进行道口出清作业，之后发出栏门下降命令，道口关闭；当列车到达接近点C时，给出列车逼近报警信号，信号灯红闪；当列车驶离道口时，道口栏门升起，信号灯亮白灯，道口再次开放.流程如图2所示.

图2 道口控制系统中的事件流程Fig.2 Events flows of control system for railway level crossings

1.2 属性提取

分析道口设计规范，将其中的属性要求分为环境类、功能类和安全类共3 类.环境类属性（ENV）用于描述系统中建模对象的性质，功能属性（FUN）描述系统应当具备的基本功能，安全类属性（SAF）描述系统在运行过程中应具备的安全条件.

提取出环境类属性如下：

ENV1：道口门栏的状态包括升起中、开启、下降中、关闭.

ENV2：控制器对栏门的控制命令包括升起、下降.

ENV3：列车在道口附近的状态包括到达接近点A、到达逼近点C、离去.

ENV4：道口信号灯的状态包括红灯、红闪、白灯.

ENV5：控制器对信号灯的控制命令包括红灯亮、红灯闪、白灯亮.

结合事件的流程分析，功能类属性有：

FUN1：控制器通过升起、下降命令控制栏门的状态转换：开启→下降中→关闭→升起中→开启.

FUN2：列车到达接近点A、到达逼近点C及离开道口时，应给出相应信号.

FUN3：列车到达接近点A时，发出接近信号，道口信号灯转变成红灯并进行道口出清作业，之后栏门下降，道口关闭.

FUN4：列车到达逼近点C时，发出逼近信号，道口信号灯红闪，列车经过T2时间后将通过道口.

FUN5：当列车驶离道口时，道口栏门准备升起，延时一段时间后道口再次开放，信号灯亮白灯.

安全类属性有：

SAF1：当列车即将通过道口时，道口应该关闭.

SAF2：当列车离去时，道口才可重新开放.

2 基于Event-B 方法的形式化建模

Event-B 是一种描述离散系统的建模语言，使用一阶逻辑、命题逻辑与集合论作为建模符号，在其支持平台Rodin 中，模型检验与定理证明两种形式化方法得到了结合应用.Event-B 模型由两部分组成：场景文件（Context）和机器文件（Machine），其中场景文件定义了系统的静态属性，包括系统的基本组成对象以及运行时必须遵循的准则，场景文件由载体集合（Carrier Set，系统实际对象的抽象集合）、常量（Constant，系统中的固定对象）、公理（Axiom，系统中的普遍原则或先验的通用准则）组成[14-15].

机器文件定义了系统运行时的动态属性，由变量（Variable）、不变式（Invariant，系统动态运行过程中应满足的基本原则）、变体（Variant）和事件（Event）.事件包含事件参数（Event Parameter）、等价关系（Witness）、防卫条件（guard）、动作（action）等组成.事件定义了系统状态之间的迁移，模型执行时最先触发初始化事件（INITIALISATION）.

2.1 初始模型

在各事件的流程分析之后，可结合各类属性的约束，建立系统事件流程的UML 图，然后使用iUML-B插件，转化得到可扩充的验证模型原型，以提高建模过程的自动化程度.初始模型是对系统进行建模和验证的起点，底层模型会影响整个模型结构的简洁性及后续精化的便捷程度.道口控制系统的核心功能是根据列车接近情况对道口栏门进行控制，故初始模型仅设计了栏门的开启与关闭过程.因此场景文件中的数据类型有（文件定义如图3所示）：

门控命令（Controller_Order）集合：初始化（Null_C）、开启（GoUp）、关闭（GoDown）；

栏门状态（Gate_State）集合：初始化（Initia）、开启中（Opening）、已开启（Opened）、关闭中（Closing）、已关闭（Closed）；

初始模型的机器文件中包含4 个事件：栏门下降（GateGoDown）、栏门关闭（Gate_Close）、栏门打开（Gate_GoUp）、栏门开放（Gate_Open），且定义变量Gate_Information、Controller_Ctrl分别表示栏门、控制器的状态变化.如图4所示，建模中通过UML图的形式直观反映栏门的状态变迁，并用此图自动生成Event-B 语句.列出部分机器文件如图5所示.

图3 初始模型中的场景文件Fig.3 Context file in the initial model

图4 初始模型中的UML 图Fig.4 UML diagram in the initial model

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

2.2 精化策略

在初始模型得到实现且通过证明之后进行精化，逐步添加与完善模型的系统功能，形成新的场景文件与机器文件，继承已被证明的定理、不变式成果.精化策略降低了系统的建模难度，保证了各级底层模型的正确性.精化过程如表1所示，各层UML图、文件见参考文献[16].

表1 模型精化过程Tab.1 Refinement processes of the model

3 系统特性验证

3.1 系统验证特性的Event-B 描述

为体现系统运行过程中安全类属性的重要性，将该属性强制进行特性验证.以不变式（INV1～INV7）表达待验证的特性，即要让这些属性成立，则需保证对应的不变式在执行过程中始终保持为真.由于该系统的实时性要求非常高，因此同时对功能类属性中的时间性约束进行验证.定义一个计时事件Tick_Tock表示系统时钟，其它有时间特性的事件通过记录各运行阶段的系统当前时间，表达出时间特性要求[17].对各条验证特性进行Event-B描述，如图6所示.

图6 基于特性的不变式验证Fig.6 Property-based invariants verification

图6中，列车当前状态变量Train_Information的取值有：接近（Approach）、逼近（Closing）、离去（Exit）；Time为系统当前时间；Time_Approach_GateClosing为关闭道口时行人与车辆必需的出清时间；T_TrainApproach为列车发出接近信号的时刻；Time_Closing为门栏下降过程中的最大持续时间；T_ClosingStart为栏门下降命令下达时刻；T_TrainClose为列车发出逼近信号的时刻；Time_Closing_Coming为列车逼近至列车驶离道口过程中的最高持续时间T2；T_OpeningStart为开启命令下达时刻；Time_Opening为栏门开启过程中的最大持续时间.

INV1 体现了FUN3 的约束，以验证列车接近信号发出后，在必要的出清理时间之内，道口仍需要保持开放.

结合FUN2 与SAF1 的属性需求，得出INV2，以验证在列车接近信号发出后，经过一定时间的行驶，列车发出逼近信号.这段时间包括道口出清时间与门栏关闭时间，即T1.

基于FUN3 的属性需求，得出INV3，以验证控制器发出栏门下降指令后，栏门应在指定时间内关闭.

INV4 表达出了FUN4 的属性需求，以验证在列车逼近信号发出后，经过一定时间的行驶，列车通过道口.

基于SAF1 的属性需求，得出INV5，以验证当列车逼近道口时，道口应该关闭.

INV6 体现了SAF2 的属性需求，以约束在列车驶离道口之后，道口才可开放，即栏门升起之前，需要判断道口状态，并同时得到栏门升起命令.

基于FUN5 的属性需求，得出INV7，以验证控制器发出栏门开启指令后，栏门应在指定时间内开放.

规范中的环境类属性全部定义在模型的Context文件中，功能类属性在Machine 文件中描述成了各个事件，结合以上不变式对应的安全属性与时间特性要求，设计需求规范在模型中已经得到了全部覆盖.

3.2 证明义务的证明

在Rodin 中，不变式对事件会产生相应的证明义务（proof obligations）.由于规范文本到逻辑事件的跨度非常大，在对系统进行形式化描述时，难免会遗漏某些关键的约束信息.在对证明义务进行证明时，这些建模缺陷会被显现出来.证明义务的交互式修改证明过程对于开发者深入理解规范，完善规范属性与模型至关重要.举例如下：

（1）系统时钟（Tick_Tock）是一个计数事件，需要添加有时间特性约束的响应，作为时钟计数的防卫条件，如图7中的guard1、guard2，以加强事件防卫条件的完备性，从而确保INV1、INV4 产生的证明义务得以通过.

图7 添加事件的防卫条件Fig.7 Additional guards of event

（2）在列车逼近（Train_Close）事件中，需要增加防卫条件：Gate_In formation=Closed，以保证INV6对应产生的证明义务得以通过.

（3）在栏门开放（Gate_Open）事件中，需要增加防卫条件：Train_In formation=Exit.虽然栏门打开（Gate_GoUp）事件中判断了列车状态（Train_Inforamtion），但由于在栏门开放（Gate_Open）事件中，栏门状态Gate_Information要转换成Opened，为了不与INV1 产生的证明义务相冲突，此处仍需要增加对列车状态的检查，以限定事件的状态空间.

证明义务统计如图8所示，图中，C1～C4 表示模型中的各层场景文件，M1_Control_Gate～M4_Control_Gate_Train_Signalling_Time 表示模型中的各层机器文件.以第4 层的机器文件为例，共计生成57 条证明义务，其中自动证明通过52 条义务，结合人工修改完善模型证明5 条，所有证明义务全部证明通过.

图8 精化过程中的证明义务统计Fig.8 Statistics of proof obligation in the refinement processes

4 道口控制系统的完善

在列车逼近（Train_Close）事件中，假设了列车可以获取道口栏门状态.而目前的道口控制系统没有这一功能，接近列车司机需要与道口管理员进行语音通话确认，无法做到实时性，且响应过程较长，存在列车未知栏门状态就已闯入道口的隐患.另外，根据研究过程中的事故调研分析，栏门关闭并不能等价于道口出清，现实中仍存在人车滞留在道口内且栏门已经闭关的可能性.

因此，安全属性SAF1 不能满足需求中列车安全通过道口的要求，也不能保证规范中的道口出清的要求，需要将其修改为：当列车即将通过道口时，道口应该关闭且道口出清；否则列车应采取制动措施.可见图2流程中缺少对道口异常状态的处理，对应管理规范中也缺少对异常状态处理流程的明确界定，导致系统缺乏稳健性（robustness）.在第四层模型中增加了对道口状态的监督及异常状态处理，流程如图9所示.

图9 道口异常处理流程Fig.9 Exception-handling process of the railway level crossings

除添加道口状态检查、信息发送、道口状态判断、列车制动等事件外，增加了列车接近（Train_Approach）、列车逼近（Train_Close）事件的防卫条件，添加了验证特性INV8，以约束当道口状况异常时，应发出警告信号，提示正在接近的列车进行制动，如图10所示.图中，变量道口状态Crossing_Infor的取值有：正常（Normal）、异常（Abnormal）；变量列车命令TrainOrder的取值有：制动（Normal）、继续前行（KeepGoing）.

图10 新增对应的异常处理流程不变式验证Fig.10 Additional invariants verification of exceptionhandling process

之后对模型不变式的冲突性与死锁进行了检验，全部通过验证，该结果进一步确认了系统原型的正确性.可见，虽然在证明过程可以修正并减少需求分析与建模过程中的缺陷，但如果需求分析过程不完善，证明通过的模型也有可能包含缺陷.因此系统设计人员需要通过分析、建模与验证过程，加深对系统设计需求及规范的理解，以提高模型的完备性与可靠性.本文相关的所有文件与模型可见参考文献[16].

5 结 论

系统功能规范是系统设计实现的依据，任何潜在的规范缺陷或解读错误都可能会给系统运营安全带来巨大风险.本文以道口管理规范为例，基于Event-B方法建立了道口控制系统的设计原型，并进行了形式化验证，得出主要结论如下：

（1）基于管理规范对系统属性及事件流程的分类分析方法、通过UML 图自动生成验证模型文件的技术及精化建模的策略，有助于清晰、准确地描述系统的特性，提高验证模型的层次性；

（2）通过证明义务的交互式修改证明过程，可以帮助开发者深入理解规范，发现规范文本自身以及跨度到逻辑表达过程中，造成的假设、约束信息遗漏或错误，从而可以修改规范与建模缺陷，完善规范属性在验证模型的表达；

（3）研究得出目前规范中存在列车驶入道口时不能确保系统安全状态的缺陷.形式化建模与验证方法有助于发现并纠正系统规范中潜在的设计漏洞，减少因规范理解不当造成的建模缺陷，验证后的模型可以作为系统设计原型，成为编码阶段工作的依据，且后续基于设计原型使用代码生成技术可以提高编码阶段的自动化程度，以减少测试阶段的成本投入.