College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China;State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210093, China 在期刊界中查找 在百度中查找 在本站中查找
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, etal. 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]
[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]