{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T17:22:08Z","timestamp":1749921728817,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031626968"},{"type":"electronic","value":"9783031626975"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-62697-5_13","type":"book-chapter","created":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T21:01:23Z","timestamp":1718053283000},"page":"239-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["TRAC: A\u00a0Tool for\u00a0Data-Aware Coordination"],"prefix":"10.1007","author":[{"given":"Jo\u00e3o","family":"Afonso","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8372-8015","authenticated-orcid":false,"given":"Elvis","family":"Konjoh Selabi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7613-621X","authenticated-orcid":false,"given":"Maurizio","family":"Murgia","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8074-0380","authenticated-orcid":false,"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7032-3281","authenticated-orcid":false,"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,11]]},"reference":[{"key":"13_CR1","unstructured":"Afonso, J.: Mechanisms for modeling and validation of smart contracts. Master\u2019s thesis, Departamento de Inform\u00e1tica, NOVA School of Science and Technology (2023). Advisor: Ant\u00f3nio Ravara"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Afonso, J., Konjoh\u00a0Selabi, E., Murgia, M., Tuosto, E., Ravara, A.: Artefact submission for paper #8 of COORDINATION 2024 (2024). https:\/\/doi.org\/10.5281\/zenodo.10996456","DOI":"10.5281\/zenodo.10996456"},{"key":"13_CR3","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":"13_CR4","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.: Contract automata library. Sci. Comput. Program. 221, 102841 (2022). https:\/\/doi.org\/10.1016\/J.SCICO.2022.102841","DOI":"10.1016\/J.SCICO.2022.102841"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-39570-8_5","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D Basile","year":"2016","unstructured":"Basile, D., Degano, P., Ferrari, G.-L., Tuosto, E.: Playing with our CAT and communication-centric applications. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 62\u201373. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_5"},{"key":"13_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/978-3-031-27481-7_31","volume-title":"Formal Methods","author":"D Basile","year":"2023","unstructured":"Basile, D., ter Beek, M.: A runtime environment for contract automata. In: Chechik, M., Katoen, J., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 550\u2013567. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_31"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M., Pugliese, R.: Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services. Log. Methods Comput. Sci. 16(2) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(2:9)2020","DOI":"10.23638\/LMCS-16(2:9)2020"},{"key":"13_CR8","unstructured":"Buterin, V.: Ethereum: a next generation smart contract and decentralized application platform (2014). https:\/\/ethereum.org\/whitepaper"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36946-9_3","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"D Clarke","year":"2013","unstructured":"Clarke, D., \u00d6stlund, J., Sergey, I., Wrigstad, T.: Ownership types: a survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 15\u201358. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36946-9_3"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Coblenz, M.J., et al.: Obsidian: typestate and assets for safer blockchain programming. ACM Trans. Program. Lang. Syst. 42(3), 14:1\u201314:82 (2020). https:\/\/doi.org\/10.1145\/3417516","DOI":"10.1145\/3417516"},{"key":"13_CR11","unstructured":"Corradini, F., Marcelletti, A., Morichetta, A., Polini, A., Re, B., Tiezzi, F.: Chorchain: a blockchain-based framework for executing and auditing BPMN choreographies. In: BPM (PhD\/Demos). CEUR Workshop Proceedings, vol.\u00a03216, pp. 132\u2013136. CEUR-WS.org (2022)"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Corradini, F., Marcelletti, A., Morichetta, A., Polini, A., Re, B., Tiezzi, F.: Engineering trustable and auditable choreography-based systems using blockchain. ACM Trans. Manag. Inf. Syst. 13(3), 31:1\u201331:53 (2022). https:\/\/doi.org\/10.1145\/3505225","DOI":"10.1145\/3505225"},{"key":"13_CR13","doi-asserted-by":"publisher","DOI":"10.1145\/3637555","author":"F Corradini","year":"2023","unstructured":"Corradini, F., Marcelletti, A., Morichetta, A., Polini, A., Re, B., Tiezzi, F.: Blockchain-based execution of BPMN choreographies with multiple instances. Distributed Ledger Technol. Res. Pract. (2023). https:\/\/doi.org\/10.1145\/3637555","journal-title":"Distributed Ledger Technol. Res. Pract."},{"key":"13_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-031-20872-0_12","volume-title":"Formal Aspects of Component Software","author":"S Crafa","year":"2022","unstructured":"Crafa, S., Laneve, C.: Liquidity analysis in resource-aware programming. In: Tarifa, S.L.T., Proen\u00e7a, J. (eds.) FACS 2022. LNCS, vol. 13712, pp. 205\u2013221. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-20872-0_12"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Crafa, S., Laneve, C., Sartor, G., Veschetti, A.: Pacta sunt servanda: legal contracts in Stipula. Sci. Comput. Program. 225 (2023). https:\/\/doi.org\/10.1016\/J.SCICO.2022.102911","DOI":"10.1016\/J.SCICO.2022.102911"},{"issue":"1","key":"13_CR16","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1016\/j.jlamp.2016.09.008","volume":"86","author":"K Dokter","year":"2017","unstructured":"Dokter, K., Jongmans, S.S., Arbab, F., Bliudze, S.: Combine and conquer: relating BIP and Reo. J. Logic Algebraic Methods Program. 86(1), 134\u2013156 (2017). https:\/\/doi.org\/10.1016\/j.jlamp.2016.09.008","journal-title":"J. Logic Algebraic Methods Program."},{"key":"13_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/978-3-031-32415-4_34","volume-title":"Financial Cryptography and Data Security","author":"A Falc\u00e3o","year":"2022","unstructured":"Falc\u00e3o, A., Mordido, A., Vasconcelos, V.T.: Protocol-based smart contract generation. In: Matsuo, S., et al. (eds.) FC 2022. LNCS, vol. 13412, pp. 555\u2013582. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-32415-4_34"},{"issue":"4","key":"13_CR18","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/2629609","volume":"36","author":"R Garcia","year":"2014","unstructured":"Garcia, R., Tanter, \u00c9., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36(4), 12 (2014). https:\/\/doi.org\/10.1145\/2629609","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR19","doi-asserted-by":"publisher","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.) 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0222, pp. 8:1\u20138:28. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.8","DOI":"10.4230\/LIPIcs.ECOOP.2022.8"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Gheri, L., Lanese, I., Sayers, N., Tuosto, E., Yoshida, N.: Design-by-contract for flexible multiparty session protocols (artifact). Dagstuhl Artifacts Ser. 8(2), 21:1\u201321:5 (2022). https:\/\/doi.org\/10.4230\/DARTS.8.2.21","DOI":"10.4230\/DARTS.8.2.21"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Godoy, J., Galeotti, J.P., Garbervetsky, D., Uchitel, S.: Predicate abstractions for smart contract validation. In: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, MODELS 2022, pp. 289\u2013299. ACM (2022). https:\/\/doi.org\/10.1145\/3550355.3552462","DOI":"10.1145\/3550355.3552462"},{"key":"13_CR22","unstructured":"Object\u00a0Management Group: Business Process Model and Notation. http:\/\/www.bpmn.org"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Hagberg, A.A., Schult, D.A., Swart, P.J.: Exploring network structure, dynamics, and function using networkx. In: Varoquaux, G., Vaught, T., Millman, J. (eds.) Proceedings of the 7th Python in Science Conference, Pasadena, CA USA, pp. 11\u201315 (2008)","DOI":"10.25080\/TCWV9851"},{"key":"13_CR24","unstructured":"Hansen, P.: Operating System Principles. Prentice-Hall, Hoboken (1973)"},{"key":"13_CR25","unstructured":"Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y.: Working Draft 17 December 2004. http:\/\/www.w3.org\/TR\/2004\/WD-ws-cdl-10-20041217"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Keerthi\u00a0Nelaturu, A.M., et\u00a0al.: Correct-by-design interacting smart contracts and a systematic approach for verifying erc20 and erc721 contracts with verisolid. IEEE Trans. Dependable Secure Comput. 20 (2023). https:\/\/doi.org\/10.1109\/TDSC.2022.3200840","DOI":"10.1109\/TDSC.2022.3200840"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Laneve, C.: Liquidity analysis in resource-aware programming. J. Log. Algebraic Methods Program. (2023)","DOI":"10.2139\/ssrn.4282044"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-662-58387-6_28","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2018","unstructured":"Mavridou, A., Laszka, A.: Designing secure ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957, pp. 523\u2013540. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28"},{"key":"13_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-030-32101-7_27","volume-title":"FC 2019","author":"A Mavridou","year":"2019","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Verisolid: correct-by-design smart contracts for ethereum. In: Goldberg, I., Moore, T. (eds.) FC 2019. LNCS, vol. 11598, pp. 446\u2013465. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27"},{"key":"13_CR30","unstructured":"Meyer, B.: Introduction to the Theory of Programming Languages. Prentice-Hall, Hoboken (1990)"},{"key":"13_CR31","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall, Hoboken (1991). http:\/\/www.eiffel.com\/doc\/#etl"},{"key":"13_CR32","unstructured":"Microsoft: The blockchain workbench (2019). https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench"},{"key":"13_CR33","unstructured":"Microsoft: Simple marketplace sample application for azure blockchain workbench (2019). https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples\/simple-marketplace"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-030-90636-8_5","volume-title":"Formal Aspects of Component Software","author":"S Orlando","year":"2021","unstructured":"Orlando, S., Pasquale, V.D., Barbanera, F., Lanese, I., Tuosto, E.: Corinne, a tool for choreography automata. In: Sala\u00fcn, G., Wijs, A. (eds.) FACS 2021. LNCS, vol. 13077, pp. 82\u201392. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90636-8_5"},{"key":"13_CR35","unstructured":"Pign\u00e9, Y., Dutot, A., Guinand, F., Olivier, D.: Graphstream: a tool for bridging the gap between complex systems and dynamic graphs (2008)"},{"key":"13_CR36","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-031-47963-2_9","volume-title":"Theoretical Aspects of Computing","author":"C Pombo","year":"2023","unstructured":"Pombo, C., Su\u00f1\u00e9, A., Tuosto, E.: A dynamic temporal logic for quality of service in choreographic models. In: \u00c1brah\u00e1m, E., Dubslaff, C., Tarifa, S. (eds.) ICTAC 2023. LNCS, vol. 14446, pp. 119\u2013138. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_9"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Qin, X., Bliudze, S., Madelaine, E., Hou, Z., Deng, Y., Zhang, M.: SMT-based generation of symbolic automata. Acta Informatica 57, 627\u2013656 (2020). https:\/\/doi.org\/10.1007\/s00236-020-00367-6","DOI":"10.1007\/s00236-020-00367-6"},{"key":"13_CR38","unstructured":"Senarruzza Anabia, D.: 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 (2023). advisors: Carlos G. Lopez Pombo and Hern\u00e1n C. Melgratti"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Singh, N.K., Fajge, A.M., Halder, R., Alam, M.I.: Formal verification and code generation for solidity smart contracts. In: Distributed Computing to Blockchain, pp. 125\u2013144. Elsevier (2023). https:\/\/doi.org\/10.1016\/B978-0-323-96146-2.00028-0","DOI":"10.1016\/B978-0-323-96146-2.00028-0"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Software Eng. SE-12(1), 157\u2013171 (1986). https:\/\/doi.org\/10.1109\/TSE.1986.6312929","DOI":"10.1109\/TSE.1986.6312929"},{"key":"13_CR41","unstructured":"Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, p.\u00a0561. North-Holland (1990)"}],"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-62697-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T14:50:05Z","timestamp":1732200605000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-62697-5_13"}},"subtitle":["(with an Application to Smart Contracts)"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031626968","9783031626975"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-62697-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"11 June 2024","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":"Groningen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","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":"17 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 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":"coordination2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}