Context: Using models to represent business processes provides several advantages, such as facilitating the communication between the stakeholders or being able to check the correctness of the processes before their implementation. In contrast to traditional process modeling approaches, the artifact-centric approach treats data as a key element of the process, also considering the tasks or activities that are performed in it. Objective: This paper presents a way to verify and validate the semantic correctness of an artifact-centric business process model defined using a combination of UML and OCL models - a BAUML model. Method: We achieve our goal by presenting several algorithms that encode the initial models into first-order logic, which then allows to use an existing satisfiability checking tool to determine their correctness. Results: An approach to verify and validate an artifact-centric BPM specified in BAUML, which uses a combination of UML and OCL models. To do this, we provide a method to translate all BAUML components into a set of logic formulas. The result of this translation ensures that the only changes allowed are those specified in the model, and that those changes are taking place according the order established by the model. Having obtained this logic representation, these models can be validated by any existing reasoning method able to deal with negation of derived predicates. Moreover, we show how to automatically generate the relevant tests to validate the models. We also show the feasibility of our approach by implementing a prototype tool and applying it to a running example. Conclusion: It is feasible to ensure the semantic correctness of an artifact-centric business process model in practice.

Peer Reviewed