{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T15:19:38Z","timestamp":1778167178967,"version":"3.51.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031955884","type":"print"},{"value":"9783031955891","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-95589-1_8","type":"book-chapter","created":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T14:48:36Z","timestamp":1750171716000},"page":"153-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Behavioural, Functional, and\u00a0Non-functional Contracts for\u00a0Dynamic Selection of\u00a0Services"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0248-5019","authenticated-orcid":false,"given":"Carlos G.","family":"Lopez Pombo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0760-0618","authenticated-orcid":false,"given":"Hern\u00e1n","family":"Melgratti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1806-6932","authenticated-orcid":false,"given":"Agust\u00edn E.","family":"Martinez-Su\u00f1\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego Senarruzza","family":"Anabia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7032-3281","authenticated-orcid":false,"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,18]]},"reference":[{"key":"8_CR1","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Pearson Education Inc. (2006)"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1109\/TSE.2012.64","volume":"39","author":"A Aleti","year":"2013","unstructured":"Aleti, A., Buhnova, B., Grunske, L., Koziolek, A., Meedeniya, I.: Software architecture optimization methods: a systematic literature review. IEEE Trans. Softw. Eng. 39, 658\u2013683 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR3","unstructured":"Anonymous: Post office protocol: Version 2. On-line (1985). https:\/\/rfc-editor.org\/rfc\/rfc937.txt"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-030-50029-0_6","volume-title":"Coordination Models and Languages","author":"F Barbanera","year":"2020","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: Choreography automata. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 86\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_6"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"8_CR6","unstructured":"Beachy, J.A., Blair, W.D.: Abstract Algebra, 3rd edn. Waveland Press Inc. (2006)"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Biere, A., Heule, M., Van\u00a0Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability: Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA336","DOI":"10.3233\/FAIA336"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-15375-4_12","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Bocchi","year":"2010","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162\u2013176. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-71316-6_3","volume-title":"Programming Languages and Systems","author":"MG Buscemi","year":"2007","unstructured":"Buscemi, M.G., Montanari, U.: CC-Pi: a constraint-based language for specifying service level agreements. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 18\u201332. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_3"},{"key":"8_CR11","unstructured":"World Wide\u00a0Web Consortium: Web services description language (WSDL) version 2.0 part 1: Core language. On-line. https:\/\/www.w3.org\/TR\/wsdl20\/"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11417019_3","volume-title":"Coordination Models and Languages","author":"R De Nicola","year":"2005","unstructured":"De Nicola, R., Ferrari, G., Montanari, U., Pugliese, R., Tuosto, E.: A process calculus for QoS-aware applications. In: Jacquet, J.-M., Picco, G.P. (eds.) COORDINATION 2005. LNCS, vol. 3454, pp. 33\u201348. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11417019_3"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9","volume-title":"Computer Aided Verification","year":"2014","unstructured":"Biere, A., Bloem, R. (eds.): CAV 2014. LNCS, vol. 8559. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9"},{"key":"8_CR15","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press (1972)"},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"542","DOI":"10.2307\/1969812","volume":"61","author":"P Erd\u00f6s","year":"1955","unstructured":"Erd\u00f6s, P., Gillman, L., Henriksen, M.: An isomorphism theorem for real-closed fields. Ann. Math. 61(3), 542\u2013554 (1955)","journal-title":"Ann. Math."},{"issue":"4","key":"8_CR17","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s00165-010-0166-z","volume":"23","author":"JL Fiadeiro","year":"2011","unstructured":"Fiadeiro, J.L., Lopes, A., Bocchi, L.: An abstract model of service discovery and binding. Formal Aspects Comput. 23(4), 433\u2013463 (2011)","journal-title":"Formal Aspects Comput."},{"key":"8_CR18","unstructured":"Gheri, L., Lanese, I., Sayers, N., Tuosto, E., Yoshida, N.: Design-by-contract for flexible multiparty session protocols. In: Ali, K., Vitek, J. (eds.) Proceedings of 36th European Conference on Object-Oriented Programming, ECOOP 2022. LIPIcs, vol.\u00a0222, pp. 8:1\u20138:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jnca.2018.03.003","volume":"110","author":"V Hayyolalam","year":"2018","unstructured":"Hayyolalam, V., Kazem, A.: A systematic literature review on QoS-aware service composition and selection in cloud environment. J. Netw. Comput. Appl. 110, 52\u201374 (2018)","journal-title":"J. Netw. Comput. Appl."},{"issue":"1","key":"8_CR20","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-34321-6_17","volume-title":"Service-Oriented Computing","author":"D Ivanovi\u0107","year":"2012","unstructured":"Ivanovi\u0107, D., Carro, M., Hermenegildo, M.V.: A constraint-based approach to quality assurance in service choreographies. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds.) Service-Oriented Computing, pp. 252\u2013267. Springer, Heidelberg (2012)"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-45005-1_3","volume-title":"Service-Oriented Computing","author":"A Kattepur","year":"2013","unstructured":"Kattepur, A., Georgantas, N., Issarny, V.: QoS analysis in heterogeneous choreography interactions. In: Basu, S., Pautasso, C., Zhang, L., Fu, X. (eds.) Service-Oriented Computing, pp. 23\u201338. Springer, Heidelberg (2013)"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Lluch-Lafuente, A., Montanari, U.: Quantitative $$\\mu $$-calculus and CTL based on constraint semirings. Electron. Notes Theor. Comput. Sci. 112, 37\u201359 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2004.02.063. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066104052417. Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages (QAPL 2004)","DOI":"10.1016\/j.entcs.2004.02.063"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Lopez Pombo, C.G., Martinez Su\u00f1\u00e9, A.E., Tuosto, E.: A dynamic temporal logic for quality of service in choreographic models. In: \u00c1brah\u00e1m, E., Dubslaff, C., Tarifa, S.L.T. (eds.) Proceedings of 20th International Colloquium on Theoretical Aspects of Computing - ICTAC 2023. LNCS, vol. 14446, pp. 119\u2013138. Springer, Lima (2023)","DOI":"10.1007\/978-3-031-47963-2_9"},{"key":"8_CR25","unstructured":"Lopez Pombo, C.G., Martinez Su\u00f1\u00e9, A.E., Tuosto, E.: MoCheQoS: automated analysis of quality of service properties of communicating systems. On-line (2023). https:\/\/arxiv.org\/abs\/2311.01415"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Lopez Pombo, C.G., Martinez Su\u00f1\u00e9, A.E., Tuosto, E.: Automated static analysis of quality of service properties of communicating systems. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Proceedings of 26th. International Symposium on Formal Methods (FM 2024) - Part II. LNCS, vol. 14934, pp. 84\u2013103. Springer, Cham (2025)","DOI":"10.1007\/978-3-031-71177-0_7"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Lopez Pombo, C.G., Montepagano, P., Tuosto, E.: SEArch: an execution infrastructure for service-based software systems. In: Castellani, I., Tiezzi, F. (eds.) Proceedings of Coordination Models and Languages - 26nd IFIP WG 6.1 International Conference, COORDINATION 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024. LNCS, vol. 14676, pp. 314\u2013330. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-62697-5_17"},{"key":"8_CR28","unstructured":"Martinez Su\u00f1\u00e9, A.E.: Formalizaci\u00f3n y an\u00e1lisis de requerimientos no-funcionales cuantificables. Ph.D. thesis, Departamento de Computaci\u00f3n, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires (2024). Advisor: Carlos G. Lopez Pombo"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-030-22397-7_13","volume-title":"Coordination Models and Languages","author":"AE Martinez Su\u00f1\u00e9","year":"2019","unstructured":"Martinez Su\u00f1\u00e9, A.E., Lopez Pombo, C.G.: Automatic quality-of-service evaluation in service-oriented computing. In: Riis Nielson, H., Tuosto, E. (eds.) COORDINATION 2019. LNCS, vol. 11533, pp. 221\u2013236. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22397-7_13"},{"key":"8_CR30","unstructured":"Rosenthal, K.I.: Quantales and Their Application. Pitman Research Notes in Mathematics Series, vol.\u00a0234. Longman Scientific & Technical (1990)"},{"key":"8_CR31","unstructured":"Anabia, D.N.S.: Bisimulaci\u00f3n de Data-aware Communicating Finite State Machines con propiedades en las acciones. Master\u2019s thesis, Departamento de Computaci\u00f3n, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires,: advisors: Carlos G. Lopez Pombo and Hern\u00e1n C, Melgratti (2023)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-Order Logic. Dover Publishing (1968)","DOI":"10.1007\/978-3-642-86718-7"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Memorandum RM-109, RAND Corporation (1951), later published in\u00a0[34] and reprinted in\u00a0[35]","DOI":"10.1525\/9780520348097"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951), originally published in\u00a0[33] and reprinted in\u00a0[35]","DOI":"10.1525\/9780520348097"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, pp. 24\u201384. Texts and Monographs in Symbolic Computation, Springer, Cham (1998), originally published in\u00a0[33] and reprinted from\u00a0[34]","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Vissani, I., Lopez Pombo, C.G., Tuosto, E.: Communicating machines as a dynamic binding mechanism of services. In: Gay, D., Alglave, J. (eds.) Proceedings of 8th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0203, pp. 85\u201398 (2016)","DOI":"10.4204\/EPTCS.203.7"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. In: OOPSLA 2020: Conference on Object-Oriented Programming Systems, Languages and Applications. p. 30 pages. No. OOPSLA (Article 148) in PACMPL. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3428216","DOI":"10.1145\/3428216"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-95589-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T14:52:27Z","timestamp":1778165547000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-95589-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031955884","9783031955891"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-95589-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"18 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Models and Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}