BProVe (Business Process Verifier) is a novel verification framework for BPMN 2.0. The analysis is based on a formal operational semantics defined for the BPMN 2.0 modelling language.
BProVe enables the verification of properties such as soundness and safeness both at process and collaboration level. Additionally, more specific properties are defined in order to ensure the conformance of the model to specific behavioural patterns. For example, this may be useful to check the correct exchange of messages as well a proper evolution of process activities (we refer to them as domain dependent properties).
- as a web service accessible by html post requests and by its web interface which exposes the most updated version of BProVe (https://pros.unicam.it/bprove-web-interface)
- as a stand-alone version and as a freely accessible service that uses BPMN open standard format as input data and returns verification results in a textual format and, when necessary, on the BPMN model itself.
- as a plug-in for Eclipse (https://www.eclipse.org) and the APROMORE platforms (http://apromore.org/platform/features/bprove) making available a tool chain supporting users in modelling and visualisation, in a friendly manner, the results of the verification.