2016/07/02 by Juan Carlos Polanco Aguilar, Koji Hasebe, Aguilar, Juan Carlos Polanco +5
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Petri Nets in System Modeling #Service-Oriented Architecture and Web Services #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.1607.00478
openalex publication_date 2016/07/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Nowadays, business enterprises often need to dynamically reconfigure their internal processes in order to improve the efficiency of the business flow. However, modifications of the workflow usually lead to several problems in terms of deadlock freedom, completeness and security. A solid solution to these problems consists in the application of model checking techniques in order to verify if specific properties of the workflow are preserved by the change in configuration. Our goal in this work is to develop a formal verification procedure to deal with these problems. The first step consists in developing a formal definition of a BPMN model of a business workflow. Then, a given BPMN model is translated into a formal model specified in Promela. Finally, by using the SPIN model checker, the correctness of the reconfigured workflow is verified.