Checking Business Process Correctness in Apromore

In this paper we present the integration of BProVe - Business Process Verifier - into the Apromore opensource process analytics platform. Given a BPMN model BProVe enables the verification of properties such as soundness and safeness. Differently from established techniques for BPMN verification, that rely on the availability of a mapping into a transition based formalism (e.g. Petri Nets), BProVe takes advantage of a direct formalisation of the BPMN semantics in terms of Structural Operational Semantics rules. On the one side, this still permits to give precise meaning to BPMN models, otherwise impossible due to the usage of natural language in the BPMN standard specification. On the other side, it permits to overcome some issues related to the mapping of BPMN to other formal languages equipped with their own semantics (e.g. non local effects of BPMN elements such as termination). The defined BPMN semantics has been implemented in MAUDE. Through the MAUDE Linear Temporal Logic (LTL) model checker, correctness properties encoded in LTL formulae are evaluated and the result is then presented to the user. The integration into Apromore allows model designers to use the Apromore BPMN editor to design models and to interact with BProVe to verify properties of the designed model. The results are shown graphically on top of the process model, so as to highlight behavioural paths that violate the correctness properties. Designers can then easily identify the violation and repair the model accordingly.