仝占方，周刚
中车株洲电力机车有限公司，湖南株洲421001
摘要：简要介绍了轨道交通车门系统的特点，通过对现有车门系统反馈的特点，提出用TLA+形式化方法验证软件功能需求可靠性的方案，最终在实际项目应用中进行应用验证，实际运行效果良好，达到了预期目标，为提高产品软件质量，具有很好的推广价值。
关键词：形式化方法；车门系统；轨道交通
0 引言
中国轨道交通领域在向电气时代和数字化智能化时代迈进的进程中，控制系统软件扮演者越来越重要的角色。作为车辆的入口，车门系统起着非常重要的作用，尤其针对地铁车辆客流量大，部分乘客站立在地铁车辆门口出行，如何进行安全可靠的开关门是非常关键的内容。
对车门系统的安全性要求，轨道交通一般采用EN 50129 / EN 50128/EN50126 标准要求采用SIL2等级[1]，对每个项目进行系统认证周期成本较高，同时经过SIL2认证的软件也可能出行严重故障。在一些要求高可靠性的关键应用上，采用形式化开发方法可以保证软件系统的可靠性。本文主要介绍形式化方法验证地铁车门软件需求的安全性可靠性。
1 需求分析
轨道车辆的车门系统是乘客上下车的入口，以3节编组，每节车厢一般装有 6 套门为例，每节车6个门控器， 2 套主电子门控器（MDCU）， 4 套从电子门控器（LDCU）， 2 套主电子门控器是连接到 MVB 车辆总线上的， 4 套 从电子门控器是与 2 个主电子门控器一起连接到 CAN 局部总线，为了区分车门位置，对每个门进行编码（1到6），如图1。单个车门的工作原理为门控系统收到指令后驱动电机进行开关门操作，设置了车门锁到位开关、关到位开关、手动解锁开关、隔离开关等进行车门状态感知，如图2所示。
.png)
车门系统在整车表现为一个分布式系统，具体行为为:在零速信号有效时，在I端司机室操作车门开左侧门，主门控器将收到的指令分别在3节车的内部传递，最终红色线侧车门全部打开；在I端司机室操作开右侧门，绿色侧全部开门；当零速信号无效时，车门所有车门自动关闭，开门信号不执行开门动作。
安全性要求：（1）车门系统在关闭过程中遇到障碍物需要弹开；（2）开门侧左右不能错误；（3）列车运行过程中不能开门。
2 形式化方法在车门系统中应用
传统的软件测试只能表明测试不存在错误，不能证明软件中没有错误。形式化方法是将程序抽象成数学公式，指采用严格的数学方法，推理证明或伪证该公式。形式化方法才能从根本上保证系统安全可靠。使用形式化规约语言来精确定义软件系统，再用形式化方法验证软件系统正确性两部分内容。
2.1形式化方法工具介绍
形式化工具有多种，对于分布式系统来说需要考虑给出先后的指令的时序顺序、逻辑关系等，最好是采用行为时序逻辑TLA+来进行描述。TLA+ 是由图灵奖作者 Leslie Lamport 于 20世纪 90 年代提出的一种基于行为逻辑与线性时态逻辑的新逻辑方法[2]。它采用一阶逻辑和集合论来描述逻辑同时表达程序与相应属性要求，具有很强的描述和验证能力。
2.2 车门系统描述
车门系统的模型描述采用通讯状态机CFSM来进行，一个通信有限状态自动机由一组有限状态自动机的集合M和一组通道C组成。
.png)
对M中的每个自动机mi，是确定有限状态机，这里表示每个门的自动机；
C中的每个通道Cij表示mi到mj的通信通道。它是一个先进先出的队列，mj从队列的头读出数据作为输入，mi把要向mj输出数据送到队列的尾部，这里表示MVB通道及CAN通道；为了叙述方便，这里讨论单个门的情况。
单个车门的门控器内部功能为如图所示，定义了7个门状态：
A1：自检，车门将关闭以启动一个初始化过程，直到车门
.png)
达到关闭位置为止。
A2：锁到位状态，表示门机械锁死；
A3：开门中状态，表示从完全关门位向开门位移动的状态；
A4：开到位状态，表示完全开门后的停止状态；
A5：障碍物状态，表示门轨迹上有障碍物，无法正常
开关门的状态。
A6：关门中状态，表示从完全开门位向关门位移动的状态；
A7：停止状态，车门无法打开或关闭
确定好状态后，再确定好状态转换函数的入口条件和退出条件，最后用形式化语言将模型描述出来，TLA+采用一阶逻辑和集合论来作为描述方法，描述状态转换过程。
.png)
3.3形式化验证
形式化验证指的是验证已有的程序是否满足形式化描述的定义。采用数学方法去论证一个系统，可以硬件系统，也可以是软件系统，形式验证方法分为等价性验证、模型检验和定理证明等方法。
TLA+ toolbox提供了模型检验和定理证明两个方法，这里主要验证模型中是否存在违背安全的状态，于是采用模型检测方法检测模型正确性，具体为TLC工具，设置好安全属性为不变式，运行模型检测，保证所有状态下的安全性正常，如果不正常会给出反例。
.png)
需要说明的是，模型检查指出的范例，并不是第一次模型检查就正常，此过程中发现错误表明存在考虑不足的情况，需要反复多次迭代最终到达无错误的目标，形式化方法体现了设计即正确哲学思想。
3.安全功能建议
形式化方法可以发现常规方法不容易发现的问题，针对车门系统的安全性，提出以下几个方面建议。
（1）车门安全继电器状态
正常情况下车门安全继电器，应该在非零速处于断开状态，切断门驱动电机的电源，保证故障不会进一步升级，需要加强对安全继电器产品故障失效模式进行审查。
（2）车门的位置编码
对于车门系统来说运行过程中有左右侧之分，开门侧错误会引起安全事件，在设计门位置编码时候需要考虑开门侧，在车门上电自检阶段判断门位置编码是否错误，如有错误及时报出故障信息。
（3）车门关闭状态保持
车门具有手动操作功能，同时外部机械部分故障时，车门控制器需要保持故障安全导向，车辆运行过程中当车门离开锁位置开关且没有手动解锁情况下，需要立即关闭车门，必要时需要增加硬件辅助装置如动车组车门的侧立集成装置进行状态保持。
（4）安全互锁回路功能验证
整车调试的时候需要严格验证安全互锁回路功能，确保功能完整实现。
（5）网络协议的安全性
车辆开关门一般会选择网络优先方式，当网络信号和硬线信号不一致时候，需要记录相关故障信息，同时TCMS和各系统之间数据安全性需要验证，需要采用IEC61375-2-3中STDv2的安全要求。
4 结束语
形式化方法是安全攸关系统是重要的方法，经过各行业验证的高可靠性方法。通过形式化方法在车门系统中的应用，通过形式化描述，需求分析的质量大大提高，很多自然语言描述无法避免的缺陷在需求分析阶段就会被发现，并得到解决，从而降低后期开发和维护的成本，并提升软件的质量和可靠性。形式化验证可以根据模型的遍历所有可能性验证软件的安全性，同时发现常规方法不容易发现的车门软件缺陷，提出了相关建议。经过实际项目运用，效果良好，有力促进了公司城轨车门系统技术水平的提升，为公司车辆可靠运行提供了技术方案。
[1]张伟、陆驰宇 城市轨道交通车辆车门控软件安全完整性技市应用研究[J] 城市轨道交通研究 2013
[2]Leslie Lamport.SpecfyingSystems[M].http://lamport.azurewebsites.net/tla/book.htm