随着软件系统开发在各行各业的不断运用和发展,人们对软件系统的实时性、可靠性和安全性等任务关键属性要求越来越高。为保证软件开发的质量,人们采用模型驱动的软件开发方法分析任务关键软件的功能和非功能属性需求,同时为了保证软件需求的正确性,利用形式化方法对用户需求进行规约。本论文结合实验室承担的国家“863”项目子课题“嵌入式软件B方法需求描述与转化方法研究及工具开发”,对形式化开发方法—B方法和体系结构分析与设计语言AADL展开研究,通过对已有的关于B方法和AADL的应用进行分析,参考已有理论成果,以项目研究的任务关键系统为背景,将在用户需求、B方法和AADL模型之间建立关联,设计出B方法到AADL模型转换工具。本文的主要工作如下：1.介绍了B方法和AADL的基础理论,分析了B方法抽象机和AADL构件模型。2.分析了将用户需求转换为B方法描述的必要性以及用B方法进行模型规约的优点。3.通过分析用户需求和B方法之间的关系,定义用户需求到B方法的转换规则,运用模型测试的方法验证转换规则的正确性。4.设计了基于B方法需求规约的转换工具。转换工具可以实现基于B方法的需求规约自动生成。我所做的B方法到AADL转换工具的实现,很好的完成了项目子课题的要求,设计的转换工具也很好的融入了模型驱动的任务关键软件系统测试的环境,对基于AADL模型驱动的测试提供了帮助。