车车通信列控系统资源管理单元安全性分析

刘振宇，李 晶

（北京城建设计发展集团股份有限公司，北京 100045）

随着轨道交通行业的快速发展，传统列控系统暴露出一系列弊端，例如客运压力大、行车效率低、轨旁设备繁多等[1]。众多科研机构和企业积极进行新一代列控系统的开发，对列控系统的结构与功能进行进一步优化。

通过分析国外列控的发展趋势，结合中国列控技术的现状，北京交通大学开展了下一代列控系统技术方案研究[2]，提出基于车车通信的下一代列车运行控制系统[3]。目前基于车车通信的列控系统尚处于研究开发阶段，有必要对列控系统进行安全分析和风险评估，以确定在具体的应用场景中是否存在不安全因素。由于列控系统是非常复杂的，相较于其他安全分析方法，STPA (system theoretic process analysis，系统理论过程分析方法)能够充分考虑组件间的交互对列控系统安全的影响[4]，现使用系统理论过程分析方法分析列控系统的安全性。

本文重点对基于车车通信列控系统的 RMU(resource management unit，资源管理单元)进行安全性分析。以RMU发送TSR (temporary speed restriction，临时限速)场景为例，构建了列控系统的分层控制结构。根据列控系统的控制结构，判断该过程中危险控制行为并找到控制缺陷。利用控制缺陷得到相关SDR(security design requirements，安全性设计需求)。通过UPPAAL工具搭建TSR发送场景下的时间自动机网络模型，最后把SDR翻译为UPPAAL可识别的语言，以此来验证SDR的合理性。

1 基于车车通信的下一代列控系统介绍

基于车车通信的列控系统的系统结构可以分为 3层，分别为：运营控制层、车载控制层以及轨旁控制层，如图1所示。运营控制层主要由DCD (dynamic capacity decision，动态运能决策系统)和RMU构成。动态运能决策系统的功能是发送行车计划和调度命令。RMU主要负责在线列车管理与临时限速下发。车载控制层是整个列控系统的核心，主要由VCM (vital computer management，车载列车管理)和 VCI (vital computer interlocking，车载联锁)组成，具有完成移动授权计算、列车超速防护和进路排列等功能；轨旁控制层主要由OC (object controller，对象控制单元)等设备组成，具有信号机、转辙机等轨旁设备的控制和表示功能。

图1 基于车车通信列控系统的系统结构Figure 1 Structure of train control system based on vehicle-vehicle communications

RMU作为基于车车通信列控系统的核心地面设备，主要功能有：①在线列车管理，包括列车的注册与注销；②下发临时限速，同时接收列车运行状态信息汇报给DCD；③OC状态监督；④存储与转发列车的各种状态数据；⑤向列车发送管辖范围内列车位置，辅助车载实现前车识别和联锁功能。RMU外部设备交互图如图2所示，由于RMU对外交互设备繁多，交互过程中极有可能出现故障导致事故发生。对其进行安全分析和风险评估，以确定特定应用场景中的不安全因素，同时制定相关的安全约束是十分必要的。

图2 RMU对外设备交互图Figure 2 Diagram of external device interaction

2 研究方法介绍

2.1 STPA模型概述

STAMP模型是基于系统理论的事故分析模型，它重点关注系统组件间的交互及控制机制[5]。STAMP理论采用多层次的系统结构来表征系统内部单元之间的信息流，主要是控制命令和反馈结果的。系统安全的重点由防止组件失效转换为实施行为的安全约束，将安全问题转换为控制问题而不是可靠性问题[6]。STAMP已经成功应用于多种安全苛求系统的分析，涉及航空航天、国防工业、交通运输、化学工业和医药生成等多个领域[7]。

STPA基于STAMP理论构建的系统控制图进行分析，从外部输入开始针对控制回路的每一个环节进行分析，辨识致因因素。STPA以系统级危险作为输入，主要通过以下4个步骤辨识导致危险出现的根本原因[8]：

第1步：针对系统级危险，确立安全约束；

第2步：搭建多层次的系统结构。搭建多层次的系统结构，可以研究系统内部各层次信息流动的过程，从交互过程中寻找系统中存在的不安全因素。

第3步：寻找导致系统危险的原因。针对所建立的分层控制结构图中的控制行为，辨识以下不安全控制行为：①系统发出的未定义安全要求的控制或不符合安全约束控制；②提供不安全的控制从而导致危险；③控制行为本身是安全的但时序不正确；④系统进行控制的时间不合要求。

第4步：分辨控制缺陷。该步骤需要对系统的各个控制闭环中的各单元进行研究，从而分辨出系统的控制缺陷，如图3所示。

图3 控制缺陷分类Figure 3 Classification of unsafe factors

2.2 UPPAAL 和时间自动机

时间自动机是在有限自动机的基础上添加了时间约束产生的[9]，可以有效地对实时系统进行建模和验证[10]，基于车车通信的列控系统是实时系统。

UPPAAL是一个对实时系统建模和验证的工具[11]，为实时系统的模型验证提供了一种规范化的验证语法-BNF(Backus-Naur Form，巴科斯范式)语法[12]，其规则如下：

3 TSR下发场景的安全性分析

考虑到不同场景下的事故会由不同的因素造成。以资源管理单元RMU向VCM下发临时限速为例，采用STPA方法进行安全性分析，目的是识别场景中的危害和不安全控制行为，以便设计安全性约束消除危害。

3.1 TSR下发场景介绍

临时限速命令具有为列车提供安全防护和运行调整的功能。TSR下发的第一步人工输入 TSR参数，DCD接收到参数后生成临时限速命令，经过相关协议拆分和转换后发送给相关RMU进行有效性验证。TSR检验无误后进行保存并等待执行，如果有效性验证失败，通过提示，值班员可在调整TSR参数后再次发送命令。RMU验证成功后，将TSR命令发送给管辖范围内的列车，VCM接收到TSR后，执行临时限速命令，然后向RMU发送反馈信息。

3.2 基于STPA的TSR下发场景安全分析

3.2.1 定义系统级危险及安全约束

由相关标准和规范可以得到列控系统的系统级危险：列车速度大于安全速度或者超出安全距离限制，标记为“H1”作为要分析的系统级危险，针对该系统级危险，安全条件是列车运行控制系统必须保证列车运行速度不超过安全速度或超出安全距离限制。

3.2.2 建立待分析系统的分层控制结构

使用分层框图对基于车车通信列控系统的分层控制结构进行描述。分层控制结构不仅包括列控子系统(例如 RMU，DCD 等)，也包括调度员以及司机等。图4为RMU向VCM发送临时限速命令的分层控制结构图，图中实线框内为基于车车通信的列控系统内部包含的单元，虚线框内为列控系统外部单元。

图4 分层控制结构Figure 4 Hierarchical control structure

在构建分层控制结构图之后，可以细化系统的交互过程，得到过程模型，如图5所示。过程模型是控制器对被控过程的理解和认知[13]，控制器中的相关算法也是在此基础上形成的。

图5 过程模型Figure 5 Process model

3.2.3 不安全控制行为辨识

根据基于车车通信的列控系统在临时限速下发场景中的控制行为，针对危险H1，辨识出可能的不安全控制行为，表1为部分不安全控制行为。

表1 不安全控制行为Table 1 Unsafe control behavior

3.2.4 控制缺陷分析

最后需要研究列控系统的控制缺陷，找到不安全控制场景出现的因素。TSR下发场景中的不安全因素如图6所示。

图6 TSR下发场景中的不安全因素Figure 6 Unsafe factors in TSR sending scenarios

控制缺陷如下：

CD1：调度员疏忽，忘记下达临时限速命令。

CD2：调度员疏忽，过晚的下达临时限速命令。

CD3：调度员操作不当，下达错误的临时限速命令。

CD4：DCD未接受到调度员操作命令，或收到错误的命令，过晚收到命令。

CD5：DCD自身硬件出现故障。

CD6：DCD的算法设计存在缺陷。

CD7：DCD未向RMU下达临时限速。

CD8：DCD对TSR的解析出现错误。

CD9：DCD过晚地向RMU下达临时限速信息。

CD10：RMU未收到来自DCD的TSR，或收到错误的TSR，超时收到TSR。

CD11：RMU自身硬件出现故障。

CD12：RMU的算法设计存在缺陷。

CD13：RMU未向VCM下达临时限速。

CD14：RMU解析TSR出现错误。

CD15：RMU过晚地向VCM下达临时限速信息

CD16：VCM未收到来自RMU的TSR，或收到错误的TSR，超时收到TSR。

CD17：VCM对TSR解析错误。

CD18：VCM自身硬件出现故障。

CD19：VCM的算法设计存在缺陷。

CD20：速度传感器速度测量误差过大。

3.2.5 安全性设计需求

对所得的控制缺陷进行分析，制定出相应的安全性设计需求，为UPPAAL模型验证语句提供来源。部分与RMU相关的安全性设计需求如下：

SDR1：RMU必须进行冗余和可靠性设计。

SDR2：RMU系统的算法必须进行可靠性测试和验证。

SDR3：RMU应对接收到的临时限速信息进行有效性检验。

SDR4：RMU在收到临时限速后应在规定的时间内作出回复。

SDR5：RMU应在规定的时间内将临时限速信息下发给VCM。

SDR6：若RMU在规定的时间内没有收到VCM的反馈，则重发TSR。

SDR7：若RMU超过规定时间未收到来自VCM的反馈，则报警。

4 基于UPPAAL的SDR验证

建立临时限速下发场景中中各个组件的时间自动机模型，包含调度员、DCD、RMU和VCM。由于篇幅有限，这里仅给出临时限速下发场景的时间自动机网络模型以及资源管理单元RMU的时间自动机模型，如图7和图8所示。

图7 TSR发送场景的时间自动机网络模型Figure 7 The timed automata model of TSR sending scenarios

图8 RMU的时间自动机模型Figure 8 The timed automata model of TSR sending scenarios

把以上分析得到的SDR翻译成BNF验证语句，在UAAPPL验证器中对BNF语句进行验证，表2为部分关键的BNF语句以及验证结果。

表2 BNF验证语句Table 2 BNF Statement

验证表明，临时限速下发场景满足STPA模型分析得到的安全性设计需求。

5 结论

使用系统理论过程分析方法对基于车车通信的列控系统中的临时限速下发场景进行了安全性分析，得到该场景下的控制缺陷，通过分析控制缺陷制定了安全性设计需求。将STPA安全分析方法与UPPAAL验证方法相结合，在UPPAAL中验证了SDR的合理性。分析结果表明，STPA和UPPAAL两种方法结合可以有效分析基于车车通信的列控系统的安全性。