{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T16:07:15Z","timestamp":1778947635302,"version":"3.51.4"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,1,21]],"date-time":"2016-01-21T00:00:00Z","timestamp":1453334400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s11432-015-5332-8","type":"journal-article","created":{"date-parts":[[2016,1,23]],"date-time":"2016-01-23T01:40:42Z","timestamp":1453513242000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Model based verification of dynamically evolvable service oriented systems","\u57fa\u4e8e\u6a21\u578b\u7684\u52a8\u6001\u53ef\u6f14\u5316\u9762\u5411\u670d\u52a1\u67b6\u6784\u9a8c\u8bc1\u65b9\u6cd5"],"prefix":"10.1007","volume":"59","author":[{"given":"Yu","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jidong","family":"Ge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pengcheng","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weigang","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,21]]},"reference":[{"key":"5332_CR1","doi-asserted-by":"crossref","first-page":"610","DOI":"10.1007\/s11432-008-0051-z","volume":"51","author":"F Yang","year":"2008","unstructured":"Yang F, L\u00fc J, Mei H. Technical framework for Internetware: an architecture centric approach. Sci China Ser-F: Inf Sci, 2008, 51: 610\u2013622","journal-title":"Sci China Ser-F: Inf Sci"},{"key":"5332_CR2","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1360\/N112014-00009","volume":"44","author":"H Wang","year":"2014","unstructured":"Wang H, Wu W, Mao X, et al. Growing construction and adaptive evolution of complex software system (in Chinese). Sci Sin Inform, 2014, 44: 743\u2013761","journal-title":"Sci Sin Inform"},{"key":"5332_CR3","doi-asserted-by":"crossref","first-page":"2716","DOI":"10.3724\/SP.J.1001.2011.03923","volume":"22","author":"J M Fu","year":"2011","unstructured":"Fu J M, Tao F, Wang D, et al. Software behavior model based on system objects. J Softw, 2011, 22: 2716\u20132728","journal-title":"J Softw"},{"key":"5332_CR4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1002\/smr.324","volume":"18","author":"Q X Wang","year":"2006","unstructured":"Wang Q X, Shen J R, Wang X, et al. A component-based approach to online software evolution. J Softw Maint Evol-Res Pract, 2006, 18: 181\u2013205","journal-title":"J Softw Maint Evol-Res Pract"},{"key":"5332_CR5","first-page":"899","volume-title":"In: Companion of the 30th International Conference on Software Engineering, Leipzig","author":"P Oreizy","year":"2008","unstructured":"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\u2013910"},{"key":"5332_CR6","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1007\/s11432-008-0057-6","volume":"51","author":"J L\u00fc","year":"2008","unstructured":"L\u00fc J, Ma X X, Tao X P, et al. On environment-driven software model for Internetware. Sci China Ser-F: Inf Sci, 2008, 51: 683\u2013721","journal-title":"Sci China Ser-F: Inf Sci"},{"key":"5332_CR7","first-page":"840","volume-title":"In: Proceedings of 1st International Conference on Availability, Reliability and Security, Vienna","author":"R Kazhamiakin","year":"2006","unstructured":"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\u2013846"},{"key":"5332_CR8","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D. A theory of timed automata. Theor Comput Sci, 1994, 126: 183\u2013235","journal-title":"Theor Comput Sci"},{"key":"5332_CR9","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R Calinescu","year":"2012","unstructured":"Calinescu R, Ghezzi C, Kwiatkowska M, et al. Self-adaptive software needs quantitative verification at runtime. Commun ACM, 2012, 55: 69\u201377","journal-title":"Commun ACM"},{"key":"5332_CR10","doi-asserted-by":"crossref","first-page":"844","DOI":"10.1109\/TSE.2008.52","volume":"34","author":"J S Dong","year":"2008","unstructured":"Dong J S, Hao P, Qin S C, et al. Timed automata patterns. IEEE Trans Softw Eng, 2008, 34: 844\u2013859","journal-title":"IEEE Trans Softw Eng"},{"key":"5332_CR11","first-page":"144","volume-title":"Proceedings of the International Conference on Software and System Process, Nanjing","author":"Y Zhou","year":"2014","unstructured":"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\u2013148"},{"key":"5332_CR12","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1360\/112011-925","volume":"42","author":"W Song","year":"2012","unstructured":"Song W, Tang J H, Zhang G X, et al. Substitutability analysis of WS-BPEL services (in Chinese). Sci Sin Inform, 2012, 42: 264\u2013279","journal-title":"Sci Sin Inform"},{"key":"5332_CR13","doi-asserted-by":"crossref","first-page":"261","DOI":"10.3724\/SP.J.1001.2010.03735","volume":"21","author":"J Zeng","year":"2010","unstructured":"Zeng J, Sun H L, Liu X D, et al. Dynamic evolution mechanism for trustworthy software based on service composition. J Softw, 2010, 21: 261\u2013276","journal-title":"J Softw"},{"key":"5332_CR14","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/s00607-014-0396-7","volume":"96","author":"Y Zhou","year":"2014","unstructured":"Zhou Y, Ma X X, Gall H. A middleware platform for the dynamic evolution of distributed component-based systems. Computing, 2014, 96: 725\u2013747","journal-title":"Computing"},{"key":"5332_CR15","first-page":"187","volume-title":"Proceedings of 6th International Conference on Quantitative Evaluation of Systems, Budapest","author":"A Hartmanns","year":"2009","unstructured":"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\u2013196"},{"key":"5332_CR16","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Proceedings of First International Conference on Runtime Verification, St. Julians","author":"A Legay","year":"2010","unstructured":"Legay A, Delahaye B, Bensalem S. Statistical model checking: an overview. In: Proceedings of First International Conference on Runtime Verification, St. Julians, 2010. 122\u2013135"},{"key":"5332_CR17","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1109\/MC.2006.362","volume":"39","author":"L Baresi","year":"2006","unstructured":"Baresi L, Di Nitto E, Ghezzi C. Toward open-world software: issue and challenges. Computer, 2006, 39: 36\u201343","journal-title":"Computer"},{"key":"5332_CR18","doi-asserted-by":"crossref","first-page":"1293","DOI":"10.1109\/32.60317","volume":"16","author":"J Kramer","year":"1990","unstructured":"Kramer J, Magee J. The evolving philosophers problem: dynamic change management. IEEE Trans Softw Eng, 1990, 16: 1293\u20131306","journal-title":"IEEE Trans Softw Eng"},{"key":"5332_CR19","doi-asserted-by":"crossref","first-page":"856","DOI":"10.1109\/TSE.2007.70733","volume":"33","author":"Y Vandewoude","year":"2007","unstructured":"Vandewoude Y, Ebraert P, Berbers Y, et al. Tranquility: a low disruptive alternative to quiescence for ensuring safe dynamic updates. IEEE Trans Softw Eng, 2007, 33: 856\u2013868","journal-title":"IEEE Trans Softw Eng"},{"key":"5332_CR20","first-page":"111","volume-title":"Proceedings of 31st International Conference on Software Engineering, Vancouver","author":"I Epifani","year":"2009","unstructured":"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\u2013121"},{"key":"5332_CR21","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Proceedings of Formal Methods for the Design of Real-Time Systems, Bertinoro","author":"G Behrmann","year":"2004","unstructured":"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\u2013236"},{"key":"5332_CR22","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David A, Larsen K, Legay A, et al. Uppaal SMC tutorial. Int J Softw Tools Technol Transfer, 2015, 17: 397\u2013415","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"5332_CR23","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/s11390-013-1322-8","volume":"28","author":"Y Zhou","year":"2013","unstructured":"Zhou Y, Baresi L, Rossi M. Towards a formal semantics for UML\/MARTE state machines based on hierarchical timed automata. J Comput Sci Technol, 2013, 28: 188\u2013202","journal-title":"J Comput Sci Technol"},{"key":"5332_CR24","volume-title":"Communicating and Mobile Systems: the Pi Calculus","author":"R Milner","year":"1999","unstructured":"Milner R. Communicating and Mobile Systems: the Pi Calculus. Cambridge: Cambridge University Press, 1999"},{"key":"5332_CR25","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/11561163_8","volume-title":"Proceedings of International Symposium on Formal Methods for Components and Objects, Amsterdam","author":"G Behrmann","year":"2005","unstructured":"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\u2013182"},{"key":"5332_CR26","unstructured":"OMG. Specification. Unified Modeling Language: Superstructure Version 2.2. OMG Formal Document, 2009"},{"key":"5332_CR27","first-page":"159","volume-title":"Proceedings of the International Conference on Service-Oriented Computing, Stockholm","author":"L Cavallaro","year":"2009","unstructured":"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\u2013174"},{"key":"5332_CR28","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1360\/03yf0192","volume":"47","author":"G Huang","year":"2004","unstructured":"Huang G, Mei H, Yang F Q. Runtime software architecture based on reflective middleware. Sci China Ser-F: Inf Sci, 2004, 47: 555\u2013576","journal-title":"Sci China Ser-F: Inf Sci"},{"key":"5332_CR29","first-page":"2","volume-title":"Proceedings of International Conference on Software Engineering and Knowledge Engineering, Boston","author":"X X Ma","year":"2007","unstructured":"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\u20138"},{"key":"5332_CR30","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1109\/TSE.2010.39","volume":"37","author":"L Baresi","year":"2011","unstructured":"Baresi L, Ghezzi C, Mottola L. Loupe: verifying publish-subscribe architectures with a magnifying lens. IEEE Trans Softw Eng, 2011, 37: 228\u2013246","journal-title":"IEEE Trans Softw Eng"},{"key":"5332_CR31","doi-asserted-by":"crossref","first-page":"679","DOI":"10.1109\/TSE.2010.79","volume":"37","author":"H B Chen","year":"2011","unstructured":"Chen H B, Yu J, Hang C Q, et al. Dynamic software updating using a relaxed consistency model. IEEE Trans Softw Eng, 2011, 37: 679\u2013694","journal-title":"IEEE Trans Softw Eng"},{"key":"5332_CR32","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/978-3-642-27705-4_22","volume-title":"Proceedings of International Confernece on Verified Software: Theories, Tools, Experiments","author":"C Hayden","year":"2012","unstructured":"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\u2013293"},{"key":"5332_CR33","first-page":"371","volume-title":"Proceedings of 28th International Conference on Software Engineering, Shanghai","author":"J Zhang","year":"2006","unstructured":"Zhang J, Cheng B. Model-based development of dynamically adaptive software. In: Proceedings of 28th International Conference on Software Engineering, Shanghai, 2006. 371\u2013380"},{"key":"5332_CR34","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1049\/iet-sen.2012.0047","volume":"7","author":"P C Zhang","year":"2013","unstructured":"Zhang P C, Leung H, Li W R, et al. Web services property sequence chart monitor: a tool chain for monitoring BPEL-based web service composition with scenario-based specifications. IET Softw, 2013, 7: 222\u2013248","journal-title":"IET Softw"},{"key":"5332_CR35","doi-asserted-by":"crossref","first-page":"2694","DOI":"10.1007\/s11432-012-4742-0","volume":"55","author":"A David","year":"2012","unstructured":"David A, Du D, Larsen K, et al. An evaluation framework for energy aware buildings using statistical model checking. Sci China Inf Sci, 2012, 55: 2694\u20132707","journal-title":"Sci China Inf Sci"},{"key":"5332_CR36","first-page":"082105","volume":"56","author":"C Xu","year":"2013","unstructured":"Xu C, Liu Y P, Cheung S C, et al. Towards context consistnecy by concurrent checking for Internetware applications. Sci China Inf Sci, 2013, 56: 082105","journal-title":"Sci China Inf Sci"},{"key":"5332_CR37","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1109\/TSE.2010.92","volume":"37","author":"R Calinescu","year":"2011","unstructured":"Calinescu R, Grunske L, Kwiatkowska M, et al. Dynamic QoS management and optimization in service-based systems. IEEE Trans Softw Eng, 2011, 37: 387\u2013409","journal-title":"IEEE Trans Softw Eng"},{"key":"5332_CR38","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1016\/j.jvlc.2005.11.001","volume":"17","author":"K H\u00f6lscher","year":"2006","unstructured":"H\u00f6lscher K, Ziemann P, Gogolla M. On translating UML models into graph transformation systems. J Vis Lang Comput, 2006, 17: 78\u2013105","journal-title":"J Vis Lang Comput"},{"key":"5332_CR39","doi-asserted-by":"crossref","first-page":"1210","DOI":"10.3724\/SP.J.1001.2011.04017","volume":"22","author":"H Z Xu","year":"2011","unstructured":"Xu H Z, Zeng G S, Chen B. Conditional hypergraph grammars and its analysis of dynamic evolution of software architectures. J Softw, 2011, 22: 1210\u20131223","journal-title":"J Softw"},{"key":"5332_CR40","first-page":"245","volume-title":"Proceedings of 19th Symposium on Foundations of Software Engineering, Hungary","author":"X X Ma","year":"2011","unstructured":"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\u2013255"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-015-5332-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-015-5332-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-015-5332-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T23:17:25Z","timestamp":1567552645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-015-5332-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,21]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["5332"],"URL":"https:\/\/doi.org\/10.1007\/s11432-015-5332-8","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,21]]},"article-number":"32101"}}