演化反映了“在演化实体或其组成元素的属性方面不断改进的过程”,而软件演化就是指软件系统或内部组成元素不断地改变来满足新的功能需求或属性需求。在现代软件系统的生命周期内,演化是一项贯穿始终的活动,系统需求的改变、功能实现的增强、新型算法的发现、运行环境的改变等等均要求软件系统具有较强的演化能力,这就要求能够保障系统的正确性。而随着软件架构的发展,作为软件生命周期中的早期设计产品,架构从全局和整体的角度为系统提供结构、行为和属性等信息,使得架构设计的演化结果的正确与否十分关键。本文重点关注对于软件架构演化的分析,以及对架构及架构演化的正确性验证。由于架构设计的复杂化,使得对架构正确与否的人工判断工作变得复杂化和难以保证准确性,而模型检验的方法能够有效地验证架构演化的正确与否,来完成这项工作。基于模型检验的工具Spin能够有效地实现对架构设计的正确性验证,但是其所需要的Promela模型无法进行直观的建模工作,不具有通用性,使得在此基础上的演化工作难以进行。因此,这需要我们建立一个架构模型来帮助验证和演化分析工作。本文使用UML (Unified Modeling Language)作为架构描述的输入,针对于架构设计的正确性相关的UML顺序图,采用扩展层次自动机对其进行建模,作为验证和演化分析的基础。本文首先介绍了基于Spin的软件架构验证方法,将架构设计文档转换成扩展层次自动机模型,采用线性时态逻辑语言LTL对架构约束进行描述,从自动机模型和LTL生成Promela模型,采用Spin进行验证并获得单版本的验证结果。而后,论文描述了架构演化的过程,并在层次自动机模型的基础上详细分析顺序图中的各种元素,包括对象、消息和复合片段,从它们的各自操作出发,分析各个元素的演化方式和演化规则。而后,在此基础上提出了一个基于验证的架构演化分析和评估方法,从各个版本的验证结果中可以获取演化的信息,以及演化对架构正确性产生的影响,从而完成对演化的分析与评估工作。最后论文通过Hadoop和MVC两个实验,分别说明了在不清楚演化过程和清楚演化过程两种情况下,如何应用我们的方法进行分析与评估工作。