{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,19]],"date-time":"2025-11-19T19:26:14Z","timestamp":1763580374555,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T00:00:00Z","timestamp":1602028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,7]]},"DOI":"10.1145\/3372020.3391553","type":"proceedings-article","created":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T20:02:05Z","timestamp":1599940925000},"page":"141-152","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Verification of Privacy-Enhanced Collaborations"],"prefix":"10.1145","author":[{"given":"Sara","family":"Belluccini","sequence":"first","affiliation":[{"name":"IMT School for Advanced Studies, Lucca, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rocco","family":"De Nicola","sequence":"additional","affiliation":[{"name":"IMT School for Advanced Studies, Lucca, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marlon","family":"Dumas","sequence":"additional","affiliation":[{"name":"University of Tartu, Tartu, Estonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pille","family":"Pullonen","sequence":"additional","affiliation":[{"name":"Cybernetica AS, Tallinn, Estonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Re","sequence":"additional","affiliation":[{"name":"University of Camerino, Camerino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[{"name":"University of Camerino, Camerino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. mCKL2 - analysing system behaviour https:\/\/www.mcrl2.org\/  [n.d.]. mCKL2 - analysing system behaviour https:\/\/www.mcrl2.org\/"},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. PLEAK - Privacy Leakage Analysis Tools https:\/\/pleak.io\/home  [n.d.]. PLEAK - Privacy Leakage Analysis Tools https:\/\/pleak.io\/home"},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. The jBPT library https:\/\/github.com\/jbpt\/codebase  [n.d.]. The jBPT library https:\/\/github.com\/jbpt\/codebase"},{"key":"e_1_3_2_1_4_1","unstructured":"2010. Towards Trustworthy Composite Service Through Business Process Model Verification. 422--427.  2010. Towards Trustworthy Composite Service Through Business Process Model Verification. 422--427."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2013.12.006"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-21297-1_2"},{"key":"e_1_3_2_1_7_1","volume-title":"Diagnosing and Repairing Data Anomalies in Process Models. In Business Process Management Workshops. Springer, 5--16","author":"Awad Ahmed","year":"2010","unstructured":"Ahmed Awad , Gero Decker , and Niels Lohmann . 2010 . Diagnosing and Repairing Data Anomalies in Process Models. In Business Process Management Workshops. Springer, 5--16 . Ahmed Awad, Gero Decker, and Niels Lohmann. 2010. Diagnosing and Repairing Data Anomalies in Process Models. In Business Process Management Workshops. Springer, 5--16."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2018.00023"},{"key":"e_1_3_2_1_9_1","volume-title":"Process algebra for synchronous communication. Information and control 60, 1-3","author":"Bergstra Jan A","year":"1984","unstructured":"Jan A Bergstra and Jan Willem Klop . 1984. Process algebra for synchronous communication. Information and control 60, 1-3 ( 1984 ), 109--137. Jan A Bergstra and Jan Willem Klop. 1984. Process algebra for synchronous communication. Information and control 60, 1-3 (1984), 109--137."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00328-7"},{"volume-title":"Advances in Software Engineering. LNCS","author":"B\u00f6rger Egon","key":"e_1_3_2_1_11_1","unstructured":"Egon B\u00f6rger and Bernhard Thalheim . 2008. A method for verifiable and validatable business process modeling . In Advances in Software Engineering. LNCS , Vol. 5316 . Springer , 59--115. Egon B\u00f6rger and Bernhard Thalheim. 2008. A method for verifiable and validatable business process modeling. In Advances in Software Engineering. LNCS, Vol. 5316. Springer, 59--115."},{"key":"e_1_3_2_1_12_1","volume-title":"Jeroen JA Keiren, Maurice Laveaux, Thomas Neele, Erik P de Vink, Wieger Wesselink, Anton Wijs, and Tim AC Willemse.","author":"Bunte Olav","year":"2019","unstructured":"Olav Bunte , Jan Friso Groote , Jeroen JA Keiren, Maurice Laveaux, Thomas Neele, Erik P de Vink, Wieger Wesselink, Anton Wijs, and Tim AC Willemse. 2019 . The mCRL2 Toolset for Analysing Concurrent Systems. In TACAS (LNCS), Vol. 11428 . Springer , 21--39. Olav Bunte, Jan Friso Groote, Jeroen JA Keiren, Maurice Laveaux, Thomas Neele, Erik P de Vink, Wieger Wesselink, Anton Wijs, and Tim AC Willemse. 2019. The mCRL2 Toolset for Analysing Concurrent Systems. In TACAS (LNCS), Vol. 11428. Springer, 21--39."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_17"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2017.11.003"},{"volume-title":"BPrdVe: a formal verification framework for business process models","author":"Corradini Flavio","key":"e_1_3_2_1_15_1","unstructured":"Flavio Corradini , Fabrizio Fornari , Andrea Polini , Barbara Re , Francesco Tiezzi , and Andrea Vandin . 2017. BPrdVe: a formal verification framework for business process models . In ASE. IEEE Computer Society , 217--228. Flavio Corradini, Fabrizio Fornari, Andrea Polini, Barbara Re, Francesco Tiezzi, and Andrea Vandin. 2017. BPrdVe: a formal verification framework for business process models. In ASE. IEEE Computer Society, 217--228."},{"key":"e_1_3_2_1_16_1","volume-title":"Rodica Tirtea, and Stefan Schiffner.","author":"Danezis George","year":"2015","unstructured":"George Danezis , Josep Domingo-Ferrer , Marit Hansen , Jaap-Henk Hoepman , Daniel Le Metayer , Rodica Tirtea, and Stefan Schiffner. 2015 . Privacy and data protection by design-from policy to engineering. arXiv preprint arXiv:1501.03726 (2015). George Danezis, Josep Domingo-Ferrer, Marit Hansen, Jaap-Henk Hoepman, Daniel Le Metayer, Rodica Tirtea, and Stefan Schiffner. 2015. Privacy and data protection by design-from policy to engineering. arXiv preprint arXiv:1501.03726 (2015)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.02.006"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 2014 Workshop on Behaviour Modelling - Foundations and Applications, BM-FA 2014","author":"Nissreen A.","year":"2014","unstructured":"Nissreen A. S. El-Saber and Artur Boronat. 2014. 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-22, 2014 . 1. Nissreen A. S. El-Saber and Artur Boronat. 2014. 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-22, 2014. 1."},{"key":"e_1_3_2_1_19_1","unstructured":"Michael Fellman and Andrea Zasada. 2014. State of the Art of Business Process Compliance Approaches: A Survey. In Information Systems.  Michael Fellman and Andrea Zasada. 2014. State of the Art of Business Process Compliance Approaches: A Survey. In Information Systems."},{"key":"e_1_3_2_1_20_1","unstructured":"Heerko Groefsema and Doina Bucur. 2013. A survey of formal business process verification: From soundness to variability. In Business Modeling and Software Design. 198--203.  Heerko Groefsema and Doina Bucur. 2013. A survey of formal business process verification: From soundness to variability. In Business Modeling and Software Design. 198--203."},{"volume-title":"Modeling and analysis of communicating systems","author":"Groote Jan Friso","key":"e_1_3_2_1_21_1","unstructured":"Jan Friso Groote and Mohammad Reza Mousavi . 2014. Modeling and analysis of communicating systems . MIT press . Jan Friso Groote and Mohammad Reza Mousavi. 2014. Modeling and analysis of communicating systems. MIT press."},{"key":"e_1_3_2_1_22_1","volume-title":"Arthur Harry Maria ter Hofstede, and Christoph J. Bussler","author":"Kiepuszewski Bartek","year":"2000","unstructured":"Bartek Kiepuszewski , Arthur Harry Maria ter Hofstede, and Christoph J. Bussler . 2000 . On structured workflow modelling. Springer , 431--445. Bartek Kiepuszewski, Arthur Harry Maria ter Hofstede, and Christoph J. Bussler. 2000. On structured workflow modelling. Springer, 431--445."},{"key":"e_1_3_2_1_23_1","volume-title":"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","author":"Koniewski Ryszard","year":"2006","unstructured":"Ryszard Koniewski , Andrzej Dzielinski , and Krzysztof Amborski . 2006 . 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 . Warsaw, 28--31. Ryszard Koniewski, Andrzej Dzielinski, and Krzysztof Amborski. 2006. 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. Warsaw, 28--31."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0106-y"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2009.08.004"},{"volume-title":"Computational Science (LNCS)","author":"Morimoto Shoichi","key":"e_1_3_2_1_26_1","unstructured":"Shoichi Morimoto . 2008. A Survey of Formal Verification for Business Process Modeling . In Computational Science (LNCS) , Vol. 5102 . Springer , 514--522. Shoichi Morimoto. 2008. A Survey of Formal Verification for Business Process Modeling. In Computational Science (LNCS), Vol. 5102. Springer, 514--522."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012002"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2011.10.005"},{"key":"e_1_3_2_1_29_1","volume-title":"International Workshop on Web Services and Formal Methods. Springer, 25--41","author":"Polyvyanyy Artem","year":"2010","unstructured":"Artem Polyvyanyy , Jussi Vanhatalo , and Hagen V\u00f6lzer . 2010 . Simplified computation and generalization of the refined process structure tree . In International Workshop on Web Services and Formal Methods. Springer, 25--41 . Artem Polyvyanyy, Jussi Vanhatalo, and Hagen V\u00f6lzer. 2010. Simplified computation and generalization of the refined process structure tree. In International Workshop on Web Services and Formal Methods. Springer, 25--41."},{"key":"e_1_3_2_1_30_1","first-page":"249","article-title":"Formal Analysis of BPMN Via a Translation into COWS","volume":"5052","author":"Prandi Davide","year":"2008","unstructured":"Davide Prandi , Paola Quaglia , and Nicola Zannone . 2008 . Formal Analysis of BPMN Via a Translation into COWS . In COORDINATION (LNCS) , Vol. 5052. 249 -- 263 . Davide Prandi, Paola Quaglia, and Nicola Zannone. 2008. Formal Analysis of BPMN Via a Translation into COWS. In COORDINATION (LNCS), Vol. 5052. 249--263.","journal-title":"COORDINATION (LNCS)"},{"volume-title":"Coordination Models and Languages","author":"Prandi Davide","key":"e_1_3_2_1_31_1","unstructured":"Davide Prandi , Paola Quaglia , and Nicola Zannone . 2008. Formal Analysis of BPMN Via a Translation into COWS . In Coordination Models and Languages . Springer , 249--263. Davide Prandi, Paola Quaglia, and Nicola Zannone. 2008. Formal Analysis of BPMN Via a Translation into COWS. In Coordination Models and Languages. Springer, 249--263."},{"volume-title":"BPM (LNCS)","author":"Pullonen Pille","key":"e_1_3_2_1_32_1","unstructured":"Pille Pullonen , Raimundas Matulevi\u010dius , and Dan Bogdanov . 2017. PEBPMN: privacy-enhanced business process model and notation . In BPM (LNCS) , Vol. 10445 . Springer , 40--56. Pille Pullonen, Raimundas Matulevi\u010dius, and Dan Bogdanov. 2017. PEBPMN: privacy-enhanced business process model and notation. In BPM (LNCS), Vol. 10445. Springer, 40--56."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-019-00718-z"},{"key":"e_1_3_2_1_34_1","volume-title":"International Conference on Software Engineering & Applications.","author":"Ramadan Mohamed","year":"2011","unstructured":"Mohamed Ramadan , Hicham G. Elmongui , and Riham Hassan 2011 . BPMN formalisation using coloured petri nets . In International Conference on Software Engineering & Applications. Mohamed Ramadan, Hicham G. Elmongui, and Riham Hassan 2011. BPMN formalisation using coloured petri nets. In International Conference on Software Engineering & Applications."},{"key":"e_1_3_2_1_35_1","volume-title":"A BPMN extension for the modeling of security requirements in business processes. IEICE transactions on information and systems 90, 4","author":"Rodr\u00edguez Alfonso","year":"2007","unstructured":"Alfonso Rodr\u00edguez , Eduardo Fern\u00e1ndez-Medina , and Mario Piattini . 2007. A BPMN extension for the modeling of security requirements in business processes. IEICE transactions on information and systems 90, 4 ( 2007 ), 745--752. Alfonso Rodr\u00edguez, Eduardo Fern\u00e1ndez-Medina, and Mario Piattini. 2007. A BPMN extension for the modeling of security requirements in business processes. IEICE transactions on information and systems 90, 4 (2007), 745--752."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0499-4"},{"volume-title":"CIT\/IUCC\/DASC\/PICom","author":"Sang Koh Song","key":"e_1_3_2_1_37_1","unstructured":"Koh Song Sang and Bo Zhou . 2015. BPMN security extensions for healthcare process . In CIT\/IUCC\/DASC\/PICom . IEEE , 2340--2345. Koh Song Sang and Bo Zhou. 2015. BPMN security extensions for healthcare process. In CIT\/IUCC\/DASC\/PICom. IEEE, 2340--2345."},{"volume-title":"Process compliance checking using taint flow analysis","author":"Seeliger Alexander","key":"e_1_3_2_1_38_1","unstructured":"Alexander Seeliger , Timo Nolle , Benedikt Schmidt , and Max M\u00fchlh\u00e1user . 2016. Process compliance checking using taint flow analysis . In ICIS. Association for Information Systems . Alexander Seeliger, Timo Nolle, Benedikt Schmidt, and Max M\u00fchlh\u00e1user. 2016. Process compliance checking using taint flow analysis. In ICIS. Association for Information Systems."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2017.11.007"},{"volume-title":"FASE (LNCS)","author":"Toots Aivo","key":"e_1_3_2_1_40_1","unstructured":"Aivo Toots , Reedik Tuuling , Maksym Yerokhin , Marlon Dumas , Luciano Garc\u00eda-Ba\u00f1uelos , Peeter Laud , Raimundas Matulevicius , Alisa Pankova , Martin Pettai , Pille Pullonen , and Jake Tom . 2019. Business Process Privacy Analysis in Pleak . In FASE (LNCS) , Vol. 11424 . Springer , 306--312. Aivo Toots, Reedik Tuuling, Maksym Yerokhin, Marlon Dumas, Luciano Garc\u00eda-Ba\u00f1uelos, Peeter Laud, Raimundas Matulevicius, Alisa Pankova, Martin Pettai, Pille Pullonen, and Jake Tom. 2019. Business Process Privacy Analysis in Pleak. In FASE (LNCS), Vol. 11424. Springer, 306--312."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/337919.337921"},{"key":"e_1_3_2_1_42_1","volume-title":"Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques. In Business Process Management, Models, Techniques, and Empirical Studies. LNCS","author":"van der Aalst W.M.P.","year":"2000","unstructured":"W.M.P. van der Aalst . 2000 . Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques. In Business Process Management, Models, Techniques, and Empirical Studies. LNCS , Vol. 1806 . Springer , 161--183. W.M.P. van der Aalst. 2000. Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques. In Business Process Management, Models, Techniques, and Empirical Studies. LNCS, Vol. 1806. Springer, 161--183."},{"key":"e_1_3_2_1_43_1","first-page":"333","article-title":"Soundness of workflow nets: classification, decidability, and analysis","volume":"23","author":"van der Aalst WM.P.","year":"2011","unstructured":"WM.P. van der Aalst , K. van Hee , A ter Hofstede , N. Sidorova , H. Verbeek , M. Voorhoeve , and M. Wynn . 2011 . Soundness of workflow nets: classification, decidability, and analysis . FAC 23 , 3 (2011), 333 -- 363 . WM.P. van der Aalst, K. van Hee, A ter Hofstede, N. Sidorova, H. Verbeek, M. Voorhoeve, and M. Wynn. 2011. Soundness of workflow nets: classification, decidability, and analysis. FAC 23, 3 (2011), 333--363.","journal-title":"FAC"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2009.02.015"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.09.010"}],"event":{"name":"FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Seoul Republic of Korea","acronym":"FormaliSE '20"},"container-title":["Proceedings of the 8th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391553","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3372020.3391553","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372020.3391553","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372020.3391553","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:19Z","timestamp":1750203859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391553"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":45,"alternative-id":["10.1145\/3372020.3391553","10.1145\/3372020"],"URL":"https:\/\/doi.org\/10.1145\/3372020.3391553","relation":{},"subject":[],"published":{"date-parts":[[2020,10,7]]},"assertion":[{"value":"2020-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}