中国列车运行控制系统 3 级(Chinese Train Control System Level 3,CTCS-3)是我国高速铁路的核心装备,负责保障高速铁路列车的行车安全,也是高速铁路的“神经中枢”,其安全性对于高速铁路的安全运营起到了关键的作用。无线闭塞中心(Radio Block Center,RBC)交接场景是CTCS-3级列车运行控制系统(简称CTCS-3级列控系统)的重要运营场景。针对其特点研究有效的、科学的安全分析方法,对于保障高速铁路的安全具有重要意义。然而,CTCS-3级列控系统的功能和组件交互之间的关系错综复杂,运用传统的安全分析方法时会面临挑战。系统理论过程分析(System-Theoretic Process Analysis,STPA)作为建立在系统理论事故模型(Systems-Theoretic Accident Model and Process,STAMP)基础上的新技术,将导致危险的主要原因归结为组件间的异常交互,满足CTCS-3级列控系统对安全分析方法的要求。但是,目前没有统一的方法来描述该模型,而采用自然语言建模又容易受人员表述能力的影响而导致歧义。此外,STPA安全分析主要依靠分析人员人工实施,其分析结果的可信度受分析人员经验的影响较大。本论文从目前现有的建模与分析方法存在的不足出发,利用UML统一建模语言的可扩展性等优点,对STPA方法中系统分层控制结构模型的构建方法进行改进,并利用NuSMV能自动给出反例的特性辅助实施STPA安全分析过程。主要的内容包括:(1)在理解并阅读了大量国内外文献研究之后,简单介绍目前安全分析方法的研究情况,并针对不同安全分析方法的优点及不足做出对比和分析,明确现有安全分析方法在列控领域的研究前景。(2)设计面向STAMP模型的UML概要文件,扩展UML类图和控制反馈消息,针对STPA方法进行扩展,从而刻画出待分析系统的分层控制结构模型。(3)将上述半形式化的UML模型转化为形式化NuSMV模型,构建功能失效描述符号(Functional Failure Description Symbol,FFDS)和故障模型(Fault Pattern,FP),对可能的功能模块失效进行文本描述,并将系统的行为模型与故障模型相整合,形成包含故障集的NuSMV模型。然后,运用模型检验的方法构建控制缺陷的分析方法。(4)针对RBC交接场景的特点,分别从静态结构以及动态行为的角度出发来描述研究实例,运用UML扩展后的概要文件创建实例中的分层控制结构模型。运用UML类图描述分层控制结构,用状态图描述控制算法,用OCL语言描述过程模型。(5)运用STPA扩展后的方法,分析RBC交接场景的控制缺陷。首先确定系统级危险,并运用STPA方法的流程分析不安全控制行为。然后将系统的不安全控制作为性质,运用NuSMV模型检验工具分析上述性质,在已建立的故障集中辨识出系统的控制缺陷。