{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:49:25Z","timestamp":1743155365253,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031737084"},{"type":"electronic","value":"9783031737091"}],"license":[{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"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-73709-1_4","type":"book-chapter","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T10:12:01Z","timestamp":1728382321000},"page":"50-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Approaches for\u00a0Modeling and\u00a0Analysis of\u00a0Business Process Collaborations"],"prefix":"10.1007","author":[{"given":"Flavio","family":"Corradini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabrizio","family":"Fornari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Re","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lorenzo","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Polini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vandin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,9]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-20401-2_8","volume-title":"Rigorous Software Engineering for Service-Oriented Systems","author":"L Caires","year":"2011","unstructured":"Caires, L., De Nicola, R., Pugliese, R., Vasconcelos, V.T., Zavattaro, G.: Core calculi for service-oriented computing. In: Wirsing, M., H\u00f6lzl, M. (eds.) Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582, pp. 153\u2013188. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20401-2_8"},{"issue":"3","key":"4_CR2","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1007\/S10270-022-01049-2","volume":"22","author":"I Compagnucci","year":"2023","unstructured":"Compagnucci, I., Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F.: A systematic literature review on iot-aware business process modeling views, requirements and notations. Softw. Syst. Model. 22(3), 969\u20131004 (2023). https:\/\/doi.org\/10.1007\/S10270-022-01049-2","journal-title":"Softw. Syst. Model."},{"key":"4_CR3","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-030-87205-2_6","volume-title":"Perspectives in Business Informatics Research","author":"I Compagnucci","year":"2021","unstructured":"Compagnucci, I., Corradini, F., Fornari, F., Re, B.: Trends on the usage of BPMN 2.0 from publicly available repositories. In: Buchmann, R.A., Polini, A., Johansson, B., Karagiannis, D. (eds.) BIR 2021. LNBIP, vol. 430, pp. 84\u201399. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-87205-2_6"},{"issue":"1","key":"4_CR4","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/S12599-023-00818-7","volume":"66","author":"I Compagnucci","year":"2024","unstructured":"Compagnucci, I., Corradini, F., Fornari, F., Re, B.: A study on the usage of the BPMN notation for designing process collaboration, choreography, and conversation models. Bus. Inf. Syst. Eng. 66(1), 43\u201366 (2024). https:\/\/doi.org\/10.1007\/S12599-023-00818-7","journal-title":"Bus. Inf. Syst. Eng."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/J.SCICO.2018.05.008","volume":"166","author":"F Corradini","year":"2018","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F.: A formal approach to modeling and verification of business process collaborations. Sci. Comput. Program. 166, 35\u201370 (2018). https:\/\/doi.org\/10.1016\/J.SCICO.2018.05.008","journal-title":"Sci. Comput. Program."},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: Bprove: a formal verification framework for business process models. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, 30 October\u201303 November 2017, pp. 217\u2013228. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115635","DOI":"10.1109\/ASE.2017.8115635"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: Bprove: tool support for business process verification. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, 30 October\u201303 November 2017, pp. 937\u2013942. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115708","DOI":"10.1109\/ASE.2017.8115708"},{"key":"4_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2021.111007","volume":"180","author":"F Corradini","year":"2021","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: A formal approach for the analysis of BPMN collaboration models. J. Syst. Softw. 180, 111007 (2021). https:\/\/doi.org\/10.1016\/J.JSS.2021.111007","journal-title":"J. Syst. Softw."},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2020.100630","volume":"119","author":"F Corradini","year":"2021","unstructured":"Corradini, F., Morichetta, A., Muzi, C., Re, B., Tiezzi, F.: Well-structuredness, safeness and soundness: a formal classification of BPMN collaborations. J. Log. Algebraic Methods Program. 119, 100630 (2021). https:\/\/doi.org\/10.1016\/J.JLAMP.2020.100630","journal-title":"J. Log. Algebraic Methods Program."},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-98648-7_6","volume-title":"Business Process Management","author":"F Corradini","year":"2018","unstructured":"Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: Animating multiple instances in BPMN collaborations: from formal semantics to tool support. In: Weske, M., Montali, M., Weber, I., vom Brocke, J. (eds.) BPM 2018. LNCS, vol. 11080, pp. 83\u2013101. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98648-7_6"},{"key":"4_CR11","unstructured":"Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: MIDA: multiple instances and data animator. In: van\u00a0der Aalst, W.M.P., et al. (eds.) Proceedings of the Dissertation Award, Demonstration, and Industrial Track at BPM 2018 co-located with 16th International Conference on Business Process Management (BPM 2018), Sydney, Australia, 9\u201314 September 2018. CEUR Workshop Proceedings, vol.\u00a02196, pp. 86\u201390. CEUR-WS.org (2018). https:\/\/ceur-ws.org\/Vol-2196\/BPM_2018_paper_18.pdf"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: BPMN 2.0 or-join semantics: global and local characterisation. Inf. Syst. 105, 101934 (2022). https:\/\/doi.org\/10.1016\/J.IS.2021.101934","DOI":"10.1016\/J.IS.2021.101934"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-319-28934-2_9","volume-title":"Formal Aspects of Component Software","author":"F Corradini","year":"2016","unstructured":"Corradini, F., Polini, A., Re, B., Tiezzi, F.: An operational semantics of BPMN collaboration. In: Braga, C., \u00d6lveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 161\u2013180. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-28934-2_9"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/S1571-0661(05)82534-4","volume":"71","author":"S Eker","year":"2004","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The maude ltl model checker. Electron. Notes Theor. Comput. Sci. 71, 162\u2013187 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"El-Saber, N.A.S., Boronat, A.: BPMN formalization and verification using maude. In: Proceedings of the 2014 Workshop on Behaviour Modelling - Foundations and Applications, BM-FA 2014, York, United Kingdom, 22 July 2014, p.\u00a01. ACM (2014). https:\/\/doi.org\/10.1145\/2630768.2630769","DOI":"10.1145\/2630768.2630769"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Gorp, P.V., Dijkman, R.M.: A visual token-based formalization of BPMN 2.0 based on in-place transformations. Inf. Softw. Technol. 55(2), 365\u2013394 (2013). https:\/\/doi.org\/10.1016\/J.INFSOF.2012.08.014","DOI":"10.1016\/J.INFSOF.2012.08.014"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-23063-4_4","volume-title":"Business Process Management","author":"A Kheldoun","year":"2015","unstructured":"Kheldoun, A., Barkaoui, K., Ioualalen, M.: Specification and verification of complex business processes - a high-level petri net-based approach. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 55\u201371. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23063-4_4"},{"key":"4_CR18","unstructured":"OMG: Business Process Model and Notation (BPMN V 2.0) (2011)"},{"key":"4_CR19","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Proceedings of ValueTools 2013, pp. 310\u2013315. ICST\/ACM (2013)"},{"key":"4_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.jedc.2022.104458","volume":"143","author":"A Vandin","year":"2022","unstructured":"Vandin, A., Giachini, D., Lamperti, F., Chiaromonte, F.: Automated and distributed statistical analysis of economic agent-based models. J. Econ. Dyn. Control 143, 104458 (2022)","journal-title":"J. Econ. Dyn. Control"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73709-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T09:04:47Z","timestamp":1729674287000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73709-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,9]]},"ISBN":["9783031737084","9783031737091"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73709-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,9]]},"assertion":[{"value":"9 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}