第一作者:刘宏杰(1983—),男,河北石家庄人,博士生.研究方向为列控系统设计、集成和安全保证.email:hjliu2@bjtu.edu.cn.
现代平交道口控制系统多为由计算机组成的基于通信的控制系统,该类型系统中的危险致因大多源于系统组件间的复杂交互场景未得到充分辨识和控制。为了避免平交道口事故的发生,提出一套基于系统理论过程分析(STPA)的铁路信号系统安全分析方法。借助对传统STPA方法的改进及XSTAMPP软件,以平交道口控制系统为案例进行了安全分析。研究结果实现了安全需求可根据危险分析结果自动生成,解决了传统STPA过程过于依赖人工的问题;分析得到的平交道口控制系统安全需求被自动转化为线性时序逻辑(LTL)语言描述的形式化规范,避免了传统STPA分析结果用自然语言描述可能存在的歧义性,为基于模型的系统设计、测试和验证提供参考。
Modern level crossing control systems are mostly computer-based and communication-based control systems. The causal factors in this type of system are mostly due to the fact that the complex interaction scenarios between system components have not been fully identified and controlled. In order to avoid the occurrence of level crossing accidents, this paper proposes a set of safety analysis methods for railway signal systems based on System Theory Process Analysis (STPA). With the improvement of the traditional STPA and the XSTAMPP, this paper takes the level crossing control system as a case for safety analysis. The results achieve the automatic generation of safety requirements based on the hazards analysis results and solved the problem that the traditional STPA process is too dependent on labor. Meanwhile, the safety requirements of the level crossing control system are automatically converted into a formal specification of the Linear Temporal Logic (LTL) language description, which avoids the possible ambiguity in the natural language description of the traditional STPA analysis results. It provides references for a model-based system design, testing and verification.
铁路的建设发展进入一个全新的阶段, 无论是列车的速度、密度还是列车的载重都比以前有了极大的提高.与此同时, 公路运输量也在不断提高, 道路交通工具数量大幅增长.这样的交通现状加上有待提高的人口素质, 导致平交道口存在很大的安全隐患[1].平交道口无论是对于铁路运输还是道路运输, 都是一个相对薄弱的环节.平交道口一旦发生事故, 其结果往往是车毁人亡, 不仅中断铁路运输, 阻塞道路通行, 严重影响着交通系统的正常运行, 还会造成重大经济损失, 甚至带来恶劣的政治影响[2].
国内外有很多关于平交道口安全的研究.国外的研究比较注重人为因素, 如列车司机和汽车司机, 文献[3]通过系统方法和心理方法对澳大利亚一起严重的平交道口事故进行分析, 分析出导致汽车司机没能注意到平交道口警告的可能原因.我国对平交道口控制系统也做了大量研究, 文献[4]根据近几年轨道交通安全事故的统计, 运用因果连锁理论对系统设计安全风险因素进行研究, 并找出控制系统设计安全风险的关键方法.文献[5]改进了传统的轨迹交叉理论, 研究结果表明环境因素在事故发生过程的重要地位.文献[1]运用事故树ATA(Accident Tree Analysis)分析法对黑龙江“ 1· 28” 重大铁路道口事故进行分析, 得出道口工作人员因素、机动车驾驶员因素、铁路防护系统因素是三大事故致因因素.
通过研究大量文献发现, 传统分析法从事故或者故障出发, 对于平交道口系统, 寻找其发生故障的组件, 从而找出事故的原因.这一过程中, 传统方法往往忽略了平交道口系统中组件交互带来的非安全控制行为, 同时, 从事故或者故障出发的思路, 可以解决已经暴露出的问题, 却无法发现潜在的其他危险.因此, 本文作者提出基于STPA的平交道口系统安全分析方法, 该方法可以识别系统中的非安全控制行为和潜在危险, 获得安全需求, 指导系统的设计, 从而使设计人员在事故发生前发现问题.
STAMP(System-Theoretic Accident Model and Processes)[6]是基于安全工程系统和控制理论的事故模型, 将安全性视为控制问题而不是单一组件问题.STAMP将系统视为控制回路相互作用, 并且由系统组件的不充分控制或在与系统环境(例如人类、组织或其他物理系统组件)中的其他组件的交互过程中, 由外部干扰引起的事故.STPA是在STAMP事故致因模型基础上提出的一种具体危险分析方法.STPA通过一系列的步骤找出导致系统危险出现问题的根本原因, 具体过程如图1所示.
STPA作为一种基于系统理论事故模型的危险分析方法, 已经成功应用于多种安全苛求系统的分析, 设计航空航天、国防工业、交通运输、化学工业、医药生成等多种领域[7].
本文所选特定无人看守平交道口如图2所示.该平交道口主要由以下部分组成:4个道路警报灯和2个护栏, 设置在平交道口外部轨道旁的信号机, 用以指示列车能否进入平交道口区域, 5类传感器, 分别为列车接近道口传感器、列车出清道口传感器、护栏位置传感器、信号灯状态传感器和警报灯状态传感器, 1个控制器单元, 控制其他各个部分动作, 电源等.
平交道口系统的工作流程为:1)当有列车接近平交道口时, 列车接近道口传感器检测到有列车接近, 传感器将该接近信息发送给控制单元.2)控制单元向道路警报灯和护栏发出控制命令, 道路警报灯闪烁, 护栏延时8 s后落下.当护栏位置处于完全落下状态时, 护栏位置传感器向控制单元反馈护栏已完全落下信息.3)控制单元给轨道旁信号机发送绿灯命令, 将信号灯从红色转换为绿色.(如果信号机未收到控制单元的绿灯命令, 信号灯需保持红色.如果列车接近, 但信号灯仍然为红色, 列车必须停在信号机前.)当列车到达平交道口并且被列车出清传感器检测到后, 列车出清传感器向控制单元反馈列车已出清信息.4)控制单元向信号机发送红灯命令, 将信号灯置为红色, 同时向道路警报灯发送熄灭命令, 向护栏发送抬升命令.
为了获取平交道口系统安全需求, 通过XSTAMPP[8]软件工具记录STPA安全分析方法的结果, 并生成STPA结果的正式规范.
根据STPA分析步骤可知, 首先分析系统层危险, 并确定相应系统层安全约束, 再层层深入.以下是对平交道口系统层分析结果:
1)平交道口系统概述:有列车接近时, 警报灯响起, 护栏落下; 列车通过后, 警报灯关闭, 护栏抬升.2)平交道口系统目标:防止列车通过平交道口时与道路交通工具或者行人相撞, 确保行车安全.3)平交道口系统会导致系统等级的事故:列车在平交道口内与行人或人驾驶的机动/非机动车辆相撞.能够导致系统等级事故的系统等级危险, 如H1:列车进入平交道口时护栏没有处于落下状态; H2:列车进入平交道口时护栏突然抬升.根据相关危险, 得出系统等级的相应安全约束, SC1:列车进入平交道口时应确保护栏处于落下状态; SC2:在列车完全出清平交道口前, 护栏应保持完全落下状态.
对平交道口系统层分析之后, 建立系统分层控制结构.根据平交道口系统工作流程及相关组件, 绘制了如图3的平交道口系统控制结构图.
图3展示了系统中不同组件的交互:传感器Strike in/Strike out分别检测列车进入与出清平交道口, 并将列车进/出平交道口信息传递给控制系统(Controller Unit).Controller Unit根据传感器的信息输入, 分别对信号机(Signals)、警报灯(Flashing lights)和护栏(Barriers)的各自执行器发出控制命令, 相应的执行器(Actuator)执行控制单元所要求的控制行为, 同时控制单元从相应传感器(Sensors)获得相关反馈信息, 了解控制对象执行控制命令后的状态是否达到了所需要的状态, 如果没有, 则继续发送相应控制命令.从而形成一个闭环回路:根据获得的反馈信息, 再调整相应控制行为.
本文作者对4大类控制行为:1)没有提供控制导致危险, 2)提供控制导致危险, 3)在错误的时间提供控制或不正确的控制顺序导致危险, 4)过早停止控制行为或控制行为持续太久导致危险逐一进行分析评估.如果一个控制行为是危险的, 将分配相应系统等级的危险, 否则, 认为它是没有危险的.基于此, 可以识别出14个非安全控制行为:4个控制信号灯的非安全控制行为, 4个控制警报灯的非安全控制行为和6个控制护栏的非安全控制行为.表1例举了护栏落下的3个非安全控制行为.
通过人工的方式为每一个非安全控制行为制定相应安全约束, 针对表1护栏的非安全控制行为, 表2给出了相应的安全约束.
为了细化非安全控制行为, 建立了带有过程模型的平交道口系统控制结构, 如图4所示.
平交道口系统是一个拥有3个过程模型变量的过程模型, 每一个过程模型的状态都会对平交道口系统的控制行为的安全性造成影响.1)过程模型变量1道路警报灯:拥有2个状态, 分别为闪烁和熄灭; 2)过程模型变量2护栏:拥有3个状态, 分别为完全升起、完全落下和中间状态; 3)过程模型变量3信号灯:拥有3个状态, 分别为红灯、绿灯和熄灭状态.
本文分析评估某一控制行为在3个过程模型不同状态组合下是否危险.对于每一个控制行为, 分析对于提供/不提供该控制行为时, 该控制行为与其他所有控制行为的组合总数理论上为2× 3× 3=18个组合.为了自动生成组合, 并且减少组合的数量, 使用XSTAMPP软件平台中的XSTPA插件, 通过组合测试算法, 从而能够自动生成情境表(context table), 同时能够识别各个过程模型变量间的最小组合数量, 大大降低了工作量.为了减小XSTPA中的过程模型变量组合数量, 选择Pairwise算法.Pairwise算法是基于数学统计和对传统的正交分析法进行优化后得到的产物, 算法中两个过程模型变量值的组合至少能被一个组合集覆盖, 因此能够大大减少组合的数量, 从而提高测试效率.算法采用两个状态最多的变量来减少组合的数量.在平交道口系统中, 状态最多的两个过程模型变量分别为护栏(3个状态)和信号灯(3个状态), 因此, 过程模型变量组合数量减少到3× 3=9个.接下来, 通过软件平台为每一个控制行为生成拥有9个状态组合的情境表, 如表3所示.
根据表3, 软件能够自动细化非安全控制行为表, 同时自动给出非安全控制行为的相应细化安全约束, 从而获得细化的安全需求.由于软件的情景表中对于提供控制行为的时间只有“ 任何时候” 、“ 过早” 和“ 过晚” 3种情况可供勾选, 至于什么是“ 过早” 和“ 过晚” , 软件无法根据具体的系统进行具体的表示, 需要在自动生成的基础上对具体时间进行人工修改, 用具体含义代替“ 过晚” .在本平交道口系统的RUCA1.1中的“ 过晚” 表示“ 警报灯闪烁大于8 s后, 护栏才开始落下” , RUCA1.2中的“ 过晚” 表示:“ 护栏在防护信号机开放绿灯之后才落下” , 如表4所示.
对于上述步骤识别出的每一个非安全控制行为, 根据平交道口系统的控制回路, 从两方面逐一分析其致因场景.
1)从反馈路径分析, 如图5所示, 传感器从被动对象获取数据有误, 或者传感器获得了正确的数据, 但在反馈给控制器过程中出现偏差、延时等, 从而导致控制器向执行器输出了不安全的控制行为命令.
2)从控制路径分析, 如图6所示, 控制器从传感器获取了正确的反馈数据, 从而输出了安全的控制行
为命令, 但是命令没有被执行器按要求执行, 从而导致最终的不安全行为.
例如, 对于非安全控制行为UCA1.2:有列车接近时, 护栏在防护信号机显示绿灯后还没有完全落下, 从反馈路径分析它的致因场景CS.1:护栏位置传感器对于护栏的位置判断出错; 从控制路径分析它的致因场景CS.2:控制器向护栏发出了正确的下落命令, 但是由于某些原因护栏没能下落或完全下落.
由于篇幅的限制, 表5例举了在有列车接近时, 护栏在防护信号机显示绿灯后还没有完全落下时的2个致因场景及相应的安全需求.其中采用UCA1.2和RUCA1.2.
基于STPA方法, 获取了平交道口防护系统的细化安全约束和与其对应的安全需求, 但其结果为自然语言, 对于不同人员, 解读上可能存在歧义.同时, 自然语言的结果无法被其他工具所识别, 影响利用STPA分析的结果, 通过相关工具对建立的平交道口模型进行模型安全性验证.
LTL[9]线性时序逻辑是一种形式化符号, 其主要作用是进行计算的逻辑推理.LTL通过时间的顺序来描述计算的路径.在LTL中主要包含X(neXt, 表示“ 下一状态” )、G(Globally, 表示“ 所有未来状态” )、F(Future, 表示“ 某个或某些未来状态” )、U(Until, 表示“ 直到” )、R(Release, 表示“ 释放” )和W(Weak— until, 表示“ 弱— 直到” )6个时序连接词.LTL通过这些连接词将时间建模成一系列“ 状态” 的序列, 同时可以向未来延伸, 这个状态路径简称“ 路径” .LTL公式一般用来描述并发现程序的性质, 通过检测程序是否具有由LTL公式描述的性质可以验证程序的解决方案是否符合需求[10].
同时, 为了使LTL数学表达式能够被Simulink等后续模型分析工具识别, 须将LTL数学表达式中的时态连接词做相应替换, 如表6所示.
1)对于细化的安全需求:当护栏处于完全抬起状态, 警报灯处于熄灭状态时, 不能提供将信号灯置为绿灯命令的LTL表达式为
[]((Barriers==up& & Flashing lights==extinguished)-> (!(controlaction==settogreen)));
该表达式意为当护栏处于完全抬起状态且警报灯处于熄灭状态时, 禁止出现将信号灯置为绿灯的控制行为, 与需求一致.
2)对于细化的安全需求:当信号灯是绿灯并且警报灯是熄灭时, 护栏必须在防护信号机开放绿灯之前完全落下的LTL表达式为
[]((Signal==green& & Flashing lights==extinguished) -> (!(Signal==green& & Flashinglights==extinguished)∪ (controlaction==drop)));
该表达式意为当信号灯状态绿灯, 且警报灯处于熄灭状态时, 为了保证护栏在规定时间落下, 采取直到输出落下动作, 并处于完全落下状态后, 才允许出现信号灯为绿灯且警报灯熄灭的状态的措施, 这是一个正确且满足安全需求的LTL表达式.
利用XSTAMPP软件平台, 根据最终得到的安全需求, 自动生成LTL公式规范, 可以利用对所得安全需求自动生成的LTL公式作为Simulink等工具的输入, 进行进一步的安全测试模型的验证分析.
利用基于STAP方法的安全分析法, 通过分析具体的平交道口系统, 找出了分析的平交道口的安全需求.
1)从系统层面, 找出了平交道口系统等级的危险, 同时确定了相应的系统等级安全约束.2)建立了平交道口系统的分层控制结构, 分析其不安全控制行为, 并对不安全行为提出安全约束.3)建立了带有过程模型的平交道口系统控制结构, 从而对于不安全控制行为进行了细化, 同时细化了安全约束, 提出了相应的安全需求.4)对非安全控制行为进行致因场景分析, 找出导致非安全控制行为在整个控制回路中可能发生的所有具体原因.从而保证提出的安全需求对于开发设计人员来说切实可行.5)将得到按安全需求, 通过XSTAMPP将所得到的安全需求进行形式化转换, 实现了将自然语言的安全需求转换为LTL正式规范, 使STPA安全分析的结果能够被其他工具所识别, 为进一步利用工具分析打下良好的基础.
在进一步研究中, 将利用得到的形式化安全需求作为Simulink的输入, 进行安全测试模型的验证分析.
The authors have declared that no competing interests exist.
[1] |
|
[2] |
|
[3] |
|
[4] |
|
[5] |
|
[6] |
|
[7] |
|
[8] |
|
[9] |
|
[10] |
|