安全关键系统是指那些系统失效会造成人员伤亡,环境和财产等的重大损失的软件系统。航空电子系统作为飞机上的核心系统,是典型的安全关键系统。需求分析是系统开发人员通过调研与分析,对用户和系统功能,性能等要求进行理解,并将非形式的需求描述转换为完整的需求定义的过程,是系统开发过程中最重要的阶段。但传统的需求表述方式由于自然语言的二义性,无法验证需求特性等问题使得需求容易出错,并且难以处理高度复杂的大型系统。基于形式化方法的需求归约过程以严格定义的语义和数学模型为基础,使得需求的表述更加清晰明了,易于理解,通过需求的自动化测试和检验工具的检验提高了需求的正确性和分析效率。但目前的形式化需求方法过于通用,工具普遍缺少安全属性的验证。本文以SCR(Software Cost Reduction)方法的研究为背景,针对传统的需求描述方法容易引入错误的问题,将SCR方法应用在飞机襟缝翼系统中,解决SCR方法过于通用性的问题,从保证系统安全性的角度出发,对基于SCR方法的检验工具T-VEC的功能进行扩展,增加安全属性验证的功能。具体研究内容如下所述:本文将形式化需求分析方法应用到安全关键性系统航空电子系统当中,使用SCR方法对原有的飞机系统中的襟缝翼控制系统的需求文档进行形式化的需求归约,针对襟缝翼控制系统中的襟翼电机转速控制模块进行详细的案例分析,通过T-VEC工具的分析和验证判断其是否满足需求的一致性、语法正确性、完备性等特性。进一步提出了SCR方法中的一些应用技巧。该工作将对SCR方法在机载软件系统中的应用提供依据。在对需求模型的安全性验证方面,对T-VEC工具进行扩展,本文在语言解析器生成器antlr的辅助下开发了模型转换工具T2N,设计语言结构转换规则,将需求描述语言T-VEC转换为符号化模型检测语言XMV,实现对提取的系统安全属性的自动化验证。基于所开发的模型转换工具T2N,以需求工程中的典型案例灯光控制系统为例,建立系统需求模型,利用T2N工具转换为NuXMV模型,并进一步在模型中添加系统安全属性。最后,在模型检测器NuXMV中对转换后的模型进行实验分析,验证T2N工具的有效性和需求模型的安全性。