{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T13:53:52Z","timestamp":1769608432466,"version":"3.49.0"},"reference-count":46,"publisher":"MDPI AG","issue":"12","license":[{"start":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T00:00:00Z","timestamp":1733356800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Lucian Blaga University of Sibiu, Romania"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"<jats:p>Workflows coordinate a series of computing tasks to create a sophisticated workflow logic. Ensuring the correctness of a workflow specification is essential for automating business processes. Errors in the specification should be identified and resolved as early as possible, during the design phase. In this paper, we propose a verification approach for workflow specifications utilizing model checking techniques. We introduce a method for verifying the correctness properties of workflow processes by utilizing our database-embedded Alternating-time Temporal Logic (ATL) model checker. First, the workflow specification is translated into a concurrent game structure (CGS). Next, the desired property is expressed as an ATL formula. Finally, the ATL model checker is executed to verify whether the correctness properties hold for the model. To support users in the formalization of business constraints, the proposed solution implements an assistant based on generative AI. The experimental results show that employing the chain-of-thought prompting method significantly enhances the reasoning process performance when using the GPT-4o model.<\/jats:p>","DOI":"10.3390\/info15120778","type":"journal-article","created":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T06:24:44Z","timestamp":1733379884000},"page":"778","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Business Constraints in Workflow-Based Applications"],"prefix":"10.3390","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9073-0781","authenticated-orcid":false,"given":"Florin","family":"Stoica","sequence":"first","affiliation":[{"name":"Department of Mathematics and Informatics, Faculty of Sciences, \u201cLucian Blaga\u201d University, 550024 Sibiu, Romania"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4758-6606","authenticated-orcid":false,"given":"Laura Florentina","family":"Stoica","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Informatics, Faculty of Sciences, \u201cLucian Blaga\u201d University, 550024 Sibiu, Romania"}]}],"member":"1968","published-online":{"date-parts":[[2024,12,5]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"46","DOI":"10.4204\/EPTCS.139.4","article-title":"Fluent LogicWorkflow Analyser: A Tool for The Verification of Workflow Properties","volume":"139","author":"Regis","year":"2014","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Su, G., and Liu, L. (2024). Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification. Future Internet, 16.","DOI":"10.3390\/fi16090319"},{"key":"ref_3","unstructured":"Dechsupa, C., Vatanawood, W., and Thongtak, A. (2019, January 13\u201315). Compositional Formal Verification for Business Process Models with Heterogeneous Notations Using Colored Petri Net. Proceedings of the International MultiConference of Engineers and Computer Scientists 2019, IMECS 2019, Hong Kong."},{"key":"ref_4","unstructured":"Mendoza, E.L., Capel, I.M., and P\u00e9rez, M. (2010, January 8\u20139). Compositional Verification of Business Processes by Model-Checking. Proceedings of the 8th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (ICEIS 2010), Funchal, Madeira, Portugal."},{"key":"ref_5","unstructured":"TechTarget (2024, October 16). Digital Process Automation. SearchCIO. Available online: https:\/\/www.techtarget.com\/searchcio\/definition\/digital-process-automation."},{"key":"ref_6","first-page":"157","article-title":"Business Process Modeled with BPMN and CTL Model Checking","volume":"12","author":"Ouazar","year":"2023","journal-title":"Int. J. Cybern. Inform."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Ougaabal, K., Zacharewicz, G., Ducq, Y., and Tazi, S. (2020). Visual Workflow Process Modeling and Simulation Approach Based on Non-Functional Properties of Resources. Appl. Sci., 10.","DOI":"10.3390\/app10134664"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Bussler, C., Hull, R., McIlraith, S., Orlowska, M.E., Pernici, B., and Yang, J. (2002, January 27\u201328). Formal Verification of e-Services and Workflows. Proceedings of the Web Services, E-Business, and the Semantic Web (WES 2002), Toronto, ON, Canada. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-36189-8"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Davulcu, H., Kifer, M., Ramakrishnan, C.R., and Ramakrishnan, I.V. (1998, January 1\u20133). Logic-Based Modeling and Analysis. Proceedings of the 17th ACM SIGART-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS 1998), Seattle, WA, USA.","DOI":"10.1145\/275487.275491"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Schroeder, M. (1999, January 9\u201311). Verification of Business Processes for a Correspondence Handling Center Using CCS. Proceedings of the European Symposium on Validation and Verification of Knowledge Based Systems and Components, Oslo, Norway.","DOI":"10.1007\/978-1-4757-6916-6_17"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., and Vandin, A. (November, January 30). BProVe: A Formal Verification Framework for Business Process Models. Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2017), Champaign, IL, USA.","DOI":"10.1109\/ASE.2017.8115635"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1108\/14637150910931479","article-title":"Business Process Verification\u2014Finally a Reality!","volume":"15","author":"Wynn","year":"2009","journal-title":"Bus. Process Manag. J."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"396","DOI":"10.4304\/jsw.5.4.396-404","article-title":"Transformation of BPMN Diagrams to YAWL Nets","volume":"5","author":"Ye","year":"2010","journal-title":"J. Softw."},{"key":"ref_14","first-page":"386","article-title":"Transforming BPMN Diagrams into YAWL Nets","volume":"Volume 5240","author":"Decker","year":"2008","journal-title":"Business Process Management"},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","article-title":"Semantics and Analysis of Business Process Models in BPMN","volume":"50","author":"Dijkman","year":"2008","journal-title":"Inf. Softw. Technol."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Huai, W., Liu, X., and Sun, H. (2010, January 26\u201329). Towards Trustworthy Composite Service Through Business Process Model Verification. Proceedings of the 7th International Conference on Ubiquitous Intelligence & Computing and 7th International Conference on Autonomic & Trusted Computing, Xi\u2019an, China.","DOI":"10.1109\/UIC-ATC.2010.114"},{"key":"ref_17","unstructured":"Koniewski, R., Dzielinski, A., and Amborski, K. (June, January 28). Use of Petri Nets and Business Processes Management Notation in Modelling and Simulation of Multimodal Logistics Chains. Proceedings of the 20th European Conference on Modeling and Simulation, G\u00f6rlitz, Germany."},{"key":"ref_18","unstructured":"Ramadan, M.Z., Elmongui, H.G., and Hassan, R. (2011, January 12\u201313). BPMN Formalisation using Coloured Petri Nets. Proceedings of the International Conference on Software Engineering & Applications (SEA 2011), Singapore."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-642-12186-9_2","article-title":"Diagnosing and Repairing Data Anomalies in Process Models","volume":"Volume 43","author":"Awad","year":"2010","journal-title":"Business Process Management Workshops"},{"key":"ref_20","first-page":"55","article-title":"Specification and Verification of Complex Business Processes\u2014A High-Level Petri Net-Based Approach","volume":"Volume 9253","author":"Kheldoun","year":"2015","journal-title":"Business Process Management"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.ins.2016.12.044","article-title":"Formal Verification of Complex Business Processes Based on High-Level Petri Nets","volume":"385\u2013386","author":"Kheldoun","year":"2017","journal-title":"Inf. Sci."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-540-88194-0_22","article-title":"A Process Semantics for BPMN","volume":"Volume 5256","author":"Wong","year":"2008","journal-title":"Formal Methods and Software Engineering"},{"key":"ref_23","unstructured":"Corradini, F., Polzonetti, A., Re, B., and Falcioni, D. (2010, January 13\u201319). An Eclipse Plug-in for Formal Verification of BPMN Processes. Proceedings of the 3rd International Conference on Communication Theory, Reliability, and Quality of Service, Athens, Greece."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1080\/10580530.2010.514164","article-title":"Business Processes Verification for e-Government Service Delivery","volume":"27","author":"Corradini","year":"2010","journal-title":"Inf. Syst. Manag."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1051\/ita\/2012002","article-title":"Formal Methods to Improve Public Administration Business Processes","volume":"46","author":"Polini","year":"2012","journal-title":"RAIRO-Theor. Inform. Appl."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"00012","DOI":"10.1051\/itmconf\/20246000012","article-title":"Advancing Verification of Process Mining Models with Quantitative Model Checking in Stochastic Environment","volume":"60","author":"Mangi","year":"2024","journal-title":"ITM Web Conf."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"987","DOI":"10.1142\/S0218194010005079","article-title":"Formal Analysis of BPMN Models: A NuSMV-Based Approach","volume":"20","author":"Lam","year":"2010","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"ref_28","first-page":"295","article-title":"Overview of Verification Tools for Business Process Models","volume":"13","author":"Suchenia","year":"2017","journal-title":"Ann. Comput. Sci. Inf. Syst."},{"key":"ref_29","first-page":"3","article-title":"Business Process Verification: The Application of Model Checking and Timed Automata","volume":"17","year":"2014","journal-title":"CLEI Electron. J."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Watahiki, K., Ishikawa, F., and Hiraishi, K. (2011, January 9\u201312). Formal Verification of Business Processes with Temporal and Resource Constraints. Proceedings of the 2011 IEEE International Conference on Systems, Man, and Cybernetics, Anchorage, AK, USA.","DOI":"10.1109\/ICSMC.2011.6083857"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Nguyen Thanh, T., Le Thanh, N., Hoang Thi Thanh, H., and Ha Thi, T. (2023, January 24\u201326). VeBPRu: A Toolchain for Formally Verifying Business Processes and Business Rules. Proceedings of the 2023 8th International Conference on Intelligent Information Technology (ICIIT 2023), Da Nang, Vietnam.","DOI":"10.1145\/3591569.3591572"},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1016\/j.procs.2017.08.002","article-title":"PrOnto: An Ontology Driven Business Process Mining Tool","volume":"112","author":"Bistarelli","year":"2017","journal-title":"Procedia Comput. Sci."},{"key":"ref_33","unstructured":"van Sinderen, M., and Maciaszek, L. (2019). Towards an Automatic Verification of BPMN Model Semantic Preservation During a Refinement Process. Software Technologies. ICSOFT 2018, Springer. Communications in Computer and Information Science."},{"key":"ref_34","unstructured":"Sales, T.P., Ara\u00fajo, J., Borbinha, J., and Guizzardi, G. (2023). FlowTGE: Automating Functional Testing of Executable Business Process Models Based on BPMN. Advances in Conceptual Modeling. ER 2023, Springer. Lecture Notes in Computer Science."},{"key":"ref_35","unstructured":"Groefsema, H., and Bucur, D. (2013, January 8\u201310). A Survey of Formal Business Process Verification: From Soundness to Variability. Proceedings of the Third International Symposium on Business Modeling and Software Design (BMSD 2013), Noordwijkerhout, The Netherlands."},{"key":"ref_36","unstructured":"Matthew Mulvaney (2024, October 16). Oracle APEX Tutorial. Available online: https:\/\/pretius.com\/blog\/oracle-apex-tutorial\/."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-Time Temporal Logic","volume":"49","author":"Alur","year":"2002","journal-title":"J. ACM"},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10458-005-0944-9","article-title":"Fully Symbolic Unbounded Model Checking for Alternating-Time Temporal Logic","volume":"11","author":"Kacprzak","year":"2005","journal-title":"Auton. Agents Multi-Agent Syst."},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"1125","DOI":"10.1142\/S0218194022500450","article-title":"ATLDesigner: ATL Model Checking Using an Attribute Grammar","volume":"32","author":"Stoica","year":"2022","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/j.dss.2003.12.001","article-title":"Model Checking for Design and Assurance of e-Business Processes","volume":"39","author":"Anderson","year":"2005","journal-title":"Decis. Support Syst."},{"key":"ref_41","first-page":"127","article-title":"Integrated Tool for Assisted Predictive Analytics","volume":"Volume 1341","author":"Simian","year":"2021","journal-title":"Proceedings of the MDIS 2020\u2014Modelling and Development of Intelligent Systems"},{"key":"ref_42","unstructured":"(2024, October 16). Oracle LiveLabs Workshop. Available online: https:\/\/apexapps.oracle.com\/pls\/apex\/r\/dbpm\/livelabs\/run-workshop?p210_wid=3880."},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1016\/j.infsof.2012.07.002","article-title":"A Pattern-Based Approach for the Verification of Business Process Descriptions","volume":"55","author":"Patig","year":"2013","journal-title":"Inf. Softw. Technol."},{"key":"ref_44","first-page":"24824","article-title":"Chain-of-Thought Prompting Elicits Reasoning in Large Language Models","volume":"35","author":"Wei","year":"2022","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"2717","DOI":"10.18653\/v1\/2023.acl-long.153","article-title":"Towards Understanding Chain-of-Thought Prompting: An Empirical Study of What Matters","volume":"Volume 1","author":"Wang","year":"2023","journal-title":"Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics"},{"key":"ref_46","unstructured":"Ayub, H. (2024, October 16). GPT-4o: Successor of GPT-4. Available online: https:\/\/hamidayub.medium.com\/gpt-4o-successor-of-gpt-4-8207acf9104e."}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/15\/12\/778\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T16:47:09Z","timestamp":1760114829000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/15\/12\/778"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,5]]},"references-count":46,"journal-issue":{"issue":"12","published-online":{"date-parts":[[2024,12]]}},"alternative-id":["info15120778"],"URL":"https:\/\/doi.org\/10.3390\/info15120778","relation":{},"ISSN":["2078-2489"],"issn-type":[{"value":"2078-2489","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,5]]}}}