摘要

As the development and wide usage of Software architecture (SA), SA evolution becomes one of the hotspots of current research in modern software engineering domain. Most current researches concentrate on the modeling of SA evolution and lack the verification and evaluation of SA evolution. We proposed a verification based approach to evaluate SA evolution. The basic process includes: 1) using Unified modeling language (UML) sequence diagram to model the interaction of components and study different types of evolution in practical examples; 2) using SPIN-based model checking to model and verify SA evolution; 3) comparing various verification outcomes and analyzing the influence of SA evolution on SA correctness and temporal properties. Both theory analysis and an experiment on a real evolution example from Model-view controller (MVC) to Spring web MVC (SWMVC) show that the verification-based approach to evaluate SA is significant.