一种开放环境下软件在线演化一致性验证方法
作者:
基金项目:

国家自然科学基金(61202002, 61272083, 61379157); 江苏省软件新技术与产业化协同创新中心计划


Towards an Approach of Consistency Verification for Online Software Evolution in Open Environments
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [34]
  • |
  • 相似文献 [20]
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    一致性保障技术是开放环境下软件在线演化研究的热点问题.区别于传统的基于图文法或基于体系结构描述语言(architectural description language,简称ADL)对结构演化进行分析的途径,提出一种从行为角度采用层次式时间自动机对软件在线演化进行分析的方法,可支持对软件的时间属性、层次特征等直接建模.提出了层次平展化算法,将层次模型等价地转化为若干并行时间自动机模型,从而可应用现有模型检测工具针对演化规约进行一致性验证,并通过实验验证了所提方法的有效性.

    Abstract:

    Consistency assurance mechanism is of particular importance for online software evolution. Different from traditional approaches based on attributed graph grammar or architectural description languages, the paper investigates the problem from the behavioral perspective and proposes a novel verification technique based on hierarchical timed automata. The approach can directly support the modeling of temporal aspects as well as the hierarchical organization of composed systems in open environments. To make it feasible for consistency verification, this paper also proposes a flattening algorithm, translating the model into a set of synchronized serial timed automata so as to be fed into third-party tool-set. An example is presented throughout the paper to illustrate the new method. Experiments are carried out to complement the discussion and demonstrate the feasibility of the proposed approach.

    参考文献
    [1] Lü J, Ma XX, Tao XP, Xu F, Hu H. Research and progress on Internetware. Science in China (Series E), 2006,36(10):1037-1080 (in Chinese with English abstract).
    [2] Frieder O, Segal ME. On dynamically updating a computer program: From concept to prototype. Journal of Systems and Software, 1991,14(2):111-128.[doi: 10.1016/0164-1212(91)90096-O]
    [3] Orso A, Rao A, Harrold MJ. A technique for dynamic updating of Java software. In: Proc. of the Int'l Conf. on Software Maintenance. IEEE, 2002. 649-658.[doi: 10.1109/ICSM.2002.1167829]
    [4] Hicks M, Nettles S. Dynamic software updating. ACM Trans. on Programming Languages and Systems (TOPLAS), 2005,27(6): 1049-1096.[doi: 10.1145/1108970.1108971]
    [5] Stoyle G, Hicks M, Bierman G, Sewell P, Neamtiu I. Mutatis mutandis: Safe and flexible dynamic software updating. ACM Trans. on Programming Languages and Systems, 2007,29(4):1-70.[doi: 10.1145/1255450.1255455]
    [6] Huang G, Mei H, Yang FQ. Runtime software architecture based on reflective middleware. Science in China (Series E), 2004,34(2): 121-138 (in Chinese with English abstract).
    [7] Yu P, Ma XX, Lü J, Tao XP. A dynamic software architecture oriented approach to online evolution. Ruan Jian Xue Bao/Journal of Software, 2006,17(6):1360-1371 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/1360.htm
    [8] Oreizy P, Medvidovic N, Taylor R. Runtime software adaptation: Framework, approaches, and styles. In: Proc. of the 30th Int'l Conf. on Software Engineering. ACM Press, 2008. 899-910.[doi: 10.1145/1370175.1370181]
    [9] Xu HZ, Zeng GS, Chen B. Conditional hypergraph grammars and its analysis of dynamic evolution of software architecture. 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] Zeng J, Sun HL, Liu XD, Deng T, Huai JP. Dynamic evolution mechanism for trustworthy software based on service composition. Ruan Jian Xue Bao/Journal of Software, 2010, 21(2):261-276 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3735.htm[doi: 10.3724/SP.J.1001.2010.03735]
    [11] Kazhamiakin R, Pandya P, Pistore M. Timed modelling and analysis in web service compositions. In: Proc. of the 1st Int'l Conf. on Availability, Reliability and Security (ARES 2006). IEEE, 2006. 7.[doi: 10.1109/ARES.2006.134]
    [12] De Lemos R, Giese H, Müller HA, et al. Software engineering for self-adaptive systems: A second research roadmap. In: Proc. of the Software Engineering for Self-Adaptive Systems II. Berlin, Heidelberg: Springer-Verlag, 2013. 1-32.[doi: 10.1007/978-3-642-35813-5_1]
    [13] Zhou Y, Ge JD, Zhang PC. Hierarchical timed automata based verification of dynamic evolution process in open environments. In: Proc. of the Int'l Conf. on Software and Systems Process (ICSSP). 2014. 144-148.[doi: 10.1145/2600821.2600838]
    [14] Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.[doi: 10.1016/0304-3975(94) 90010-8]
    [15] Safra S. On the comlexity of w automata. In: Proc. of the 29th Foundations of Computer Science. IEEE, 1988.[doi: 10.1109/SFCS. 1988.21948]
    [16] Li LX, Jin Z, Li G. Modeling and verifying services of internet of things based on timed automata. Chinese Journal of Computers, 2011,34(8):1365-1377 (in Chinese with English abstract).[doi: 10.3724/SP.J.1016.2011.01365]
    [17] Chen W, Xue YZ, Zhao C, Li MS. A method for testing real-time system based on timed automata. Ruan Jian Xue Bao/Journal of Software, 2007,18(1):62-73 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/18/62.htm
    [18] Zhou Y, Baresi L, Rossi M. Towards a formal semantics for UML/MARTE state machines based on hierarchical timed automata. Journal of Computer Science and Technology, 2013,28(1):188-202.[doi: 10.1007/s11390-013-1322-8]
    [19] Kramer J, Magee J. The evolving philosophers problem: Dynamic change management. IEEE Trans. on Software Engineering, 1990,16(11):1293-1306.[doi: 10.1109/32.60317]
    [20] Vandewoude Y, Ebraert P, Berbers Y, D'Hondt T. Tranquility: A low disruptive alternative to quiescence for ensuring safe dynamic updates. IEEE Trans. on Software Engineering, 2007,33(12):856-868.[doi: 10.1109/TSE.2007.70733]
    [21] Behrmann G, David A, Larsen KG, Häkansson J, Pettersson P, Wang Y, Hendriks M. UPPAAL 4.0. In: Proc. of the 3rd Int'l Conf. on Quantitative Evaluation of Systems (QEST 2006). IEEE, 2006. 125-126.[doi: 10.1109/QEST.2006.59]
    [22] Alpern B, Schneider FB. Recognizing safety and liveness. Distributed Computing, 1987,2(3):117-126.[doi: 10.1007/BF01782772]
    [23] Liu Y, Zhang YC, Zhang B, Zhang MW, Zhu ZL. Analysis of service replaceability on behavior effect. Journal of Computer Research and Development, 2010,47(8):1442-1449 (in Chinese with English abstract).
    [24] Song W, Tang JH, Zhang GX, Ma XX. WS-BPEL service repalceability anlayisis. Science in China (Information Science), 2012, 42(3):264-279 (in Chinese with English abstract).
    [25] Zhang J, Cheng BHC. Model-Based development of dynamically adaptive software. In: Proc. of the 28th Int'l Conf. on Software Engineering. ACM Press, 2006. 371-380.[doi: 10.1145/1134285.1134337]
    [26] Hayden CM, Magill S, Hicks M, Foster N, Foster JS. Specifying and verifying the correctness of dynamic software updates. In: Proc. of the Verified Software: Theories, Tools, Experiments. Berlin, Heidelberg: Springer-Verlag, 2012. 278-293.[doi: 10.1007/978-3-642-27705-4_22]
    [27] Baresi L, Ghezzi C, Mottola L. On accurate automatic verification of publish-subscribe architectures. In: Proc. of the 29th Int'l Conf. on Software Engineering. 2007. 199-208.[doi: 10.1109/ICSE.2007.57]
    [28] Baresi L, Ghezzi C, Mottola L. Loupe: Verifying publish-subscribe architectures with a magnifying lens. IEEE Trans. on Software Engineering, 2011,37(2):228-246.[doi: 10.1109/TSE.2010.39]
    [29] Chen HB, Yu J, Hang CQ, Zang BY, Yew PC. Dynamic software updating using a relaxed consistency model. IEEE Trans. on Software Engineering. 2011,27(5):679-694.[doi: 10.1109/TSE.2010.79]
    [30] Zhou Y. A runtime architecture-based approach for the dynamic evolution of distributed component-based systems. In: Proc. of the 30th Int'l Conf. on Software Engineering. ACM Press, 2008. 979-982.[doi: 10.1145/1370175.1370217]
    [31] Garlan D, Khersonsky S, Kim J. Model checking publish-subscribe systems. In: Proc. of the 10th Int'l SPIN Workshop. LNCS, Springer-Verlag, 2002. 166-180.[doi: 10.1007/3-540-44829-2_11]
    [32] Calinescu R, Ghezzi C, Kwiatkowska M, Mirandola R. Self-Adaptive software needs quantitative verification at runtime. Communications of the ACM, 2012,55(9):69-77.[doi: 10.1145/2330667.2330686]
    [33] Wang HM, Shi PC, Ding B, Yin G, Shi DX. Online evolution of software services. Chinese Journal of Computers, 2011,34(2): 318-328 (in Chinese with English abstract).
    [34] Ma XX, Baresi L, Ghezzi C, Panzica V, Manna L, Lü J. Version-Consistent dynamic reconfiguration of component-based distributed systems. In: Proc. of the 19th ACM SIGSOFT Symp. and the 13th European Conf. on Foundations of Software Engineering. ACM Press, 2011. 245-255.[doi: 10.1145/2025113.2025148]
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

周宇,黄延凯,黄志球,吴维刚.一种开放环境下软件在线演化一致性验证方法.软件学报,2015,26(4):747-759

复制
分享
文章指标
  • 点击次数:5210
  • 下载次数: 6905
  • HTML阅读次数: 2347
  • 引用次数: 0
历史
  • 收稿日期:2014-06-29
  • 最后修改日期:2014-10-14
  • 在线发布日期: 2015-04-02
文章二维码
您是第19830950位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号