{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:17:32Z","timestamp":1760044652431},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540878780"},{"type":"electronic","value":"9783540878797"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87879-7_8","type":"book-chapter","created":{"date-parts":[[2008,10,8]],"date-time":"2008-10-08T22:23:08Z","timestamp":1223504588000},"page":"119-134","source":"Crossref","is-referenced-by-count":47,"title":["Quality Prediction of Service Compositions through Probabilistic Model Checking"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Gallotti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo","family":"Ghezzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raffaela","family":"Mirandola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giordano","family":"Tamburrelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Wosp : Proceedings of the international workshop on software and performance, (1998-2007)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/11563228_3","volume-title":"SAFECOMP","author":"N. Addouche","year":"2005","unstructured":"Addouche, N., Antoine, C., Montmain, J.: Combining extended uml models and formal methods to analyze real-time systems. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol.\u00a03688. pp. 24\u201336. Springer, Heidelberg (2005)"},{"issue":"1","key":"8_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design: An International Journal\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"8_CR4","unstructured":"Alves, A.: et\u00a0al. Web service business process execution language version 2.0. Committee Draft, 17 (May 2006)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Ardagna, D., Pernici, B.: Global and Local QoS Guarantee in Web Service Selection. In: Proc. of Business Process Management Workshops, pp. 32\u201346 (2005)","DOI":"10.1109\/ICWS.2005.66"},{"issue":"5","key":"8_CR6","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/MS.2003.1231149","volume":"20","author":"C. Atkinson","year":"2003","unstructured":"Atkinson, C., Kuhne, T.: Model-driven development: A metamodeling foundation. IEEE Software\u00a020(5), 36\u201341 (2003)","journal-title":"IEEE Software"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"issue":"5","key":"8_CR8","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1109\/TSE.2004.9","volume":"30","author":"S. Balsamo","year":"2004","unstructured":"Balsamo, S., Di Marco, A., Inverardi, P., Simeoni, M.: Model-based performance prediction in software development: A survey. IEEE Trans. Software Eng.\u00a030(5), 295\u2013310 (2004)","journal-title":"IEEE Trans. Software Eng."},{"issue":"6","key":"8_CR9","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1049\/iet-sen:20070027","volume":"1","author":"L. Baresi","year":"2007","unstructured":"Baresi, L., Bianculli, D., Ghezzi, C., Guinea, S., Spoletini, P.: Validation of web service compositions. IET Software\u00a01(6), 219\u2013232 (2007)","journal-title":"IET Software"},{"key":"8_CR10","first-page":"55","volume-title":"SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems","author":"L. Baresi","year":"2007","unstructured":"Baresi, L., Gerosa, G., Ghezzi, C., Mottola, L.: Playing with time in publish-subscribe using a domain-specific model checker. In: SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems, pp. 55\u201362. ACM, New York (2007)"},{"key":"8_CR11","first-page":"199","volume-title":"ICSE 2007: Proceedings of the 29th International Conference on Software Engineering","author":"L. Baresi","year":"2007","unstructured":"Baresi, L., Ghezzi, C., Mottola, L.: On accurate automatic verification of publish-subscribe architectures. In: ICSE 2007: Proceedings of the 29th International Conference on Software Engineering, Washington, DC, USA, pp. 199\u2013208. IEEE Computer Society, Los Alamitos (2007)"},{"key":"8_CR12","doi-asserted-by":"publisher","DOI":"10.1002\/0471200581","volume-title":"Queuing Network and Markov Chains","author":"G. Bolch","year":"1998","unstructured":"Bolch, G., Greiner, S., de Meer, H., Trivedi, K.: Queuing Network and Markov Chains. John Wiley, Chichester (1998)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Canfora, G., Di Penta, M., Esposito, R., Villani, M.L.: An Approach for QoS-aware Service Composition Based on Genetic Algorithms. In: Proc. of Genetic and Computation Conf. Washington, DC, pp. 1069\u20131075 (June 2005)","DOI":"10.1145\/1068009.1068189"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1109\/SCW.2006.1","volume-title":"Services computing workshops, SCW 2006","author":"V. Cardellini","year":"2006","unstructured":"Cardellini, V., Casalicchio, E., Grassi, V., Mirandola, R.: A framework for optimal service selection in broker-based architectures with multiple QoS classes. In: Services computing workshops, SCW 2006, pp. 105\u2013112. IEEE Computer Society, Los Alamitos (2006)"},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1002\/spip.302","volume":"12","author":"J. Cardoso","year":"2007","unstructured":"Cardoso, J.: Complexity analysis of BPEL web processes. Software Process: Improvement and Practice\u00a012(1), 35\u201349 (2007)","journal-title":"Software Process: Improvement and Practice"},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.websem.2004.03.001","volume":"1","author":"J. Cardoso","year":"2004","unstructured":"Cardoso, J., Sheth, A.P., Miller, J.A., Arnold, J., Kochut, K.: Quality of service for workflows and web service processes. J. Web Sem.\u00a01(3), 281\u2013308 (2004)","journal-title":"J. Web Sem."},{"key":"8_CR17","first-page":"46","volume":"0","author":"W.L. Dong","year":"2006","unstructured":"Dong, W.L., YU., H.: Optimizing web service composition based on qos negotiation. EDOCW\u00a00, 46 (2006)","journal-title":"EDOCW"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/11513988_15","volume-title":"Computer Aided Verification","author":"M.B. Dwyer","year":"2005","unstructured":"Dwyer, M.B., Hatcliff, J., Hoosier, M., Robby,: Building your own software model checker using the bogor extensible model checking framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 148\u2013152. Springer, Heidelberg (2005)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11549970_15","volume-title":"Formal Techniques for Computer Systems and Business Processes","author":"S. Gilmore","year":"2005","unstructured":"Gilmore, S., Haenel, V., Kloul, L., Maidl, M.: Choreographing security and performance analysis for web services. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW\/WS-EM 2005. LNCS, vol.\u00a03670. pp. 200\u2013214. Springer, Heidelberg (2005)"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.ress.2004.08.004","volume":"89","author":"S. Gilmore","year":"2005","unstructured":"Gilmore, S., Kloul, L.: A unified tool for performance modelling and prediction. Reliability Engineering and System Safety\u00a089, 17\u201332 (2005)","journal-title":"Reliability Engineering and System Safety"},{"issue":"4","key":"8_CR21","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1016\/j.jss.2006.07.023","volume":"80","author":"V. Grassi","year":"2007","unstructured":"Grassi, V., Mirandola, R., Sabetta, A.: Filling the gap between design and performance\/reliability models of component-based systems: A model-driven approach. Journal of Systems and Software\u00a080(4), 528\u2013558 (2007)","journal-title":"Journal of Systems and Software"},{"issue":"5","key":"8_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-73196-2_16","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007","author":"F. He","year":"2007","unstructured":"He, F., Baresi, L., Ghezzi, C., Spoletini, P.: Formal analysis of publish-subscribe systems by probabilistic timed automata. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol.\u00a04574, pp. 247\u2013262. Springer, Heidelberg (2007)"},{"key":"8_CR24","first-page":"449","volume-title":"Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE)","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.: Quantitative verification: Models, techniques and tools. In: Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 449\u2013458. ACM Press, New York (2007)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/11921998_11","volume-title":"Quality of Software Architectures","author":"A. Marco Di","year":"2006","unstructured":"Di Marco, A., Mirandola, R.: Model transformation in software performance engineering. In: Hofmeister, C., Crnkovi\u0107, I., Reussner, R. (eds.) QoSA 2006. LNCS, vol.\u00a04214, pp. 95\u2013110. Springer, Heidelberg (2006)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Software Architectures, Components, and Applications","author":"M. Marzolla","year":"2008","unstructured":"Marzolla, M., Mirandola, R.: Performance prediction of web service workflows. In: Overhage, S., Szyperski, C.A., Reussner, R., Stafford, J.A. (eds.) QoSA 2007. LNCS, vol.\u00a04880. Springer, Heidelberg (2008)"},{"issue":"5","key":"8_CR28","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/MIC.2004.27","volume":"8","author":"E.M. Maximilien","year":"2004","unstructured":"Maximilien, E.M., Singh, M.P.: A Framework and Ontology for Dynamic Web Services Selection. IEEE Internet Computing\u00a08(5), 84\u201393 (2004)","journal-title":"IEEE Internet Computing"},{"issue":"6","key":"8_CR29","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/MIC.2002.1067740","volume":"6","author":"D.A. Menasce","year":"2002","unstructured":"Menasce, D.A.: QoS Issues in Web Services. IEEE Internet Computing\u00a06(6), 72\u201375 (2002)","journal-title":"IEEE Internet Computing"},{"key":"8_CR30","unstructured":"Object Management Group. UML 2.0 superstructure specification (2002)"},{"key":"8_CR31","unstructured":"Object Management\u00a0Group OMG. UML Profile for Modeling and Analysis of Real-Time and Embedded Systems. ptc\/07-08-04 (2007)"},{"key":"8_CR32","unstructured":"Papyrus UML, \n                    \n                      http:\/\/www.papyrusuml.org\/"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1007\/978-3-540-45227-0_80","volume-title":"Database and Expert Systems Applications","author":"C. Patel","year":"2003","unstructured":"Patel, C., Supekar, K., Lee, Y.: A QoS Oriented Framework for Adaptive Management of Web Service Based Workflows. In: Ma\u0159\u00edk, V., \u0160t\u011bp\u00e1nkov\u00e1, O., Retschitzegger, W. (eds.) DEXA 2003. LNCS, vol.\u00a02736, pp. 826\u2013835. Springer, Heidelberg (2003)"},{"key":"8_CR34","unstructured":"PRISM, Probabilistic Model Checker, \n                    \n                      http:\/\/www.prismmodelchecker.org\/"},{"key":"8_CR35","first-page":"205","volume":"0","author":"F. Rosenberg","year":"2006","unstructured":"Rosenberg, F., Platzer, C., Dustdar, S.: Bootstrapping performance and dependability attributes of web services. ICWS\u00a00, 205\u2013212 (2006)","journal-title":"ICWS"},{"key":"8_CR36","first-page":"140","volume":"0","author":"D. Rud","year":"2006","unstructured":"Rud, D., Schmietendorf, A., Dumke, R.: Performance modeling of WS-BPEL-based web service compositions. SCW\u00a00, 140\u2013147 (2006)","journal-title":"SCW"},{"key":"8_CR37","first-page":"505","volume":"0","author":"H.A. Schmid","year":"2006","unstructured":"Schmid, H.A.: Service congestion: The problem, and an optimized service composition architecture as a solution. ICWS\u00a00, 505\u2013514 (2006)","journal-title":"ICWS"},{"key":"8_CR38","unstructured":"Yu, T., Lin, K.J.: A Broker-Based Framework for QoS-Aware Web Service Composition. In: Proc. of 2005 IEEE Int\u2019l Conf. on e-Technology, e-Commerce and e-Service (March 2005)"},{"issue":"5","key":"8_CR39","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1109\/TSE.2004.11","volume":"30","author":"L. Zeng","year":"2004","unstructured":"Zeng, L., Benatallah, B., Ngu, A.H.H., Dumas, M., Kalagnanam, J., Chang, H.: QoS-Aware Middleware for Web Services Composition. IEEE Trans. Softw. Eng.\u00a030(5), 311\u2013327 (2004)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Quality of Software Architectures. Models and Architectures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87879-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T03:38:52Z","timestamp":1548387532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87879-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540878780","9783540878797"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87879-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}