Verification-Based Analysis And Evaluation Of Software Architecture Evolution

The evolution reflects "The process of continuous attributes improvement of evolution entities or their components.", while software evolution refers to the continuous changes of the software system or its components to satisfied new functional or attribute requirements. In the lifecycle of modern software system, the evolution exists throughout the whole development. Many factors require software have a stronger ability of evolution to guarantee the correctness of system, which including the change of system requirements, the improvement of functions, the discovering of new arithmetic, the change of environment, etc. Following the development of SA (software architecture), SA, as the early design products of software lifecycle, describes structure, behavior and attribute information from the perspective of global and overall. This makes it very crucial that the evolution result of SA design is correct or not.Therefore, this thesis special concentrates on the analysis and verification of SA evolution by using model checking method to efficient and automatic verify SA design. Spin is a famous and widely used model checking tool, which can efficient realize correctness verification of SA design. However, the Promela model is difficult to conduct intuitive modeling work, which means that the model-based evolution work is extremely hard. Therefore, we need to establish a SA model to assist verifying and analyzing evolution.In the thesis, the SA design is described by UML (Unified Modeling Language), thus we use EHA (Extended Hierarchical Automata) to modeling SA design, which is the basis of verification and evolution analysis. Based on the EHA model, the thesis introduces a Spin-based verification method, which transform the SA design from UML to EHA model; use LTL (Linear Temporal Logic) to describe the system constraint; generate verification model from EHA model and LTL formula; use Spin to verify and gain the verification result. Then, the thesis describe the SA evolution process, and detailed analyze the evolution operation and rule of each element in the UML sequence diagram, including object, message and fragment. Then, based on the verification method before, we propose a SA evolution analysis and evaluation method, which obtain the evolution information from de SA evolution documents and the verification result of each SA design; analyze the verification result and evolution influence to summarize a comprehensive evaluation consequence. Finally, the thesis conduct two experiments, the SA evolution of Hadoop and MVC, to explain how to use out evaluation method to work on the actual cases, in the circumstances of knowing the specific evolution process or not.