中文摘要：

运用模型检测技术验证动态演化的正确性,是近年来软件体系结构动态演化研究领域面临的一个挑战.然而,当前的方法很少考虑软件体系结构动态演化时的相关条件.针对该问题,提出用条件状态转移系统表示软件体系结构动态演化的状态模型,将软件体系结构超图映射为状态,演化规则运用映射为条件状态转移关系,给出软件体系结构动态演化的条件超图文法到条件状态转移系统的映射方法以及相应的实现算法,实现了软件体系结构动态演化的条件状态转移系统的构建,并证明了在该映射方法下,软件体系结构动态演化条件超图文法与条件状态转移系统的互模拟等价.最后通过案例分析,运用该方法以及模型检测技术,验证了软件体系结构动态演化的相关性质,从而验证了该方法的有效性.

英文摘要：

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.