微信服务号

微信订阅号

2025年4月5日 22:10 星期六
首页 > 过刊浏览>2016年第27卷第7期 >1772-1788. DOI:10.13328/j.cnki.jos.004841
PDF HTML阅读 XML下载 导出引用 引用提醒
一种演化超图文法到状态转移系统的映射方法
作者:
基金项目:

国家自然科学基金(61272107,61262001);国家高技术研究发展计划(863)(2009AA012201);国家教育部网络时代的科技论文快速共享专项(20110740001);江西省青年科学家培养对象计划(20142BCB23017);江西省自然科学基金(20114BAB201043);江西省科技支撑计划(20112BBE50048);江西省发明专利产业化技术示范项目(20143BBM26115)


Method of Mapping Evolution Hypergraph Grammars to State Transition Systems
Author:
Fund Project:

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)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [33]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [1] Godfrey MW, German DM. The past, present, and future of software evolution. In:Proc. of the 24th IEEE Int'l Conf. on Software Maintenance. Washington:IEEE Press, 2008.129-138.[doi:10.1109/FOSM.2008.4659256]
    [2] Boehm B. The changing nature of software evolution. IEEE Software, 2010,27(4):26-28.[doi:10.1109/MS.2010.103]
    [3] Shaw M, Clements P. The golden age of software architecture. IEEE Software, 2006,23(2):31-39.[doi:10.1109/MS.2006.58]
    [4] Gomaa H, Hussein M. Software reconfiguration patterns for dynamic evolution of software architectures. In:Proc. of the 4th Working IEEE/IFIP Conf. on Software Architecture (WICSA 2004). Norway:IEEE CS Press, 2004.79-88.[doi:10.1109/WICSA. 2004.1310692]
    [5] Mens T, Magee J, Rumpe B. Evolving software architecture descriptions of critical systems. IEEE Computer, 2010,43(5):42-48.[doi:10.1109/MC.2010.136]
    [6] Zhang P, Muccini H, Li B. A classification and comparison of model checking software architecture techniques. Journal of Systems and Software, 2010,83(5):723-744.[doi:10.1016/j.jss.2009.11.709]
    [7] Clarke E, Grumberg O, Peled D. Model Checking. Cambridge:MIT Press, 2000.
    [8] Xu HZ, Zeng GS. Dynamic evolution of software architectures based on hypergraph grammars. Journal of Tongji University (Natural Science), 2011,39(5):745-750(in Chinese with English abstract).[doi:10.3969/j.issn.0253-374x.2011.05.021]
    [9] Xu HZ, Zeng GS, Chen B. Conditional hypergraph grammars and its analysis of dynamic evolution of software architectures. Ruan Jian Xue Bao/Journal of Software, 2011,22(6):1210-1223(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4017.htm[doi:10.3724/SP.J.1001.2011.04017]
    [10] Xu HZ, Zeng GS. Modeling and verifying composite dynamic evolution of software architectures using hypergraph grammars. Int'l Journal of Software Engineering and Knowledge Engineering, 2013,23(6):775-799.[doi:10.1142/S0218194013500204]
    [11] Börger E. The ASM refinement method. Formal Aspects of Computing, 2003,15(2-3):237-257.[doi:10.1007/s00165-003-0012-7]
    [12] Oquendo F. π-ADL:An architecture description language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures. ACM Sigsoft Software Engineering Notes, 2004,29(3):1-14.[doi:10.1145/986710.986728]
    [13] Mei H, Chen F, Wang QX, Feng YD. ABC/ADL:An ADL supporting component composition. LNCS, 2002,2495:38-47.[doi:10.1007/3-540-36103-0_6]
    [14] Kacem MH, Kacem AH, Jmaiel M, Drira K. Describing dynamic software architectures using an extended UML model. In:Proc. of the Symp. on Applied Computing. New York:ACM Press, 2006.1245-1249.[doi:10.1145/1141277.1141569]
    [15] Bruni R, Bucchiarone A, Gnesi S, Melgratti H. Modelling dynamic software architectures using typed graph grammars. Electronic Notes in Theoretical Computer Science, 2008,213(1):39-53.[doi:10.1016/j.entcs.2008.04.073]
    [16] Ma XX, Cao C, Yu P, Zhou Y. A supporting environment based on graph grammar for dynamic software architectures. Ruan Jian Xue Bao/Journal of Software, 2008,19(8):1881-1892(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/19/1881.htm[doi:10.3724/SP.J.1001.2008.01881]
    [17] Chang ZM, Mao XJ, Qi ZC. Applying bigraph theory to self-adaptive software architecture. Chinese Journal of Computers, 2009, 32(1):97-106(in Chinese with English abstract).[doi:10.3724/SP.J. 1016.2009.00097]
    [18] Dormoy J, Kouchnarenko O, Lanoix A. Using temporal logic for dynamic reconfigurations of components. LNCS, 2012,6921:200-217.[doi:10.1007/978-3-642-27269-1_12]
    [19] Fiadeiro JL, Lopes A. A model for dynamic reconfiguration in service-oriented architectures. Software & Systems Modeling, 2013, 12(2):349-367.[doi:10.1007/s10270-012-0236-1]
    [20] Pelliccione P, Inverardi P, Muccini H. CHARMY:A framework for designing and verifying architectural specifications. IEEE Trans. on Software Engineering, 2009,35(3):325-346.[doi:10.1109/TSE.2008.104]
    [21] Lanoix A, Dormoy J, Kouchnarenko O. Combining proof and model-checking to validate reconfigurable architectures. Electronic Notes in Theoretical Computer Science, 2011279(2):43-57.[doi:10.1016/j.entcs.2011.11.011]
    [22] Eckardt T, Heinzemann C, Henkler S, Hirsch M, Priesterjahn C, Schäfer W. Modeling and verifying dynamic communication structures based on graph transformations. Computer Science-Research and Development, 2013,28(1):3-22.[doi:10.1007/s00450-011-0184-y]
    [23] Rensink A. The GROOVE simulator:A tool for state space generation. LNCS, 2004,3062:479-485.[doi:10.1007/978-3-540-25959-6_40]
    [24] Hermann F, Kastenberg H, Modica1 T. Towards translating graph transformation approaches by model transformations. Electronic Communications of the EASST, 2006. http://journal.ub.tu-berlin.de/eceasst/article/view/20
    [25] Lin HM, Zhang WH. Model checking:Theories, techniques and applications. Acta Electronica Sinica, 2002,30(S1):1907-1912(in Chinese with English abstract). http://www.ejournal.org.cn/CN/Y2002/V30/IS1/1907
    [26] Baier C, Katoen JP. Principles of Model Checking. Cambridge:MIT Press, 2008.
    [27] Holzmann G. The model checker SPIN. IEEE Trans. on Software Engineering, 1997,23(5):279-295.[doi:10.1109/32.588521]
    附中文参考文献:
    [8] 徐洪珍,曾国荪.基于超图文法的软件体系结构动态演化.同济大学学报(自然科学版),2011,39(5):45-750.[doi:10.3969/j.issn. 0253-374x.2011.05.021]
    [9] 徐洪珍,曾国荪,陈波.软件体系结构动态演化的条件超图文法及分析.软件学报,2011,22(6):1210-1223. http://www.jos.org.cn/1000-9825/4017.htm[doi:10.3724/SP.J.1001.2011.04017]
    [16] 马晓星,曹春,余萍,周宇.基于图文法的动态软件体系结构支撑环境.软件学报,2008,19(8):1881-1892. http://www.jos.org.cn/1000-9825/19/1881.htm[doi:10.3724/SP.J.1001.2008.01881]
    [17] 常志明,毛新军,齐治昌.Bigraph理论在自适应软件体系结构上的应用.计算机学报,2009,32(1):97-106.[doi:10.3724/SP.J.1016.2009.00097]
    [25] 林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(S1):1907-1912. http://www.ejournal.org.cn/CN/Y2002/V30/IS1/1907
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2014-08-18
  • 最后修改日期:2014-11-24
  • 在线发布日期: 2016-07-07
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19791893位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号