信息物理融合系统CPS是通过计算、通信与控制技术有机和深度的融合实现计算资源与物理资源紧密结合的下一代智能系统,体系结构分析与设计语言AADL是一种基于构件的体系结构建模语言,是嵌入式实时系统体系结构描述语言标准,广泛应用于航空电子等安全关键领域的系统建模分析。本文基于AADL将形式化建模与验证方法引入CPS的分析与设计中,提出了一套面向CPS的模型建立、模型转换及模型验证的完整框架。首先,对AADL的基本建模元素、建模流程及CPS系统特点、建模需求进行研究分析,总结AADL对CPS软硬件体系结构建模的优点,以及对CPS中大量数据和并发、不确定关系缺乏形式化描述的不足,基于形式化规格说明语言Z和进程演算对AADL进行扩充,为AADL添加对变量约束的Z模式和并发、不确定以及动作约束算子的描述,对数据进行形式化的描述来对其进行约束,对动态并发、不确定的因素进行建模,提出一种能够描述CPS系统行为的体系结构建模规范CPS-AADL。其次,由于AADL不支持直接的形式化验证,本文在构件交互自动机研究的基础上提出一种带数据约束并支持系统构件交互描述的形式化规范,带数据约束的构件交互自动机Z-COIA,同时给出Z-COIA的组合验证算法,并将CPS-AADL模型转换到Z-COIA形式化规范,给出了模型转换规则及其正确性说明。最后,在经典时序逻辑的基础上提出了面向Z-COIA的时序逻辑系统CIA-CTL,并给出其具体的语法语义定义和模型检测算法,从而实现了对CPS-AADL模型检测和验证分析,并通过一个典型的CPS系统——喷气飞机的飞行导航系统的模型建立、模型转换以及模型验证的具体过程和对本文给出的形式化建模与验证的整体框架进行分析实践,验证了提出的形式化建模方法的可行性和有效性。