嵌入式系统广泛应用于诸如航天、航天、交通等安全关键领域,这类系统通常具有较高的安全性和可靠性约束,一旦失效即有可能导致重大的财产损失、环境破坏以及人员伤亡等重大后果,因此,我们一般将这类系统称之为安全关键系统。对于安全关键系统,构建其软件工程体系是十分困难的,其中一个难点就在于系统要遵循合法的,可控的需求。在软件开发过程中,需求是否有缺陷对安全关键系统的安全性和可靠性有决定作用。因此在安全关键系统开发过程中,各制品间的可追踪关系是非常重要的一个环节,尤其是需求和设计之间的一致性关系。目前,由于需求大多是用领域相关的自然语言来描述,或者使用如RUCM等半形式化的方法描述。而设计模型大多使用的是形式化或者半形式化的语言,从而难以保证安全关键系统的需求和设计模型之间的一致性。根据软件项目统计结果发现:50%以上的系统错误是由于需求的错误或缺失导致的,而且在追踪这些错误需求要花费超过80%的错误修正成本。因此如果可以改进需求描述,加强需求和设计之间的联系,那么这些系统错误可能可以被更早地发现并且可以尽早解决这些错误。由此可见,减少需求中的缺陷,建立需求和设计模型间的追踪关系,对于安全关键系统的开发具有重要意义。本文使用复杂嵌入式实时系统体系结构建模语言AADL(Architecture and Analysis Design Language)作为安全关键系统设计建模语言,能够有效描述系统运行时体系结构模型,并且AADL具有子语言扩展的附件,如AADL错误模型附件,使其能更好地支持系统体系结构建模。AADL的需求附件给出了一个系统保证方法ALISA(Architecture-Led Incremental System Assurance),该方法可以用于验证软件的设计模型是否可以满足相应的需求。目前,使用ALISA方法来检验自然语言需求和AADL模型之间的一致性关系仍存在很多问题:ALISA提供了形式化的需求规约,但是和非形式化的自然语言文本需求还具有很大的差距,因此无法直接将自然语言的需求文本转化到ALISA需求规约;ALISA可以针对不同抽象层面的AADL模型的某个构件属性进行验证,但是由于AADL模型具有多个抽象层次,多个构件和多个属性,人为地进行AADL模型的检验需要很大的工作量;另一个问题是,ALISA只考虑了需求和AADL核心构件之间的追踪关系并没有考虑AADL的错误模型附件。针对以上问题,本文提出一种新的需求验证方法,即使用ALISA框架来实现AADL模型和自然语言需求一致性的自动化验证。主要研究内容如下:(1)对于自然语言的二义性和不确定性问题,本文设计了一个面向特定领域的限定自然语言的需求模板用于安全关键系统需求规约,然后通过模型转换的方式实现限定自然语言需求模板到ALISA形式化需求规约的转换。(2)对于AADL多层次设计模型难以进行人为验证的问题,根据ALISA的需求规约和相应的AADL模型,使用ATL(ATLAS Transformation Language)技术,在元模型层面上定义转换规则,可以自动化地生成模型的验证框架,该验证框架可以用于验证需求中的关键属性。(3)对于ALISA需求规约无法描述AADL错误模型附件信息的问题,扩展需求规约来描述不同错误状态,并将扩展后的需求规约与其他ALISA框架元素相关联。最后根据错误附件和需求规约,使用ATL技术,自动化生成验证框架。在上述理论工作的基础上,设计并实现了相应的原型工具,并通过一个典型的安全关键系统——婴儿保温箱恒温系统进行案例分析。根据本文所给出的一致性定义,来判断系统设计是否满足需求,以实现在软件开发过程的前期实现需求确认,从而降低开发成本,由此来阐述本文方法的有效性和可行性。