Checking business process correctness in apromore

Abstract

© Springer International Publishing AG, part of Springer Nature 2018. In this paper we present the integration of BProVe - Business Process Verifier - into the Apromore open-source 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 usag..