{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T03:11:21Z","timestamp":1780629081935,"version":"3.54.1"},"reference-count":79,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,1,3]],"date-time":"2025-01-03T00:00:00Z","timestamp":1735862400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,3]],"date-time":"2025-01-03T00:00:00Z","timestamp":1735862400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"PRIN project \u201cSEDUCE\u201d","award":["2017TWRCNB"],"award-info":[{"award-number":["2017TWRCNB"]}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["FA8750-16-C-0011"],"award-info":[{"award-number":["FA8750-16-C-0011"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-16-C-0011"],"award-info":[{"award-number":["FA8750-16-C-0011"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"name":"PRIN project \u201cITMaTTerS\u201d","award":["2017FTXR7S"],"award-info":[{"award-number":["2017FTXR7S"]}]},{"name":"PRIN project \u201cFluidware\u201d","award":["2017KRC7KT"],"award-info":[{"award-number":["2017KRC7KT"]}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0011"],"award-info":[{"award-number":["FA8750-16-C-0011"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,4]]},"DOI":"10.1007\/s10270-024-01217-6","type":"journal-article","created":{"date-parts":[[2025,1,3]],"date-time":"2025-01-03T09:49:06Z","timestamp":1735897746000},"page":"489-521","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Model-based verification of data protection mechanisms in collaborative business processes"],"prefix":"10.1007","volume":"24","author":[{"given":"Sara","family":"Belluccini","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rocco","family":"De Nicola","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marlon","family":"Dumas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pille","family":"Pullonen-Raudvere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Barbara","family":"Re","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,1,3]]},"reference":[{"key":"1217_CR1","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1016\/j.is.2013.12.006","volume":"47","author":"R Accorsi","year":"2015","unstructured":"Accorsi, R., Lehmann, A., Lohmann, N.: Information leak detection in business process models: theory, application, and tool support. Inf. Syst. 47, 244\u2013257 (2015)","journal-title":"Inf. Syst."},{"key":"1217_CR2","doi-asserted-by":"crossref","unstructured":"Agostinelli, S., Maggi, F.M., Marrella, A., Sapio, F.: Achieving GDPR compliance of BPMN process models. In: Information Systems Engineering in Responsible Information Systems\u2014CAiSE Forum 2019, Rome, Italy, June 3\u20137, 2019, Proceedings, pp. 10\u201322 (2019)","DOI":"10.1007\/978-3-030-21297-1_2"},{"key":"1217_CR3","doi-asserted-by":"crossref","unstructured":"Ahmadian, A.S., Str\u00fcber, D., J\u00fcrjens, J.: Privacy-enhanced system design modeling based on privacy features. In: Proceedings of the 34th ACM\/SIGAPP Symposium on Applied Computing, pp. 1492\u20131499 (2019)","DOI":"10.1145\/3297280.3297431"},{"key":"1217_CR4","doi-asserted-by":"crossref","unstructured":"Awad, A., Decker, G., Lohmann, N.: Diagnosing and repairing data anomalies in process models. In: Business Process Management Workshops, pp. 5\u201316. Springer (2010)","DOI":"10.1007\/978-3-642-12186-9_2"},{"key":"1217_CR5","doi-asserted-by":"crossref","unstructured":"Ayala-Rivera, V., Pasquale, L.: The grace period has ended: an approach to operationalize GDPR requirements. In: 26th IEEE International Requirements Engineering Conference, RE 2018, Banff, AB, Canada, August 20-24, 2018, pp. 136\u2013146 (2018)","DOI":"10.1109\/RE.2018.00023"},{"key":"1217_CR6","volume":"76","author":"M Bakhtina","year":"2023","unstructured":"Bakhtina, M., Matulevi\u010dius, R., Seeba, M.: Tool-supported method for privacy analysis of a business process model. J. Inf. Secur. Appl. 76, 103525 (2023)","journal-title":"J. Inf. Secur. Appl."},{"key":"1217_CR7","doi-asserted-by":"crossref","unstructured":"Belluccini, S., De\u00a0Nicola, R., Dumas, M., Pullonen, P., Re, B., Tiezzi, F.: Verification of privacy-enhanced collaborations. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering, pp. 141\u2013152 (2020)","DOI":"10.1145\/3372020.3391553"},{"key":"1217_CR8","doi-asserted-by":"crossref","unstructured":"Belluccini, S., De\u00a0Nicola, R., Re, B., Tiezzi, F.: Palm: a technique for process algebraic specification mining. In: International Conference on Integrated Formal Methods, pp. 397\u2013418. Springer (2020)","DOI":"10.1007\/978-3-030-63461-2_22"},{"issue":"1\u20133","key":"1217_CR9","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"JA Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1\u20133), 109\u2013137 (1984)","journal-title":"Inf. Control"},{"key":"1217_CR10","first-page":"211","volume":"62","author":"C Bodei","year":"2002","unstructured":"Bodei, C., Degano, P., Focardi, R., Gorrieri, R., Martinelli, F.: Techniques for security checking: non-interference vs control flow analysis. ENTCS 62, 211\u2013228 (2002)","journal-title":"ENTCS"},{"key":"1217_CR11","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., Thalheim, B.: A method for verifiable and validatable business process modeling. In: Advances in Software Engineering, LNCS, vol. 5316, pp. 59\u2013115. Springer (2008)","DOI":"10.1007\/978-3-540-89762-0_3"},{"key":"1217_CR12","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Yalman, S.: Confidentiality enhanced life-cycle assessment. In: International Conference on Business Process Management, pp. 434\u2013446. Springer (2021)","DOI":"10.1007\/978-3-030-94343-1_33"},{"key":"1217_CR13","doi-asserted-by":"crossref","unstructured":"Bunte, O., Groote, J.F., Keiren, J.J., Laveaux, M., Neele, T., de\u00a0Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.: The mCRL2 toolset for analysing concurrent systems. In: TACAS, LNCS, vol. 11428, pp. 21\u201339. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"1217_CR14","doi-asserted-by":"crossref","unstructured":"Capecchi, S., Castellani, I., Dezani-Ciancaglini, M., Rezk, T.: Session types for access and information flow control. In: CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, pp. 237\u2013252 (2010)","DOI":"10.1007\/978-3-642-15375-4_17"},{"key":"1217_CR15","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.trpro.2021.01.015","volume":"52","author":"C Caramuta","year":"2021","unstructured":"Caramuta, C., Giacomini, C., Longo, G., Montrone, T., Poloni, C., Ricco, L.: Integration of BPMN modeling and multi-actor AHP-aided evaluation to improve port rail operations. Transp. Res. Procedia 52, 139\u2013146 (2021)","journal-title":"Transp. Res. Procedia"},{"key":"1217_CR16","doi-asserted-by":"crossref","unstructured":"Carchiolo, V., Catalano, G., Malgeri, M., Pellegrino, C., Platania, G., Trapani, N.: Modelling and optimization of wind farms\u2019 processes using BPM. In: Information Technology for Management: Current Research and Future Directions, pp. 95\u2013115. Springer (2020)","DOI":"10.1007\/978-3-030-43353-6_6"},{"key":"1217_CR17","unstructured":"Castro, S., Teixeira, L.: BPMN and Lean Contributions for the ISO9001 implementation: a case study within the plastics industry. In: International Conference on Industrial Engineering and Operations Management, pp. 1228\u20131237. IEOM Society International (2020)"},{"issue":"3","key":"1217_CR18","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)","journal-title":"Softw. Syst. Model."},{"key":"1217_CR19","doi-asserted-by":"crossref","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: Bprove: a formal verification framework for business process models. In: ASE, pp. 217\u2013228. IEEE Computer Society (2017)","DOI":"10.1109\/ASE.2017.8115635"},{"key":"1217_CR20","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.datak.2017.11.003","volume":"113","author":"F Corradini","year":"2018","unstructured":"Corradini, F., Ferrari, A., Fornari, F., Gnesi, S., Polini, A., Re, B., Spagnolo, G.O.: A guidelines framework for understandable BPMN models. Data Knowl. Eng. 113, 129\u2013154 (2018)","journal-title":"Data Knowl. Eng."},{"key":"1217_CR21","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. Algebr. Methods Program. 119, 100630 (2021)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"1217_CR22","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2019.101459","volume":"103","author":"F Corradini","year":"2022","unstructured":"Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: Formalising and animating multiple instances in BPMN collaborations. Inf. Syst. 103, 101459 (2022)","journal-title":"Inf. Syst."},{"key":"1217_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2022.104322","volume":"160","author":"F Corradini","year":"2023","unstructured":"Corradini, F., Pettinari, S., Re, B., Rossi, L., Tiezzi, F.: A BPMN-driven framework for multi-robot system development. Robot. Auton. Syst. 160, 104322 (2023)","journal-title":"Robot. Auton. Syst."},{"key":"1217_CR24","doi-asserted-by":"publisher","unstructured":"Danezis, G., Domingo-Ferrer, J., Hansen, M., Hoepman, J.H., Metayer, D.L., Tirtea, R., Schiffner, S.: Privacy and data protection by design-from policy to engineering. Tech. rep., European Union Agency for Network and Information Security (2015https:\/\/doi.org\/10.2824\/38623","DOI":"10.2824\/38623"},{"key":"1217_CR25","unstructured":"de\u00a0la Croix, J.P., Lim, G.: Event-driven modeling and execution of robotic activities and contingencies in the Europa lander mission concept using BPMN. In: International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS). Universities Space Research Association (2020)"},{"key":"1217_CR26","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proceedings of the 12th international Conference on Database Theory, pp. 252\u2013267 (2009)","DOI":"10.1145\/1514894.1514924"},{"issue":"3","key":"1217_CR27","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2694428.2694430","volume":"43","author":"A Deutsch","year":"2014","unstructured":"Deutsch, A., Hull, R., Vianu, V.: Automatic verification of database-centric systems. ACM SIGMOD Rec. 43(3), 5\u201317 (2014)","journal-title":"ACM SIGMOD Rec."},{"issue":"12","key":"1217_CR28","doi-asserted-by":"publisher","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","volume":"50","author":"RM Dijkman","year":"2008","unstructured":"Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281\u20131294 (2008)","journal-title":"Inf. Softw. Technol."},{"issue":"2","key":"1217_CR29","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s10009-021-00636-w","volume":"24","author":"M Dumas","year":"2022","unstructured":"Dumas, M., Garc\u00eda-Ba\u00f1uelos, L., J\u00e4\u00e4ger, J., Laud, P., Matulevicius, R., Pankova, A., Pettai, M., Pullonen-Raudvere, P., Toots, A., Tuuling, R., Yerokhin, M.: Multi-level privacy analysis of business processes: the pleak toolset. Int. J. Softw. Tools Technol. Transf. 24(2), 183\u2013203 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1217_CR30","unstructured":"Elkoumy, G., Fahrenkrog-Petersen, S.A., Dumas, M., Laud, P., Pankova, A., Weidlich, M.: Shareprom: A tool for privacy-preserving inter-organizational process mining. In: BPM (PhD\/Demos), CEUR Workshop Proceedings, vol. 2673, pp. 72\u201376. CEUR-WS.org (2020)"},{"key":"1217_CR31","doi-asserted-by":"crossref","unstructured":"Elkoumy, G., Fahrenkrog-Petersen, S.A., Sani, M.F., Koschmider, A., Mannhardt, F., von Voigt, S.N., Rafiei, M., von Waldthausen, L.: Privacy and confidentiality in process mining: threats and research challenges. ACM Trans. Manag. Inf. Syst. 13(1), 11:1-11:17 (2022)","DOI":"10.1145\/3468877"},{"key":"1217_CR32","doi-asserted-by":"crossref","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, July 22\u201322, 2014, p.\u00a01 (2014)","DOI":"10.1145\/2630768.2630769"},{"key":"1217_CR33","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1016\/j.procs.2021.12.043","volume":"196","author":"I Essefi","year":"2022","unstructured":"Essefi, I., Rahmouni, H.B., Ladeb, M.F.: Integrated privacy decision in BPMN clinical care pathways models using DMN. Procedia Comput. Sci. 196, 509\u2013516 (2022)","journal-title":"Procedia Comput. Sci."},{"key":"1217_CR34","doi-asserted-by":"publisher","unstructured":"Fedele, C., Butler, K., Petersen, C., Lovelly, T.: Protecting satellite proximity operations via secure multi-party computation. In: AIAA SCITECH 2024 Forum (2024). https:\/\/doi.org\/10.2514\/6.2024-0271","DOI":"10.2514\/6.2024-0271"},{"key":"1217_CR35","unstructured":"Fellman, M., Zasada, A.: State of the art of business process compliance approaches: a survey. In: Information Systems (2014)"},{"key":"1217_CR36","doi-asserted-by":"crossref","unstructured":"Gl\u00f6ckner, M., Schwarzbach, B., Makarov, S., Franczyk, B., Ludwig, A.: Privacy preserving BPMS for collaborative BPaaS. In: 2017 Federated Conference on Computer Science and Information Systems (FedCSIS), pp. 925\u2013934. IEEE (2017)","DOI":"10.15439\/2017F330"},{"key":"1217_CR37","doi-asserted-by":"crossref","unstructured":"Groefsema, H., Bucur, D.: A survey of formal business process verification: from soundness to variability. In: Business Modeling and Software Design, pp. 198\u2013203 (2013)","DOI":"10.5220\/0004775401980203"},{"key":"1217_CR38","doi-asserted-by":"crossref","unstructured":"Groefsema, H., van Beest, N.: Design-time compliance of service compositions in dynamic service environments. In: 2015 IEEE 8th International Conference on Service-Oriented Computing and Applications (SOCA), pp. 108\u2013115. IEEE (2015)","DOI":"10.1109\/SOCA.2015.14"},{"issue":"3","key":"1217_CR39","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1109\/TSC.2016.2579621","volume":"11","author":"H Groefsema","year":"2016","unstructured":"Groefsema, H., van Beest, N.R., Aiello, M.: A formal model for compliance verification of service compositions. IEEE Trans. Serv. Comput. 11(3), 466\u2013479 (2016)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"1217_CR40","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"1217_CR41","doi-asserted-by":"crossref","unstructured":"Houhou, S., Baarir, S., Poizat, P., Qu\u00e9innec, P.: A first-order logic semantics for communication-parametric BPMN collaborations. In: International Conference on Business Process Management, pp. 52\u201368. Springer (2019)","DOI":"10.1007\/978-3-030-26619-6_6"},{"key":"1217_CR42","doi-asserted-by":"publisher","unstructured":"Huai, W., Liu, X., Sun, H.: Towards trustworthy composite service through business process model verification. In: 2010 7th International Conference on Ubiquitous Intelligence & Computing and 7th International Conference on Autonomic & Trusted Computing, pp. 422\u2013427 (2010). https:\/\/doi.org\/10.1109\/UIC-ATC.2010.114","DOI":"10.1109\/UIC-ATC.2010.114"},{"issue":"6","key":"1217_CR43","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10207-014-0271-8","volume":"14","author":"L Kamm","year":"2015","unstructured":"Kamm, L., Willemson, J.: Secure floating point arithmetic and private satellite collision analysis. Int. J. Inf. Secur. 14(6), 531\u2013548 (2015)","journal-title":"Int. J. Inf. Secur."},{"key":"1217_CR44","doi-asserted-by":"crossref","unstructured":"Kherbouche, O.M., Ahmad, A., Basson, H.: Using model checking to control the structural errors in BPMN models. In: IEEE 7th International Conference on Research Challenges in Information Science (RCIS), pp. 1\u201312. IEEE (2013)","DOI":"10.1109\/RCIS.2013.6577723"},{"key":"1217_CR45","doi-asserted-by":"crossref","unstructured":"Kiepuszewski, B., ter Hofstede, A.H.M., Bussler, C.J.: On structured workflow modelling. In: Advanced Information Systems Engineering, pp. 431\u2013445. Springer (2000)","DOI":"10.1007\/3-540-45140-4_29"},{"key":"1217_CR46","doi-asserted-by":"crossref","unstructured":"Koniewski, R., Dzielinski, A., Amborski, K.: Use of petri nets and business processes management notation in modelling and simulation of multimodal logistics chains. In: 20th European Conference on Modeling and Simulation, pp. 28\u201331. Warsaw (2006)","DOI":"10.7148\/2006-0099"},{"issue":"5","key":"1217_CR47","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s00165-009-0106-y","volume":"21","author":"C Masalagiu","year":"2009","unstructured":"Masalagiu, C., Chin, W.N., Andrei, \u015e, Alaiba, V.: A rigorous methodology for specification and verification of business processes. Formal Aspects Comput. 21(5), 495\u2013510 (2009)","journal-title":"Formal Aspects Comput."},{"key":"1217_CR48","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2020.110587","volume":"166","author":"J Mass","year":"2020","unstructured":"Mass, J., Srirama, S.N., Chang, C.: Step-one: simulated testbed for edge-fog processes based on the opportunistic network environment simulator. J. Syst. Softw. 166, 110587 (2020)","journal-title":"J. Syst. Softw."},{"issue":"5","key":"1217_CR49","doi-asserted-by":"publisher","first-page":"1101","DOI":"10.1108\/BPMJ-09-2017-0241","volume":"25","author":"S Mazhar","year":"2019","unstructured":"Mazhar, S., Wu, P.P., Rosemann, M.: Designing complex socio-technical process systems: the airport example. Bus. Process. Manag. J. 25(5), 1101\u20131125 (2019)","journal-title":"Bus. Process. Manag. J."},{"key":"1217_CR50","unstructured":"mCRL2 - analysing system behaviour. https:\/\/www.mcrl2.org\/"},{"key":"1217_CR51","unstructured":"mcrl22lps. https:\/\/www.mcrl2.org\/web\/user_manual\/tools\/release\/mcrl22lps.html"},{"issue":"2","key":"1217_CR52","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.infsof.2009.08.004","volume":"52","author":"J Mendling","year":"2010","unstructured":"Mendling, J., Reijers, H.A., van der Aalst, W.M.: Seven process modeling guidelines. Inf. Softw. Technol. 52(2), 127\u2013136 (2010)","journal-title":"Inf. Softw. Technol."},{"key":"1217_CR53","doi-asserted-by":"crossref","unstructured":"Morimoto, S.: A survey of formal verification for business process modeling. In: Computational Science, LNCS, vol. 5102, pp. 514\u2013522. Springer (2008)","DOI":"10.1007\/978-3-540-69387-1_58"},{"key":"1217_CR54","unstructured":"Nake, L.: Integrating IT security aspects into business process models: a taxonomy of BPMN extensions. In: Kuehnel, S., Nastjuk, I., Sackmann, S., Trang, S. (eds.) Proceedings of the 3rd International Workshop on Current Information Security and Compliance Issues in Information Systems Research (CIISR 2023) Co-located with the 18th International Conference on Wirtschaftsinformatik (WI 2023), Paderborn, Germany, September 18, 2023, CEUR Workshop Proceedings, vol. 3512, pp. 38\u201348. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3512\/fullpaper3.pdf"},{"key":"1217_CR55","unstructured":"OMG: Business Process Model and Notation (BPMN 2.0) (2011). https:\/\/www.omg.org\/spec\/BPMN\/2.0\/"},{"key":"1217_CR56","unstructured":"Pleak - privacy leakage analysis tools. https:\/\/pleak.io\/home"},{"issue":"2","key":"1217_CR57","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1051\/ita\/2012002","volume":"46","author":"A Polini","year":"2012","unstructured":"Polini, A., Polzonetti, A., Re, B.: Formal methods to improve public administration business processes. RAIRO - Theor. Inf. Appl. 46(2), 203\u2013229 (2012)","journal-title":"RAIRO - Theor. Inf. Appl."},{"key":"1217_CR58","doi-asserted-by":"crossref","unstructured":"Polyvyanyy, A., Vanhatalo, J., V\u00f6lzer, H.: Simplified computation and generalization of the refined process structure tree. In: International Workshop on Web Services and Formal Methods, pp. 25\u201341. Springer (2010)","DOI":"10.1007\/978-3-642-19589-1_2"},{"issue":"6","key":"1217_CR59","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1016\/j.is.2011.10.005","volume":"37","author":"A Polyvyanyy","year":"2012","unstructured":"Polyvyanyy, A., Garc\u00eda-Ba\u00f1uelos, L., Dumas, M.: Structuring acyclic process models. Inf. Syst. 37(6), 518\u2013538 (2012)","journal-title":"Inf. Syst."},{"key":"1217_CR60","doi-asserted-by":"crossref","unstructured":"Prandi, D., Quaglia, P., Zannone, N.: Formal analysis of BPMN via a translation into COWS. In: COORDINATION, LNCS, vol. 5052, pp. 249\u2013263 (2008)","DOI":"10.1007\/978-3-540-68265-3_16"},{"key":"1217_CR61","doi-asserted-by":"crossref","unstructured":"Prandi, D., Quaglia, P., Zannone, N.: Formal analysis of BPMN via a translation into COWS. In: Coordination Models and Languages, pp. 249\u2013263. Springer (2008)","DOI":"10.1007\/978-3-540-68265-3_16"},{"key":"1217_CR62","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2022.102013","volume":"107","author":"L Pufahl","year":"2022","unstructured":"Pufahl, L., Zerbato, F., Weber, B., Weber, I.: BPMN in healthcare: challenges and best practices. Inf. Syst. 107, 102013 (2022)","journal-title":"Inf. Syst."},{"key":"1217_CR63","doi-asserted-by":"crossref","unstructured":"Pullonen, P., Matulevi\u010dius, R., Bogdanov, D.: PE-BPMN: privacy-enhanced business process model and notation. In: BPM, LNCS, vol. 10445, pp. 40\u201356. Springer (2017)","DOI":"10.1007\/978-3-319-65000-5_3"},{"issue":"6","key":"1217_CR64","doi-asserted-by":"publisher","first-page":"3235","DOI":"10.1007\/s10270-019-00718-z","volume":"18","author":"P Pullonen","year":"2019","unstructured":"Pullonen, P., Tom, J., Matulevicius, R., Toots, A.: Privacy-enhanced BPMN: enabling data privacy analysis in business processes models. Softw. Syst. Model. 18(6), 3235\u20133264 (2019)","journal-title":"Softw. Syst. Model."},{"key":"1217_CR65","unstructured":"Ramadan, M., Elmongui, H.G., Hassan, R.: BPMN formalisation using coloured petri nets. In: International Conference on Software Engineering and Applications (2011)"},{"issue":"4","key":"1217_CR66","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1093\/ietisy\/e90-d.4.745","volume":"90","author":"A Rodr\u00edguez","year":"2007","unstructured":"Rodr\u00edguez, A., Fern\u00e1ndez-Medina, E., Piattini, M.: A BPMN extension for the modeling of security requirements in business processes. IEICE Trans. Inf. Syst. 90(4), 745\u2013752 (2007)","journal-title":"IEICE Trans. Inf. Syst."},{"issue":"3","key":"1217_CR67","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/s10270-015-0499-4","volume":"16","author":"M Salnitri","year":"2017","unstructured":"Salnitri, M., Dalpiaz, F., Giorgini, P.: Designing secure business processes with SecBPMN. Softw. Syst. Model. 16(3), 737\u2013757 (2017)","journal-title":"Softw. Syst. Model."},{"key":"1217_CR68","doi-asserted-by":"crossref","unstructured":"Sang, K.S., Zhou, B.: BPMN security extensions for healthcare process. In: CIT\/IUCC\/DASC\/PICom, pp. 2340\u20132345. IEEE (2015)","DOI":"10.1109\/CIT\/IUCC\/DASC\/PICOM.2015.346"},{"key":"1217_CR69","doi-asserted-by":"crossref","unstructured":"Scheuerlein, H., Rauchfuss, F., Dittmar, Y., et\u00a0al.: New methods for clinical pathways-Business Process Modeling Notation (BPMN) and Tangible Business Process Modeling (t.BPM). Langenbecks Arch. Surg 397, 755\u2013761 (2012)","DOI":"10.1007\/s00423-012-0914-z"},{"key":"1217_CR70","unstructured":"Seeliger, A., Nolle, T., Schmidt, B., M\u00fchlh\u00e4user, M.: Process compliance checking using taint flow analysis. In: ICIS. Association for Information Systems (2016)"},{"key":"1217_CR71","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.csi.2017.11.007","volume":"58","author":"A Souri","year":"2018","unstructured":"Souri, A., Navimipour, N.J., Rahmani, A.M.: Formal verification approaches and standards in the cloud computing: a comprehensive and systematic review. Comput. Stand. Interfaces 58, 1\u201322 (2018)","journal-title":"Comput. Stand. Interfaces"},{"key":"1217_CR72","unstructured":"The jBPT library. https:\/\/github.com\/jbpt\/codebase"},{"key":"1217_CR73","doi-asserted-by":"crossref","unstructured":"Toots, A., Tuuling, R., Yerokhin, M., Dumas, M., Garc\u00eda-Ba\u00f1uelos, L., Laud, P., Matulevicius, R., Pankova, A., Pettai, M., Pullonen, P., Tom, J.: Business process privacy analysis in pleak. In: FASE, LNCS, vol. 11424, pp. 306\u2013312. Springer (2019)","DOI":"10.1007\/978-3-030-16722-6_18"},{"issue":"8","key":"1217_CR74","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1016\/S0306-4379(00)00003-X","volume":"24","author":"WMP van der Aalst","year":"1999","unstructured":"van der Aalst, W.M.P.: Process-oriented architectures for electronic commerce and interorganizational workflow. Inf. Syst. 24(8), 639\u2013671 (1999)","journal-title":"Inf. Syst."},{"key":"1217_CR75","doi-asserted-by":"crossref","unstructured":"van\u00a0der Aalst, W., van Hee, K.M., ter Hofstede Arthurand\u00a0Sidorova, N., Verbeek, H.M.W., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. Formal Asp. Comput. 23(3), 333\u2013363 (2011). http:\/\/link.springer.com\/article\/10.1007\/s00165-010-0161-4","DOI":"10.1007\/s00165-010-0161-4"},{"key":"1217_CR76","doi-asserted-by":"crossref","unstructured":"van\u00a0der Aalst, W.: Workflow verification: finding control-flow errors using petri-net-based techniques. In: Business Process Management, Models, Techniques, and Empirical Studies, LNCS, vol. 1806, pp. 161\u2013183. Springer (2000)","DOI":"10.1007\/3-540-45594-9_11"},{"issue":"9","key":"1217_CR77","doi-asserted-by":"publisher","first-page":"793","DOI":"10.1016\/j.datak.2009.02.015","volume":"68","author":"J Vanhatalo","year":"2009","unstructured":"Vanhatalo, J., V\u00f6lzer, H., Koehler, J.: The refined process structure tree. Data Knowl. Eng. 68(9), 793\u2013818 (2009)","journal-title":"Data Knowl. Eng."},{"issue":"8","key":"1217_CR78","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/j.scico.2009.09.010","volume":"76","author":"PYH Wong","year":"2011","unstructured":"Wong, P.Y.H., Gibbons, J.: Formalisations and applications of BPMN. Sci. Comput. Program. 76(8), 633\u2013650 (2011)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"1217_CR79","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1108\/14637150910931479","volume":"15","author":"MT Wynn","year":"2009","unstructured":"Wynn, M.T., Verbeek, H., van der Aalst, W.M., ter Hofstede, A.H., Edmond, D.: Business process verification-finally a reality! Bus. Process. Manag. J. 15(1), 74\u201392 (2009)","journal-title":"Bus. Process. Manag. J."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01217-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01217-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01217-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T11:13:17Z","timestamp":1746011597000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01217-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,3]]},"references-count":79,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["1217"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01217-6","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,3]]},"assertion":[{"value":"17 May 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 August 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 January 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}