{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T04:45:12Z","timestamp":1778215512057,"version":"3.51.4"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present \"Image missing\", a bounded \"Image missing\"\"Image missing\"to statically analyse Quality of Service ( \"Image missing\") properties of message-passing systems. We consider QoS properties on measurable application-level attributes as well as resource consumption metrics, for example, those relating monetary cost to memory usage. The applicability of \"Image missing\"is evaluated through case studies and experiments. A first case study is based on the AWS cloud while a second one analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of \"Image missing\". These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_7","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"84-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Automated Static Analysis of\u00a0Quality of\u00a0Service Properties of\u00a0Communicating Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0248-5019","authenticated-orcid":false,"given":"Carlos G. Lopez","family":"Pombo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1806-6932","authenticated-orcid":false,"given":"Agust\u00edn Eloy Martinez","family":"Su\u00f1\u00e9","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":[[2024,9,13]]},"reference":[{"issue":"4","key":"7_CR1","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":"7_CR2","unstructured":"Amazon: AWS Lambda Service Level Agreement. https:\/\/aws.amazon.com\/lambda\/sla\/"},{"key":"7_CR3","unstructured":"Amazon: AWS Lambda Pricing. https:\/\/aws.amazon.com\/lambda\/pricing\/"},{"key":"7_CR4","unstructured":"World Wide\u00a0Web Consortium: Web Services Description Language (WSDL) Version 2.0 Part 1: Core Language. https:\/\/www.w3.org\/TR\/wsdl20\/"},{"key":"7_CR5","doi-asserted-by":"publisher","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. Volume 14446 of Lecture Notes in Computer Science., Lima, Per\u00fa, Springer-Verlag (December 2023), pp. 119\u2013138 (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_9","DOI":"10.1007\/978-3-031-47963-2_9"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlamp.2017.11.002","volume":"95","author":"E Tuosto","year":"2018","unstructured":"Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Logical Algebraic Methods. Program. 95, 17\u201340 (2018)","journal-title":"J. Logical Algebraic Methods. Program."},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C., Rehof, J., eds.: Proceedings of 14th International Conference Tools and Algorithms for the Construction and Analysis of Systems TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008. Volume 4963 of Lecture Notes in Computer Science., Springer-Verlag (2008), pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Coto, A., Guanciale, R., Tuosto, E.: Choreographic development of message-passing applications - A tutorial. In Bliudze, S., Bocchi, L., eds.: Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings. Volume 12134 of Lecture Notes in Computer Science., Springer (2020) 20\u201336","DOI":"10.1007\/978-3-030-50029-0_2"},{"key":"7_CR9","unstructured":"Coto, A., Guanciale, R., Lange, J., Tuosto, E.: ChorGram: tool support for choreographic development (2015). https:\/\/bitbucket.org\/eMgssi\/chorgram\/src\/master\/"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Lange, J., Tuosto, E., Yoshida, N.: A tool for choreography-based analysis of message-passing software. In: Gay, S., Ravara, A., eds.: Behavioural Types: from Theory to Tools. Automation, Control and Robotics. River (2017), pp. 125\u2013146 (2017)","DOI":"10.1201\/9781003337331-6"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Lopez\u00a0Pombo, C.G., Martinez-Su\u00f1\u00e9, A.E., Tuosto, E.: MoCheQoS: Automated Static Analysis of Quality of Service Properties of Communicating Systems - Artifact. https:\/\/zenodo.org\/doi\/10.5281\/zenodo.10038447. Git repository available at https:\/\/bitbucket.org\/aemartinez\/chorgram\/src\/mocheqos-fm24\/. June 2024","DOI":"10.1007\/978-3-031-71177-0_7"},{"key":"7_CR12","unstructured":"Amazon: AWS Global Infrastructure. https:\/\/aws.amazon.com\/about-aws\/global-infrastructure. Accessed 27 March 2024"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-030-99524-9_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Imai","year":"2022","unstructured":"Imai, K., Lange, J., Neykova, R.: Kmclib: automated inference and verification of session types from OCaml programs. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 379\u2013386. Cham, Springer International Publishing, Lecture Notes in Computer Science (2022)"},{"issue":"2","key":"7_CR14","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":"7_CR15","doi-asserted-by":"crossref","unstructured":"Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Ann. Pure Appl. Logic 96(1\u20133), 187\u2013207 (1999). Originally published in\u00a0[49]","DOI":"10.1016\/S0168-0072(98)00039-6"},{"key":"7_CR16","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[50] and reprinted in\u00a0[51]","DOI":"10.1525\/9780520348097"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Albert, E., et al.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Serv. Oriented Comput. Appl. 8(4), 323\u2013339 (2014). This article refines and substantially extends\u00a0[52]","DOI":"10.1007\/s11761-013-0148-0"},{"issue":"OOPSLA2","key":"7_CR18","doi-asserted-by":"publisher","first-page":"1589","DOI":"10.1145\/3622854","volume":"7","author":"G Iraci","year":"2023","unstructured":"Iraci, G., Chuang, C.E., Hu, R., Ziarek, L.: Validating IoT devices with rate-based session types. Proc. ACM Program. Lang. 7(OOPSLA2), 1589\u20131617 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S., eds.: Proceedings of 31st International Conference Computer Aided Verification (CAV 2019), Part I. Volume 11561 of Lecture Notes in Computer Science., Springer-Verlag (July 2019), pp. 97\u2013117 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_6","DOI":"10.1007\/978-3-030-25540-4_6"},{"key":"7_CR20","unstructured":"Anonymous: Post office protocol: Version 2 (1985). https:\/\/rfc-editor.org\/rfc\/rfc937.txt"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Hardt, D.: The OAuth 2.0 Authorization Framework (2012). https:\/\/rfc-editor.org\/rfc\/rfc6749.txt","DOI":"10.17487\/rfc6749"},{"key":"7_CR22","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 (November 2023) https:\/\/arxiv.org\/abs\/2311.01415"},{"key":"7_CR23","unstructured":"Ory: Ory - API-first Identity Management, Authentication and Authorization. For Secure, Global, GDPR-compliant Apps. https:\/\/www.ory.sh\/. Accessed 3 April 2024"},{"key":"7_CR24","unstructured":"Amazon Web Services, Inc.: Bulk Cloud Email Service - Amazon Simple Email Service - AWS. https:\/\/aws.amazon.com\/ses\/. Accessed 3 April 2024"},{"key":"7_CR25","unstructured":"Amazon Web Services Inc.: AWS Marketplace: iRedMail (IMAP, SMTP, POP3) Email Server on Ubuntu 18.04 LTS. https:\/\/aws.amazon.com\/marketplace\/pp\/prodview-xswbskbnidz5e. Accessed 3 April 2024"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"McCabe, T.J.: A complexity measure. IEEE Trans. Softw. Eng. SE-2(4), 308\u2013320 (1976)","DOI":"10.1109\/TSE.1976.233837"},{"key":"7_CR27","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. Software Eng. 39, 658\u2013683 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"7_CR28","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.P.: 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."},{"key":"7_CR29","doi-asserted-by":"publisher","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.: Proceedings of 10th International Conference on Service-Oriented Computing \u2013 ICSOC 2012. Volume 7636 of Lecture Notes in Computer Science., pp. 252\u2013267. Springer-Verlag (November 2012). https:\/\/doi.org\/10.1007\/978-3-642-34321-6_17","DOI":"10.1007\/978-3-642-34321-6_17"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Kattepur, A., Georgantas, N., Issarny, V.: Qos analysis in heterogeneous choreography interactions. In: Basu, S., Pautasso, C., Zhang, L., Fu, X., eds.: Proceedings of the 11nd International Conference on Service Oriented Computing \u2013 ICSOC \u201913. Volume 8274 of Lecture Notes in Computer Science., Springer-Verlag (December 2013), pp.23\u201338 (2013). https:\/\/doi.org\/10.1007\/978-3-642-45005-1_3","DOI":"10.1007\/978-3-642-45005-1_3"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Martinez Su\u00f1\u00e9, A.E., Lopez Pombo, C.G.: Automatic quality-of-service evaluation in service-oriented computing. In: Nielson, H.R., Tuosto, E., eds.: Proceedings of Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019. Volume 11533 of Lecture Notes in Computer Science., Springer-Verlag (June 2019), pp. 221\u2013236 (2019). https:\/\/doi.org\/10.1007\/978-3-030-22397-7_13","DOI":"10.1007\/978-3-030-22397-7_13"},{"key":"7_CR32","unstructured":"Envisage: Engineering Virtualized Services. http:\/\/envisage-project.eu"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M., eds.: Revised papers of the 9th International Symposium Formal Methods for Components and Objects (FMCO 2010). Volume 6957 of Lecture Notes in Computer Science., Springer-Verlag (2012), pp. 142\u2013164 (2012)","DOI":"10.1007\/978-3-642-25271-6_8"},{"key":"7_CR34","unstructured":"The ABS Framework. https:\/\/abs-models.org, https:\/\/github.com\/abstools\/abstools"},{"key":"7_CR35","unstructured":"de\u00a0Gouw, S., Mauro, J., Nobakht, B., Zavattaro, G.: Modeling deployment decisions for elastic services with ABS. On-line (2016). http:\/\/www.envisage-project.eu\/modeling-deployment-decisions-for-elastic-services-with-abs\/"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"de\u00a0Gouw, S., Mauro, J., Nobakht, B., Zavattaro, G.: Declarative elasticity in ABS. In: Aiello, M., Johnsen, E.B., Dustdar, S., Georgievski, I., eds.: Proceedings of Service-Oriented and Cloud Computing (ESOCC 2016) - 5th IFIP WG 2.14 European Conference. Volume 9846 of Lecture Notes in Computer Science., Springer-Verlag (September 2016), pp. 118\u2013134 (2016). https:\/\/doi.org\/10.1007\/978-3-319-44482-6_8","DOI":"10.1007\/978-3-319-44482-6_8"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"de Boer, F.S., et al.: Analysis of SLA compliance in the cloud - an automated, model-based approach. In: Ancona, D., Pace, G., eds.: Proceedings of Second Workshop on Verification of Objects at RunTime EXecution (VORTEXECOOP\/ISSTA 2018). Volume 302 of EPTCS. (July 2019) pp. 1\u201315 (2019)","DOI":"10.4204\/EPTCS.302.0"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Giachino, E., de\u00a0Gouw, S., Laneve, C., Nobakht, B.: Statically and dynamically verifiable SLA metrics. In: \u00c1brah\u00e1m, E., Bonsangue, M.M., Johnsen, E.B., eds.: Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Volume 9660 of Lecture Notes in Computer Science., Springer (2016), pp. 211\u2013225 (2016). https:\/\/doi.org\/10.1007\/978-3-319-30734-3_15","DOI":"10.1007\/978-3-319-30734-3_15"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: Key-abs: a deductive verification tool for the concurrent modeling language ABS. In Felty, A.P., Middeldorp, A., eds.: Proceedings of 25th International Conference on Automated Deduction - CADE-25. Volume 9195 of Lecture Notes in Computer Science., Springer-Verlag (August 2015), pp. 517\u2013526 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_35","DOI":"10.1007\/978-3-319-21401-6_35"},{"key":"7_CR40","unstructured":"Rosenthal, K.I.: Quantales and their application. Volume 234 of Pitman research notes in mathematics series. Longman Scientific & Technical (1990)"},{"key":"7_CR41","doi-asserted-by":"publisher","unstructured":"Buscemi, M.G., Montanari, U.: Cc-pi: a constraint-based language for specifying service level agreements. In: De Nicola, R., ed.: Proceedings of 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2007). Volume 4421 of Lecture Notes in Computer Science., Springer-Verlag (2007), pp. 18\u201332 (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_3","DOI":"10.1007\/978-3-540-71316-6_3"},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"Lluch-Lafuente, A., Montanari, U.: Quantitative $$\\mu $$-calculus and CTL based on constraint semirings. Electron. Notes Theoret. Comput. Sci. 112, 37\u201359 (2005). Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages (QAPL 2004)","DOI":"10.1016\/j.entcs.2004.02.063"},{"key":"7_CR43","doi-asserted-by":"publisher","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.: Proceedings of 7th International Conference Coordination Models and Languages, COORDINATION 2005. Volume 3454 of Lecture Notes in Computer Science., Springer-Verlag (April 2005), pp. 33\u201348 (2005). https:\/\/doi.org\/10.1007\/11417019_3","DOI":"10.1007\/11417019_3"},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: The 6th Joint Meeting on European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering: Companion Papers. ESEC-FSE Companion \u201907, New York, NY, USA, Association for Computing Machinery (September 2007), pp. 449\u2013458 (2007)","DOI":"10.1145\/1295014.1295018"},{"key":"7_CR45","unstructured":"Baier, C., Katoen, J.P., eds.: Principles of Model Checking. The MIT Press (2008)"},{"key":"7_CR46","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, pp. 585\u2013591. Lecture Notes in Computer Science, Berlin, Heidelberg, Springer (2011)"},{"issue":"2","key":"7_CR47","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR48","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Report Series BRICS-RS-97-8, Basic Research in Computer cience (1997). https:\/\/tidsskrift.dk\/brics\/issue\/view\/2365","DOI":"10.7146\/brics.v4i8.18798"},{"key":"7_CR50","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951) Originally published in\u00a0[16] and reprinted in\u00a0[51]","DOI":"10.1525\/9780520348097"},{"key":"7_CR51","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A Decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Vienna (1998). Originally published in\u00a0[16] and reprinted from\u00a0[50]. https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_3","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"7_CR52","doi-asserted-by":"publisher","unstructured":"de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Schlatte, R., Wong, P.Y.: Formal modeling of resource management for cloud architectures: an industrial case study. In: Paoli, F.D., Pimentel, E., Zavattaro, G., eds.: Proceedings of First European Conference Service-Oriented and Cloud Computing (ESOCC 2012). Volume 7592 of Lecture Notes in Computer Science., Springer-Verlag (September 2012), pp. 91\u2013106 Refined and substantially extended in\u00a0[17]. https:\/\/doi.org\/10.1007\/978-3-642-33427-6_7","DOI":"10.1007\/978-3-642-33427-6_7"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T01:10:31Z","timestamp":1732756231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The source code of the tool, the code for generating the experimental data, and detailed instructions on how to reproduce the results presented in this paper are available in the Zenodo repository with the identifier. (See citation in []).","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}