近年来,模型驱动(Model-Driven)尤其是采用形式化模型驱动的安全关键软件设计与开发方法逐渐受到重视,并被工业界认为是切实可行的重要手段。AADL(Architecture Analysis and Design Lanuage)是一种广泛应用于安全关键领域的形式化建模语言标准。然而,由于AADL语言的语法元素庞大、语义复杂,手工构建安全关键软件尤其是大规模复杂安全关键软件的AADL设计模型难度较大。如何自动或半自动构建AADL形式化设计模型是目前工业界和学术界广泛关注的问题。本文提出了一种面向安全关键软件建模的AADL设计模型自动生成方法,重点研究了基于限定自然语言的安全关键软件需求建模及其到AADL模型的自动转换、基于源代码的AADL模型逆向重构等关键问题,并设计和开发了相关原型工具,主要研究成果如下:首先,安全关键软件引起严重事故的原因往往可以追溯到软件需求尤其是安全性需求的问题,当前工业界的软件需求主要通过自然语言文本描述,而自然语言二义性、不精确、难以被自动处理的特性使得模型驱动开发方法的生命周期一般较少涉及需求阶段。本文针对自然语言需求和AADL模型驱动开发方法之间还存在鸿沟的挑战,提出一种基于限定自然语言的安全关键软件需求规约方法RNLreq及其到AADL设计模型的自动转换方法RNL2AADL。RNLreq通过数据字典、领域词库、需求模板和限定句式等结构化方式约束工程师的需求描述行为,能够在尽量不改变工程师撰写软件需求的习惯的前提下,通过约束自然语言的表达能力降低需求的二义性;RNL2AADL通过自动化转换,能够有效降低工程师构建AADL设计模型的难度。其次,在安全关键软件系统开发与维护过程中,部分需求与设计信息往往遗留在源代码中而没有反馈补充到自然语言需求,因此,在对已有软件系统架构进行复用或重构的过程中,如何将这部分需求与设计信息从代码中抽取到AADL设计模型也是一个重要问题。本文提出一种从C代码到AADL模型的自动转换方法C2AADL,基于抽象语法树对C代码进行解析,并通过一个中间转换模型CAInterM简化转换过程,给出C到CAInterM再到AADL的转换算法。C2AADL能够自动抽取并保留代码中的架构信息,减少软件架构复用或重构过程中的工作量。最后,在AADL开源建模环境OSATE中实现了限定自然语言需求规约工具RNLreqTool、RNLreq到AADL模型转换工具RNL2AADLTool和C程序到AADL模型转换工具C2AADLTool等三个原型工具,并基于航天导弹发控系统进行了应用性验证。