{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T04:09:02Z","timestamp":1747541342960,"version":"3.40.5"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319153162"},{"type":"electronic","value":"9783319153179"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15317-9_3","type":"book-chapter","created":{"date-parts":[[2015,1,29]],"date-time":"2015-01-29T06:05:37Z","timestamp":1422511537000},"page":"31-48","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verified Service Compositions by Template-Based Construction"],"prefix":"10.1007","author":[{"given":"Sven","family":"Walther","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,1,30]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K Apt","year":"2009","unstructured":"Apt, K., de Boer, F., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, London (2009)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-40020-2_2","volume-title":"Recent Trends in Algebraic Development Techniques","author":"F Arbab","year":"2003","unstructured":"Arbab, F., Rutten, J.J.M.M.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 34\u201355. Springer, Heidelberg (2003)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbad","year":"2004","unstructured":"Arbad, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14, 329\u2013366 (2004)","journal-title":"Math. Struct. Comput. Sci."},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Arifulina, S., Becker, M., Platenius, M.C., Walther, S.: SeSAME: modeling and analyzing high-quality service compositions. In: Proceedings of the 29th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2014), Tool Demonstrations. ACM, 15\u201319 September 2014, to appear","DOI":"10.1145\/2642937.2648621"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Horrocks, I., Sattler, U.: Description logics. In: Frank van Harmelen, V.L., Porter, B. (eds.) Foundations of Artificial Intelligence, vol. 3, pp. 135\u2013179. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03003-9"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Becker, M., Luckey, M., Becker, S.: Performance analysis of self-adaptive systems for requirements validation at design-time. In: QoSA, pp. 43\u201352. ACM (2013)","DOI":"10.1145\/2465478.2465489"},{"issue":"1","key":"3_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jss.2008.03.066","volume":"82","author":"S Becker","year":"2009","unstructured":"Becker, S., Koziolek, H., Reussner, R.: The palladio component model for model-driven performance prediction. J. Syst. Softw. 82(1), 3\u201322 (2009). Special Issue: Software Performance - Modeling and Analysis","journal-title":"J. Syst. Softw."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Bures, T., Hnetynka, P., Plasil, F.: SOFA 2.0: balancing advanced features in a hierarchical component model. In: SERA, pp. 40\u201348 (2006)","DOI":"10.1109\/SERA.2006.62"},{"issue":"9","key":"3_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69\u201377 (2012)","journal-title":"Commun. ACM"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Farahbod, R., Gl\u00e4sser, U., Vajihollahi, M.: Abstract operational semantics of the business process execution language for web services. Technical report (2005)","DOI":"10.1007\/978-3-540-24773-9_7"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-30122-6_4","volume-title":"Principles and Practice of Semantic Web Reasoning","author":"E Franconi","year":"2004","unstructured":"Franconi, E., Tessaris, S.: Rules and queries with ontologies: a unified logical framework. In: Ohlbach, H.J., Schaffert, S. (eds.) PPSWR 2004. LNCS, vol. 3208, pp. 50\u201360. Springer, Heidelberg (2004)"},{"key":"3_CR12","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Boston (1995)"},{"issue":"2","key":"3_CR13","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1006\/knac.1993.1008","volume":"5","author":"TR Gruber","year":"1993","unstructured":"Gruber, T.R.: A translation approach to portable ontology specifications. Knowl. Acquisition 5(2), 199\u2013220 (1993)","journal-title":"Knowl. Acquisition"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-92673-3_0","volume-title":"Handbook on Ontologies: International Handbooks on Information Systems","author":"N Guarino","year":"2009","unstructured":"Guarino, N., Oberle, D., Staab, S.: What is an ontology? In: Staab, S., Studer, R. (eds.) Handbook on Ontologies: International Handbooks on Information Systems, pp. 1\u201317. Springer, Heidelberg (2009)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Hemer, D.: Semi-automated component-based development of formally verified software. In: Proceedings of the 11th Refinement Workshop (REFINE 2006), Electronic Notes in Theoretical Computer Science, vol. 187, pp. 173\u2013188 (2007)","DOI":"10.1016\/j.entcs.2006.08.051"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-63533-5_26","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"D Hemer","year":"1997","unstructured":"Hemer, D., Lindsay, P.: Reuse of verified design templates through extended pattern matching. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 495\u2013514. Springer, Heidelberg (1997)"},{"issue":"5","key":"3_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.entcs.2008.04.044","volume":"211","author":"M Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, M., G\u00f6nczy, L.: Simulation and formal analysis of workflow models. Electron. Notes Theor. Comput. Sci. 211, 221\u2013230 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.compind.2012.09.004","volume":"64","author":"SK Kumar","year":"2013","unstructured":"Kumar, S.K., Harding, J.A.: Ontology mapping using description logic and bridging axioms. Comput. Ind. 64(1), 19\u201328 (2013)","journal-title":"Comput. Ind."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Lindsay, P.A., Hemer, D.: An industrial-strength method for the construction of formally verified software. In: Australian Software Engineering Conference, p. 27 (1996)","DOI":"10.1109\/ASWEC.1996.534120"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-540-30581-1_4","volume-title":"Semantic Web Services and Web Process Composition","author":"D Martin","year":"2005","unstructured":"Martin, D., Paolucci, M., McIlraith, S.A., Burstein, M., McDermott, D., McGuinness, D.L., Parsia, B., Payne, T.R., Sabou, M., Solanki, M., Srinivasan, N., Sycara, K.: Bringing semantics to web services: the OWL-S approach. In: Cardoso, J., Sheth, A.P. (eds.) SWSWPC 2004. LNCS, vol. 3387, pp. 26\u201342. Springer, Heidelberg (2005)"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-540-92673-3_26","volume-title":"Handbook on Ontologies: International Handbooks on Information Systems","author":"NF Noy","year":"2009","unstructured":"Noy, N.F.: Ontology mapping. In: Staab, S., Studer, R. (eds.) Handbook on Ontologies: International Handbooks on Information Systems, pp. 573\u2013590. Springer, Heidelberg (2009)"},{"key":"3_CR23","unstructured":"OASIS: Web services business process execution language v2.0. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.pdf"},{"issue":"2\u20133","key":"3_CR24","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.scico.2007.03.002","volume":"67","author":"C Ouyang","year":"2007","unstructured":"Ouyang, C., Verbeek, E., van der Aalst, W.M.P., Breutel, S., Dumas, M., ter Hofstede, A.H.M.: Formal semantics and analysis of control flow in WS-BPEL. Sci. Comput. Program. 67(2\u20133), 162\u2013198 (2007)","journal-title":"Sci. Comput. Program."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR26","unstructured":"Singh, M.P.: Formal aspects of workflow management - part 1: semantics (1997)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Walther, S., Wehrheim, H.: Knowledge-based verification of service compositions - an SMT approach. In: ICECCS, pp. 24\u201332 (2013)","DOI":"10.1109\/ICECCS.2013.14"},{"key":"3_CR28","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Upper Saddle River (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15317-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,17]],"date-time":"2025-05-17T23:23:46Z","timestamp":1747524226000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15317-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319153162","9783319153179"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15317-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"30 January 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}