摘要：在中国的交通运输体系中,铁路已经成为其中最重要的基础设施和最大众化的交通工具。而列车运行控制系统(简称列控系统)是保证列车行车安全和高效运行的关键装备,是整个铁路系统的核心技术。一旦列控系统出现安全性问题,极有可能导致行车中断,甚至是车毁人亡的灾难。因此,在列控系统开发的早期,即需求阶段对系统进行安全分析尤为重要。列控系统的研究采用国际通用的方法——“标准先行”,即先完成系统规范的制定,然后以此指导后续的系统开发。故此,本文对于列控系统需求阶段的安全分析是以列控系统需求规范作为研究对象,并对其描述的系统进行建模分析与形式化验证,然后建立故障模型进行融合完成安全分析。主要的研究内容如下：1、采用统一建模语言(Unified Modeling Language, UML)对列控规范进行初期建模分析,从系统需求、静态结构和动态行为三个维度抽象出列控系统的主要特征,并对建模语言进行了扩展设计,增强建模语言的刻画能力。2、运用转换规则,将UML模型转换成形式化NuSMV模型,利用形式化技术完成需求规范的验证,奠定后续安全分析的基础。提出故障模式的失效符号标记,产生融合故障模型的形式化模型,完成本文提出的基于UML-NuSMV模型的列控系统需求阶段安全分析的工作。3、为列控系统需求阶段的属性验证和安全分析开发了支持工具：RMTool。该工具实质是一个插件,集成到(Rational Software Architect, RSA)平台,通过相关的接口与形式化工具、UML模型进行链接,实现模型转换、属性验证以及安全分析三大主要功能,较好地辅助本文研究内容的展开。