Model Checking of BPMN Models for Reconfigurable Workflows
This addresses workflow reliability issues for business enterprises, but it is incremental as it applies existing model checking techniques to a specific domain.
The paper tackles the problem of verifying that dynamic reconfigurations of business workflows preserve essential properties like deadlock freedom and security, by developing a formal verification procedure that translates BPMN models into Promela and uses the SPIN model checker for correctness checks.
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.