结构分析与设计语言AADL是一种嵌入式实时系统的体系结构建模的语言标准,因为其可以兼顾软件和硬件两方面共同建模,已被广泛应用于许多安全攸关系统的建模,如航电系统以及大型构件式系统等系统。对于系统建立的模型,采用何种方式去验证其安全可靠性目前已经成为AADL研究领域的一个主流方向。在系统建模过程中,对于采用构件组合技术实现封装多业务功能的大型系统,AADL已经有很多方面详细的语义描述如线程、进程、行为附件以及连接等,但对于模型中的数据约束性质和状态变迁的时序性质的刻画仍然有所欠缺,同时形式规则说明语言Z语言对于数据约束的描述方面具很强的表达能力,计算树逻辑CTL可以很好地描述状态在变迁时的时序性质。通过对AADL进行Z语言和CTL扩充,使得对构件式系统的子系统建立的模型可以更好的组合成安全可靠的模型。在形式化建模方面,本文提出在AADL的行为附件里扩充Z语言和计算树逻辑CTL,用来描述组件之间的数据约束性质和具有时序性质的状态变迁,提出了Z-AADL建模规范,增强了AADL建模的灵活性和多样性,也为不同开发人员采用不同建模方式的多模块间的组合提供了可能。另外,对于上述构件式系统的组合式建模,本文提出了针对采用不同建模方式的模型,分别采用模型检测和定理证明对其进行组合验证。对于模型检测部分,本文将Z-AADL建模规范转换成ZIA规范后对系统进行验证;对于定理证明部分,本文首先给出计算树逻辑的公理系统,然后采用定理证明器PVS验证时序逻辑公式,从而验证系统在时序性质方面的安全可靠性。在每章的最后,都给出了相应的实例来说明文中提出的建模或验证方法的可行性。