###
Journal of Software:2016.27(7):1772-1788

一种演化超图文法到状态转移系统的映射方法
徐洪珍,曾国荪,王晓燕
(东华理工大学 计算机科学与技术系, 江西 南昌 330013;同济大学 计算机科学与技术系, 上海 201804)
Method of Mapping Evolution Hypergraph Grammars to State Transition Systems
XU Hong-Zhen,ZENG Guo-Sun,WANG Xiao-Yan
(Department of Computer Science and Technology, East China University of Technology, Nanchang 330013, China;Department of Computer Science and Technology, Tongji University, Shanghai 201804, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 1557   Download 1381
Received:August 18, 2014    Revised:November 24, 2014
> 中文摘要: 运用模型检测技术验证动态演化的正确性,是近年来软件体系结构动态演化研究领域面临的一个挑战.然而,当前的方法很少考虑软件体系结构动态演化时的相关条件.针对该问题,提出用条件状态转移系统表示软件体系结构动态演化的状态模型,将软件体系结构超图映射为状态,演化规则运用映射为条件状态转移关系,给出软件体系结构动态演化的条件超图文法到条件状态转移系统的映射方法以及相应的实现算法,实现了软件体系结构动态演化的条件状态转移系统的构建,并证明了在该映射方法下,软件体系结构动态演化条件超图文法与条件状态转移系统的互模拟等价.最后通过案例分析,运用该方法以及模型检测技术,验证了软件体系结构动态演化的相关性质,从而验证了该方法的有效性.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61272107,61262001);国家高技术研究发展计划(863)(2009AA012201);国家教育部网络时代的科技论文快速共享专项(20110740001);江西省青年科学家培养对象计划(20142BCB23017);江西省自然科学基金(20114BAB201043);江西省科技支撑计划(20112BBE50048);江西省发明专利产业化技术示范项目(20143BBM26115) 国家自然科学基金(61272107,61262001);国家高技术研究发展计划(863)(2009AA012201);国家教育部网络时代的科技论文快速共享专项(20110740001);江西省青年科学家培养对象计划(20142BCB23017);江西省自然科学基金(20114BAB201043);江西省科技支撑计划(20112BBE50048);江西省发明专利产业化技术示范项目(20143BBM26115)
Foundation items:National Natural Science Foundation of China (61272107, 61262001); National High Technology Research and Development Program of China (863) (2009AA012201); Special Plan of the Rapid Sharing of Technology Papers in the Network Era of Higher Education of China (20110740001); Program of Training Young Scientists of Jiangxi Province (20142BCB23017); Natural Science Foundation of Jiangxi Province of China (20114BAB201043); Science & Technology Support Program of Jiangxi Province of China (20112BBE50048); Invention Patent Industrialization Technology Demonstration Project of Jiangxi Province of China (20143BBM26115)
Reference text:

徐洪珍,曾国荪,王晓燕.一种演化超图文法到状态转移系统的映射方法.软件学报,2016,27(7):1772-1788

XU Hong-Zhen,ZENG Guo-Sun,WANG Xiao-Yan.Method of Mapping Evolution Hypergraph Grammars to State Transition Systems.Journal of Software,2016,27(7):1772-1788