logo

SCIENCE CHINA Information Sciences, Volume 59, Issue 3: 032101(2016) https://doi.org/10.1007/s11432-015-5332-8

Model based verification of dynamically evolvable service oriented systems

More info
  • ReceivedOct 20, 2015
  • AcceptedDec 2, 2015
  • PublishedJan 21, 2016

Abstract

Dynamic evolution is highly desirable for service oriented systems in open environments. For the evolution to be trusted, it is crucial to keep the process consistent with the specification. In this paper, we study two kinds of evolution scenarios and propose a novel verification approach based on hierarchical timed automata to model check the underlying consistency with the specification. It examines the procedures before, during and after the evolution process, respectively and can support the direct modeling of temporal aspects, as well as the hierarchical decomposition of software structures. Probabilities are introduced to model the uncertainty characterized in open environments and thus can support the verification of parameter-level evolution. We present a flattening algorithm to facilitate automated verification using the mainstream timed automata based model checker --UPPAAL (integrated with UPPAAL-SMC). We also provide a motivating example with performance evaluation that complements the discussion and demonstrates the feasibility of our approach.


Acknowledgment

Acknowledgments

This work was partially funded by national Natural Science Foundation of China (Grant Nos. 61202002, 61202097, 61379157), collaborative Innovation Center of Novel Software Technology and Industrialization, chinese Fundamental Research Funds for the Central Universities (Grant No. NZ2013306), national Basic Research Program of China (973 Program) (Grant No. 2014CB744905), and Natural Science Foundation of Jiangsu Province (Grant No. BK20131277). the authors would like to thank Prof. Zining CAO, Dr. Taolue CHEN, Prof. Dehui DU, Jiayi GU, and Yankai HUANG for their help with the work.


References

[1] Yang F, Lü J, Mei H. Sci China Ser-F: Inf Sci, 2008, 51: 610-622 CrossRef Google Scholar

[2] Wang H, Wu W, Mao X, et al. Sci Sin Inform, 2014, 44: 743-761 Google Scholar

[3] Fu J M, Tao F, Wang D, et al. J Softw, 2011, 22: 2716-2728 CrossRef Google Scholar

[4] Wang Q X, Shen J R, Wang X, et al. J Softw Maint Evol-Res Pract, 2006, 18: 181-205 CrossRef Google Scholar

[5] Oreizy P, Medvidovic N, Taylor R. Runtime software adaptation: framework, approaches, and styles. In: Companion of the 30th International Conference on Software Engineering, Leipzig, 2008. 899--910. Google Scholar

[6] L{ü} J, Ma X X, Tao X P, et al. Sci China Ser-F: Inf Sci, 2008, 51: 683-721 CrossRef Google Scholar

[7] Kazhamiakin R, Pandya P, Pistore M. Timed modelling and analysis in web service compositions. In: Proceedings of 1st International Conference on Availability, Reliability and Security, Vienna, 2006. 840--846. Google Scholar

[8] Alur R, Dill D. Theor Comput Sci, 1994, 126: 183-235 CrossRef Google Scholar

[9] Calinescu R, Ghezzi C, Kwiatkowska M, et al. Commun ACM, 2012, 55: 69-77 Google Scholar

[10] Dong J S, Hao P, Qin S C, et al. IEEE Trans Softw Eng, 2008, 34: 844-859 CrossRef Google Scholar

[11] Zhou Y, Ge J D, Zhang P C. Hierarchical timed automata based verification of dynamic evolution process in open environments. In: Proceedings of the International Conference on Software and System Process, Nanjing, 2014. 144--148. Google Scholar

[12] Song W, Tang J H, Zhang G X, et al. Sci Sin Inform, 2012, 42: 264-279 Google Scholar

[13] Zeng J, Sun H L, Liu X D, et al. J Softw, 2010, 21: 261-276 CrossRef Google Scholar

[14] Zhou Y, Ma X X, Gall H. Computing, 2014, 96: 725-747 Google Scholar

[15] Hartmanns A, Hermanns H. A modest approach to checking probabilistic timed automata. In: Proceedings of 6th International Conference on Quantitative Evaluation of Systems, Budapest, 2009. 187--196. Google Scholar

[16] Legay A, Delahaye B, Bensalem S. Statistical model checking: an overview. In: Proceedings of First International Conference on Runtime Verification, St. Julians, 2010. 122--135. Google Scholar

[17] Baresi L, Di~Nitto E, Ghezzi C. Computer, 2006, 39: 36-43 Google Scholar

[18] Kramer J, Magee J. IEEE Trans Softw Eng, 1990, 16: 1293-1306 CrossRef Google Scholar

[19] Vandewoude Y, Ebraert P, Berbers Y, et al. IEEE Trans Softw Eng, 2007, 33: 856-868 CrossRef Google Scholar

[20] Epifani I, Ghezzi C, Mirandola R, et al. Model evolution by run-time parameter adaptation. In: Proceedings of 31st International Conference on Software Engineering, Vancouver, 2009. 111--121. Google Scholar

[21] Behrmann G, David A, Larsen K. A tutorial on Uppaal. In: Proceedings of Formal Methods for the Design of Real-Time Systems, Bertinoro, 2004. 200--236. Google Scholar

[22] David A, Larsen K, Legay A, et al. Int J Softw Tools Technol Transfer, 2015, 17: 397-415 CrossRef Google Scholar

[23] Zhou Y, Baresi L, Rossi M. J Comput Sci Technol, 2013, 28: 188-202 CrossRef Google Scholar

[24] Milner R. Communicating and Mobile Systems: the Pi Calculus. Cambridge: Cambridge University Press, 1999. Google Scholar

[25] Behrmann G, Larsen K, Rasmussen J. Priced timed automata: algorithms and applications. In: Proceedings of International Symposium on Formal Methods for Components and Objects, Amsterdam, 2005. 162--182. Google Scholar

[26] OMG. {Specification. Unified Modeling Language: Superstructure Version 2.2}. OMG Formal Document, 2009. Google Scholar

[27] Cavallaro L, Di~Nitto E, Pradella M. An automatic approach to enable replacement of conversational services. In: Proceedings of the International Conference on Service-Oriented Computing, Stockholm, 2009. 159--174. Google Scholar

[28] Huang G, Mei H, Yang F Q. Sci China Ser-F: Inf Sci, 2004, 47: 555-576 CrossRef Google Scholar

[29] Ma X X, Zhou Y, Pan J, et al. Constructing self-adaptive systems with polymorphic software architecture. In: Proceedings of International Conference on Software Engineering and Knowledge Engineering, Boston, 2007. 2--8. Google Scholar

[30] Baresi L, Ghezzi C, Mottola L. IEEE Trans Softw Eng, 2011, 37: 228-246 CrossRef Google Scholar

[31] Chen H B, Yu J, Hang C Q, et al. IEEE Trans Softw Eng, 2011, 37: 679-694 CrossRef Google Scholar

[32] Hayden C, Magill S, Hicks M, et al. Specifying and verifying the correctness of dynamic software updates. In: Proceedings of International Confernece on Verified Software: Theories, Tools, Experiments. Berlin: Springer, 2012. 278--293. Google Scholar

[33] Zhang J, Cheng B. Model-based development of dynamically adaptive software. In: Proceedings of 28th International Conference on Software Engineering, Shanghai, 2006. 371--380. Google Scholar

[34] Zhang P C, Leung H, Li W R, et al. IET Softw, 2013, 7: 222-248 CrossRef Google Scholar

[35] David A, Du D, Larsen K, et al. Sci China Inf Sci, 2012, 55: 2694-2707 CrossRef Google Scholar

[36] Xu C, Liu Y P, Cheung S C, et al. Sci China Inf Sci, 2013, 56: 082105-2707 Google Scholar

[37] Calinescu R, Grunske L, Kwiatkowska M, et al. IEEE Trans Softw Eng, 2011, 37: 387-409 CrossRef Google Scholar

[38] Hölscher K, Ziemann P, Gogolla M. J Vis Lang Comput, 2006, 17: 78-105 CrossRef Google Scholar

[39] Xu H Z, Zeng G S, Chen B. J Softw, 2011, 22: 1210-1223 CrossRef Google Scholar

[40] Ma X X, Baresi L, Ghezzi C, et al. Version-consistent dynamic reconfiguration of component-based distributed systems. In: Proceedings of 19th Symposium on Foundations of Software Engineering, Hungary, 2011. 245--255. Google Scholar

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1       京公网安备11010102003388号