列车运行控制系统(以下简称“列控系统”)需求规范是列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,由于列控系统是一个复杂的安全苛求系统,仅依靠经验制定的系统需求规范不可避免地存在某些漏洞或者安全隐患。另外,用自然语言刻画的系统需求规范可能存在歧义,这为系统的设计与开发带来不利影响。因此对列控系统需求规范进行形式化建模与验证显得十分必要。本文以我国CTCS-3级列控系统需求规范为应用背景,围绕系统需求规范的建模与验证方法展开研究。首先,提出了一种改进型列控系统需求规范形式化建模与验证方法,其主要特点是能够在系统需求规范、模型、验证过程以及验证结果之间建立一条双向、完整的追踪链,始终保证系统需求规范、模型以及程序代码之间的一致性。然后,在该方法的基础上,对如何保证模型与系统需求规范的一致性和覆盖性,以及系统需求规范的UML模型与CSP模型之间的转换技术进行了深入探讨。论文的主要成果和创新点有：(1)通过集成规范管理、形式化建模以及验证等多种技术手段,改进了当前的列控系统需求规范建模与验证方法。与其它建模与验证方法只能针对系统需求规范的某一场景或某种单一特性不同,该方法能够适用于整个列控系统需求规范。(2)针对列控系统需求规范的特点,在列控系统需求规范形式化建模与验证方法中强化了安全规范要素,通过映射关系,用形式化方法将安全要素融入规范模型中。同时,建立了相对完整的追踪与反馈机制,有助于研究人员对自然语言系统需求规范与模型进行一致性和覆盖性进行分析,并且能够实现建模模型与验证模型的转换以及对验证结果的分析,从而使验证结果能够利用反馈机制追踪至规范文档。(3)建立了基于扩展UML的列控系统需求规范建模方法,给出了列控系统需求规范建模模板,模板中的构造型、标记值及约束刻画了系统需求规范中主要的强制性安全需求,使模型能够体现系统的安全特性,并且增强了模型的可重用性,提高了建模的效率。另一方面,细化了规范建模和模型检查规则,明确定义了列控系统需求规范片段的分类方法以及规范与模型的映射方式。这些规则的建立,能够大大减少建模人员在建模过程中的主观因素。(4)提出了UML模型转换成CSP模型的方法,分别建立了UML和CSP的元模型,通过分析源元模型和目标元模型语言的特征,建立了一组模型转换规则,以实现原子映射和模式映射。为了保证严谨而科学的模型转换过程,探讨了模型转换中特性的保持及转换规则正确性的证明方法。(5)设计并实现了列控系统需求规范形式化建模与验证软件工具。该软件工具集模型抽取、转换、验证以及分析功能于一体,为列控系统需求规范的建模与验证提供了一个自动化的环境。应用表明,利用该软件工具,能够有效提高列控系统需求规范建模与验证的效率。