| 摘要: |
| 运用模型检测技术验证动态演化的正确性,是近年来软件体系结构动态演化研究领域面临的一个挑战.然而,当前的方法很少考虑软件体系结构动态演化时的相关条件.针对该问题,提出用条件状态转移系统表示软件体系结构动态演化的状态模型,将软件体系结构超图映射为状态,演化规则运用映射为条件状态转移关系,给出软件体系结构动态演化的条件超图文法到条件状态转移系统的映射方法以及相应的实现算法,实现了软件体系结构动态演化的条件状态转移系统的构建,并证明了在该映射方法下,软件体系结构动态演化条件超图文法与条件状态转移系统的互模拟等价.最后通过案例分析,运用该方法以及模型检测技术,验证了软件体系结构动态演化的相关性质,从而验证了该方法的有效性. |
| 关键词: 软件演化 体系结构 模型检测 条件超图文法 条件状态转移 |
| DOI：10.13328/j.cnki.jos.004841 |
| 分类号: |
| 基金项目:国家自然科学基金(61272107,61262001);国家高技术研究发展计划(863)(2009AA012201);国家教育部网络时代的科技论文快速共享专项(20110740001);江西省青年科学家培养对象计划(20142BCB23017);江西省自然科学基金(20114BAB201043);江西省科技支撑计划(20112BBE50048);江西省发明专利产业化技术示范项目(20143BBM26115) |
|
| Method of Mapping Evolution Hypergraph Grammars to State Transition Systems |
|
XU Hong-Zhen1,2, ZENG Guo-Sun2, WANG Xiao-Yan1
|
|
1.Department of Computer Science and Technology, East China University of Technology, Nanchang 330013, China;2.Department of Computer Science and Technology, Tongji University, Shanghai 201804, China
|
| 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. |
| Key words: software evolution architecture model checking conditional hypergraph grammar conditional state transition |
