随着安全关键软件的规模和复杂性不断增长,确保软件设计和功能的正确性变得更加困难。模型驱动开发方法已经成为了安全关键软件设计与开发的主要手段,而AADL(Architecture Analysis and Design Language)作为复杂嵌入式系统的体系结构与分析标准语言,广泛应用于安全关键软件的软/硬件体系结构、运行时环境、功能和非功能属性的建模。AADL语言能够比较自然的将复杂安全关键软件的层次分解(Hierarchical Decomposition),通过层次化的方法能够抽象的管理系统的复杂度。在工业界应用中,如何完成对层次化的复杂AADL模型验证是亟待解决的问题,而传统的AADL模型验证方法往往是将扁平化的整个模型进行模型转换然后直接验证,这种方法将整个模型的状态空间展开,在验证复杂系统的AADL模型时存在状态空间爆炸问题。本文提出了一种面向安全关键软件的AADL模型组合验证(Compositional Verification)方法,重点研究了AADL体系结构模型的组合验证和AADL组件功能行为验证等关键问题,并设计和开发了AADL模型验证原型工具。主要研究成果如下:首先,提出AADL体系结构模型的组合验证方法,基于系统层次分解构造系统的AADL体系结构模型,然后将系统各个层次的组件需求形式化为组件契约,即抽象的外部可见行为,基于组件契约对系统体系结构模型进行验证,验证系统体系结构的正确性。然后,提出了AADL2UPPAAL的模型转换方法,将AADL模型转换为UPPAAL模型对体系结构模型的叶子组件的功能行为进行验证与分析,UPPAAL以时间自动作为理论基础,使用时间计算树逻辑支持功能正确性、可达性、安全性等性质的验证。最后,基于开源建模环境OSATE设计并实现了AADL模型验证原型工具,支持基于AGREE的体系结构模型的组合验证和支持基于UPPAAL的组件功能行为验证,然后采用了AGREE和UPPAAL相结合的方式对工业界实际案例进行验证,并通过对工业界实际案例分析了AADL组合验证工具的有效性和局限性。通过上述验证方法,不仅保证了单组件的功能正确性,也能保证整个系统的体系结构正确性。