A SAT-Based Formal Approach for Verifying Business Process Configuration.

Nowadays, some organizations are using and deploying similar business processes to achieve their business objectives. Typically, these processes often exhibit specific differences in terms of structure and context depending on the organizations needs. In this context, configurable process models are used to represent variants in a generic manner. Hence, the behavior of similar variants is grouped in a single model holding configurable elements. Such elements are then customized and configured depending on specific needs. Nevertheless, the decision to configure an element may be incorrect leading to critical behavioral errors. In the present work, we propose a formal model based on propositional satisfiability formula allowing to find all possible correct elements configuration. This approach allows to provide the designers with correct configuration decisions. In order to show the feasibility of the proposed approach, an experimentation was conducted using a case study.