Abstract:How to verify the correctness of dynamic evolution process using the model checking technique is a challenge in the dynamic software architecture evolution research field at present. In fact, the existing approaches in this direction rarely consider relevant conditions of dynamic software architecture evolution. To solve the problem, this paper proposes a state model of dynamic software architecture evolution using the conditional state transition system. This approach maps software architecture hypergraphs to states, and the application of evolution rules to the conditional state transition relation. It also provides the method for mapping conditional hypergraph grammars of dynamic software architecture evolution to conditional state transition systems and corresponding realization algorithms, as well as for implementing the construction of the conditional state transition system of dynamic software architecture evolution. Furthermore, the bisimulation equivalence between the conditional hypergraph grammar of software architecture dynamic evolution and the conditional state transition system under the mapping method is proved. Finally, the paper presents a case study in applying the proposed method and model checking to verify corresponding properties of dynamic software architecture evolution, demonstrating the effectiveness of the proposed method.