中国列车运行控制系统 1 级(Chinese Train Control System level 1,简称 CTCS-1)适用于200km/h以下新建及改造线路,采用目标-距离连续速度控制模式监控列车安全运行,目前正处于研发阶段。因此,对该系统进行安全分析与评估,来识别特定的应用场景存在的安全隐患,有着非常重要的意义。区域列控数据中心(Regional Data Center,简称RDC)作为CTCS-1级列控系统的核心地面设备,是一个实时多任务系统,它处理来自调度集中、临时限速服务器和车站联锁发送的数据,结合列车的位置报告,通过GSM-R网络向车载设备发送线路数据和临时限速信息。本文研究了基于STPA(System-Theory Process Analysis,系统理论的过程分析)与模型验证相结合的RDC安全性分析方法。与传统的风险识别方法相比,STPA能够系统化、模块化地准确识别风险。论文完成的主要工作如下:(1)首先,以RDC的行车数据生成和临时限速发送场景为例,完成了基于STPA的RDC安全分析流程。对事故和危险进行识别,使用SysML中的内部模块图描述CTCS-1级列控系统的分层控制结构模型,详细刻画RDC的过程模型,分析控制行为缺陷并逐项分析系统中的不安全控制行为,最终得到相关的安全约束和需求(Safety Design Requirement,简称SDR),为之后的UPPAAL模型验证语句提供来源。(2)然后,使用SysML对RDC的主要运营场景进行建模,并将模型转换为时间自动机模型。使用SysML顺序图对RDC信息控制中主要流程进行建模,包括设备启动、列车注册、正常行车、列车注销四个流程,使用SysML顺序图、活动图和状态机图对临时限速场景进行单独建模;采用ATL(Atlas Transformation Language)模型转换方法,通过建立SysML元模型和UPPAAL元模型,以及建立明确的SysML顺序图、活动图和状态机图到时间自动机的转换规则,将SysML顺序图、活动图和状态机图转换为时间自动机模型。(3)最后,完成基于STPA的安全分析和基于UPPAAL的验证的结合,以验证RDC是否满足SDR和相应的功能要求。将STPA分析得到的SDR映射为BNF(Backus Normal Form,巴科斯范式)验证语句,并将其划分为逻辑功能、时序功能和安全性三类语句;将SysML模型转换得到的时间自动机模型进行整合,得到时间自动机模型网络,通过UPPAAL模拟仿真及安全性需求验证,验证了基于STPA的安全分析与模型验证相结合的方法的有效性。