随着科技的发展,软件系统所处的环境也随之改变,传统的静态软件体系结构已不再适应当前用户的需求,而动态软件体系结构不仅能够增强用户的自定义性和可扩展性,也能降低系统开发的费用和减少系统所面临的风险,同时还具有为用户提供更新系统属性的服务,因此动态软件体系结构的开发与研究已成为软件工程研究的热点。近年来,动态软件体系结构研究的主要内容集中在建模和模型验证等两方面。动态软件体系结构建模是成功设计软件系统的基础；而动态软件体系结构模型验证是保证动态软件体系结构质量的关键因素。两者缺一不可。动态软件体系结构建模和模型验证具有一定的特殊性,目前对此研究还很不完善,缺少统一的建模和验证方法。由此可知,针对动态软件体系结构建模和模型验证方法的研究具有重要意义,未来此领域将拥有更广阔的发展空间。本文凝聚了作者多年来在软件系统开发领域中的研究成果,结合实践提出对动态软件体系结构建模和模型验证方法用以满足软件体系结构动态性的需求。并通过“电力企业生产工程管理系统”应用案例进行实践验证,取得良好效果。具体内容主要包含以下几点：(1)基于软件体系结构的理论基础,阐述了如何选取适应当前系统环境的动态软件体系结构的建模方法及模型验证方法,并通过实践表明在动态软件体系结构研究领域中,正确选取建模方法和模型验证方法的重要意义。(2)本文提出了一种需求目标驱动的动态软件体系结构建模方法。该方法在Le Metayer的体系结构建模的理论和原则指导下,基于概念属性的需求目标模型和图元符号描述体系的SAAM方法而提出的一种需求目标驱动的动态软件体系结构的建模方法。(3)本文基于谓词μ演算和空间逻辑,提出了一种基于谓词μ演算的空间逻辑的动态软件体系结构属性表示逻辑方法。该方法在谓词μ演算的基础上,增加了空间算子.的表示逻辑,统一地对结构和行为属性进行逻辑表示,解决了属性逻辑分别表示的问题。而在属性逻辑表示的过程中,本文提出了属性目标的部分满意度模型,并基于此模型评估属性满意度,从而解决属性目标常常是部分满足的问题。(4)本文在动态软件体系结构模型验证中,分别提出了需求目标驱动的基于等价理论的缩减状态空间方法和基于LMC的动态软件体系结构模型验证算法。利用等价理论验证体系结构操作前后的等价关系,对动态体系结构模型提出一种新的缩减状态空间方法,从而实现了对初始体系结构的验证并简化了状态空间的搜索,一定程度缓解状态空间爆炸问题；初始体系结构的状态空间可作为模型验证算法的输入,而模型验证算法是模型验证的核心。另外本文基于LMC算法,还提出一种扩展LMC的动态软件体系结构模型验证算法,扩展了对空间算子的验证,解决了结构和行为属性同时验证的问题。(5)根据本文所提出的动态软件体系结构建模和模型验证方法,对“电力企业生产工程管理系统”案例进行了应用研究。