摘要：列控系统需求工程是列控系统开发的起点和基础。对需求规范进行建模分析是提高规范质量、降低系统开发风险和成本的有效手段。CTCS-3级列控系统的研究采用了“标准先行”的国际通用方法,即先制订系统的标准规范,以便于指导系统后续的研发。而需求规范的制定多数是依靠领域专家的经验,自然语言以及人为因素不可避免地存在某些漏洞或表意不清,这为系统的设计与开发带来了不利影响。因此对列控系统需求规范进行形式化建模与验证显得十分必要。本文以CTCS-3级列控系统需求规范为主要研究对象,并对其建模与形式化验证分析方法展开研究。主要内容包括以下三点：1、本文着眼于研究一种有效的列控系统规范建模分析方法,该方法从系统需求、静态结构以及动态行为三方面描述了列控系统的主要特征,并对SysML建模语言进行了扩展,设计了SysML概要文件,从而增强了建模语言的刻画能力。2、从定性和定量分析两个方面提出了两种需求规范的形式化分析方法。其中,基于属性的需求分析方法是对规范模型进行定性分析,从系统规范的一致性、系统的可实现性、设计意图以及相关性质的确认方面进行了分析验证。而基于MITLFG的需求分析方法是对规范中带有时间约束的需求进行定量刻画,两者之间起到了互补的作用。3、为了更好地运用列控系统规范的建模与分析方法,开发了一款软件：ReqTool。该软件实质是一个工具集,它以Eclipse平台为基础,通过扩展Eclipse接口与RATSY、Topcased进行集成,实现模型提取、模型构建以及模型分析三大主要功能,大大地提高了建模与验证的效率,较好地实现了建模验证的自动化。