{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:14:02Z","timestamp":1742991242328,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572586"},{"type":"electronic","value":"9783031572593"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A business process is a collection of structured tasks corresponding to a service or a product. Business processes do not execute once and for all, but are executed multiple times resulting in multiple instances. In this context, it is particularly difficult to ensure correctness and efficiency of the multiple executions of a process. In this paper, we propose to rely on Probabilistic Model Checking (PMC) to automatically verify that multiple executions of a process respect some specific probabilistic property. This approach applies at runtime, thus the evaluation of the property is periodically verified and the corresponding results updated. However, we go beyond runtime PMC for BPMN, since we propose runtime enforcement techniques to keep executing the process while avoiding the violation of the property. To do so, our approach combines monitoring techniques, computation of probabilistic models, PMC, and runtime enforcement techniques. The approach has been implemented as a toolchain and has been validated on several realistic BPMN processes.<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_3","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"56-76","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Probabilistic Runtime Enforcement of Executable BPMN Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0114-0641","authenticated-orcid":false,"given":"Yli\u00e8s","family":"Falcone","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3654-8791","authenticated-orcid":false,"given":"Gwen","family":"Sala\u00fcn","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8396-5886","authenticated-orcid":false,"given":"Ahang","family":"Zuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On Runtime Enforcement via Suppressions. In: 29th International Conference on Concurrency Theory (CONCUR 2018). pp. 34:1\u201334:17. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.34","key":"3_CR1"},{"unstructured":"Activiti: Open source business automation (accessed December 2021), https:\/\/www.activiti.org\/","key":"3_CR2"},{"doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. Lectures on Runtime Verification: Introductory and Advanced Topics pp. 1\u201333 (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1","key":"3_CR3","DOI":"10.1007\/978-3-319-75632-5_1"},{"doi-asserted-by":"crossref","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: Runtime Verification over Out-of-Order Streams. ACM Trans. Comput. Logic 21(1) (oct 2019). https:\/\/doi.org\/10.1145\/3355609","key":"3_CR4","DOI":"10.1145\/3355609"},{"doi-asserted-by":"crossref","unstructured":"Ceballos, H.G., Cantu, F.J.: Discovering causal relations in semantically-annotated probabilistic business process diagrams. In: Global Conference on Artificial Intelligence, GCAI. pp. 29\u201340 (2018). https:\/\/doi.org\/10.29007\/nd7r","key":"3_CR5","DOI":"10.29007\/nd7r"},{"doi-asserted-by":"crossref","unstructured":"Ceballos, H.G., Flores-Solorio, V., Garcia, J.P.: A probabilistic BPMN normal form to model and advise human activities. In: International Workshop on Engineering Multi-Agent Systems. pp. 51\u201369. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-26184-3_4","key":"3_CR6","DOI":"10.1007\/978-3-319-26184-3_4"},{"doi-asserted-by":"crossref","unstructured":"De\u00a0Masellis, R., Su, J.: Runtime enforcement of first-order LTL properties on data-aware business processes. In: Service-Oriented Computing: 11th International Conference, ICSOC 2013, Berlin, Germany, December 2-5, 2013, Proceedings 11. pp. 54\u201368. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-45005-1_5","key":"3_CR7","DOI":"10.1007\/978-3-642-45005-1_5"},{"doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Rocha, C., Sala\u00fcn, G.: Stochastic analysis of BPMN with time in rewriting logic. Science of Computer Programming 168, 1\u201317 (2018). https:\/\/doi.org\/10.1016\/j.scico.2018.08.007","key":"3_CR8","DOI":"10.1016\/j.scico.2018.08.007"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E., Jutla, C.S., Sistla, A.: On model checking for the mu-calculus and its fragments. Theoretical Computer Science 258(1), 491\u2013522 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00034-7","key":"3_CR9","DOI":"10.1016\/S0304-3975(00)00034-7"},{"unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Engineering dependable software systems pp. 141\u2013175 (2013). https:\/\/doi.org\/10.3233\/978-1-61499-207-3-141","key":"3_CR10"},{"doi-asserted-by":"crossref","unstructured":"Falcone, Y., J\u00e9ron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Sci. Comput. Program. 123, 2\u201341 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.02.008","key":"3_CR11","DOI":"10.1016\/j.scico.2016.02.008"},{"doi-asserted-by":"crossref","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.C., Richier, J.L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design 38, 223\u2013262 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0114-4","key":"3_CR12","DOI":"10.1007\/s10703-011-0114-4"},{"doi-asserted-by":"crossref","unstructured":"Falcone, Y., Pinisetty, S.: On the Runtime Enforcement of Timed Properties. In: Proceedings of the Runtime Verification 2019 conference, pp. 48\u201369. Springer (Oct 2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_4","key":"3_CR13","DOI":"10.1007\/978-3-030-32079-9_4"},{"doi-asserted-by":"crossref","unstructured":"Falcone, Y., Sala\u00fcn, G.: Runtime Enforcement with Reordering, Healing, and Suppression. In: SEFM 2021 - 19th IEEE International Conference on Software Engineering and Formal Methods. pp. 1\u201320. IEEE, Virtual, United Kingdom (Dec 2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_3","key":"3_CR14","DOI":"10.1007\/978-3-030-92124-8_3"},{"doi-asserted-by":"crossref","unstructured":"Falcone, Y., Sala\u00fcn, G., Zuo, A.: Probabilistic Model Checking of BPMN Processes at Runtime. In: iFM 2022 - International Conference on integrated Formal Methods. pp. 1\u201317. Lugano, Switzerland (Jun 2022). https:\/\/doi.org\/10.1007\/978-3-031-07727-2_11","key":"3_CR15","DOI":"10.1007\/978-3-031-07727-2_11"},{"doi-asserted-by":"crossref","unstructured":"Faqrizal, I., Sala\u00fcn, G.: Counting Bugs in Behavioural Models using Counterexample Analysis. In: FormaliSE 2022 - International Conference on Formal Methods in Software Engineering. pp. 1\u201311. Pittsburgh, United States (May 2022). https:\/\/doi.org\/10.1145\/3524482.3527647","key":"3_CR16","DOI":"10.1145\/3524482.3527647"},{"doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89\u2013107 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","key":"3_CR17","DOI":"10.1007\/s10009-012-0244-z"},{"doi-asserted-by":"crossref","unstructured":"Herbert, L., Sharp, R.: Precise quantitative analysis of probabilistic business process model and notation workflows. Journal of Computing and Information Science in Engineering 13(1), 011007 (2013). https:\/\/doi.org\/10.1115\/1.4023362","key":"3_CR18","DOI":"10.1115\/1.4023362"},{"doi-asserted-by":"crossref","unstructured":"Herbert, L.T., Sharp, R.: Quantitative analysis of probabilistic BPMN workflows. In: International Design Engineering Technical Conferences and Computers and Information in Engineering Conference. vol. 45011, pp. 509\u2013518. American Society of Mechanical Engineers (2012). https:\/\/doi.org\/10.1115\/DETC2012-70653","key":"3_CR19","DOI":"10.1115\/DETC2012-70653"},{"unstructured":"ISO\/IEC: International standard 19510, information technology - business process model and notation. (2013)","key":"3_CR20"},{"doi-asserted-by":"crossref","unstructured":"Krishna, A., Poizat, P., Sala\u00fcn, G.: VBPMN: Automated Verification of BPMN Processes. In: 13th International Conference on integrated Formal Methods (iFM 2017). Turin, Italy (Sep 2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_21","key":"3_CR21","DOI":"10.1007\/978-3-319-66845-1_21"},{"doi-asserted-by":"crossref","unstructured":"Krishna, A., Poizat, P., Sala\u00fcn, G.: Checking Business Process Evolution. Science of Computer Programming 170, 1\u201326 (Jan 2019). https:\/\/doi.org\/10.1016\/j.scico.2018.09.007","key":"3_CR22","DOI":"10.1016\/j.scico.2018.09.007"},{"doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1\u201328 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90030-6","key":"3_CR23","DOI":"10.1016\/0890-5401(91)90030-6"},{"doi-asserted-by":"crossref","unstructured":"Mateescu, R., Requeno, J.I.: On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators. International Journal on Software Tools for Technology Transfer 20(5), 563\u2013587 (Oct 2018). https:\/\/doi.org\/10.1007\/s10009-018-0499-0","key":"3_CR24","DOI":"10.1007\/s10009-018-0499-0"},{"doi-asserted-by":"crossref","unstructured":"Mateescu, R., Sala\u00fcn, G., Ye, L.: Quantifying the Parallelism in BPMN Processes using Model Checking. In: The 17th International ACM Sigsoft Symposium on Component-Based Software Engineering (CBSE 2014). Lille, France (Jun 2014). https:\/\/doi.org\/10.1145\/2602458.2602473","key":"3_CR25","DOI":"10.1145\/2602458.2602473"},{"doi-asserted-by":"crossref","unstructured":"Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Maibaum, T. (eds.) FM 2008. Lecture Notes in Computer Science, vol.\u00a05014, pp. 148\u2013164. Springer Verlag, Turku, Finland (May 2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_12","key":"3_CR26","DOI":"10.1007\/978-3-540-68237-0_12"},{"doi-asserted-by":"crossref","unstructured":"Poizat, P., Sala\u00fcn, G., Krishna, A.: Checking Business Process Evolution. In: 13th International Conference on Formal Aspects of Component Software (FACS). Besan\u00e7on, France (Oct 2016). https:\/\/doi.org\/10.1007\/978-3-319-57666-4_4","key":"3_CR27","DOI":"10.1007\/978-3-319-57666-4_4"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:02:03Z","timestamp":1712322123000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_3","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":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}