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).
BProVe is published as an open source project under the GPL 2 license. It can be downloaded from the BProVe Bitbucket repository.
- 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.
- as a web service accessible by html post requests.
The stand-alone version consists in a Java Application which can be downloaded from this dropbox link.
Step 1. Launch the BProVe_standalone.jar application by clicking over it.
Step 2. Load a BPMN model (try airline_model.bpmn) in this folder.
Step 3. Select a save path and insert a file name. The generated file will contain information of the verification such as: Parsed model from BPMN to BPMN Operational Semantics Syntax; information about element present in the model; result of the conducted verifications. NOTE: this file will be generated immediately but written only after closing the application.
Step 4. Click over the GENERATE button
Step 5. If everything is ok, click over YES to proceed to the property verification menu
Step 6. Choose one property to verify and click the respective “CHECK” button. WAIT for a result to be reported in the AREA at the bottom of the menu. NOTE: if a “False” result is returned, a file named “copia1.bpmn” will be generated presenting the original BPMN model with highlighted the element along the path violating the property. Each time a “False” result is returned that “copia1.bpmn” file is overwritten.
- The current version of the BPRoVe plugin is available in the Eclipse Marketplace at https://marketplace.eclipse.org/content/bprove.
- BProVe update site http://pros.unicam.it/BProVe_update_site/
Step 1. From the menu choose:
Install New Software...
Step 2. Click the
Step 3. In the
Add Repository dialog that appears, paste the BProVe update site http://pros.unicam.it/BProVe_update_site/ click the
Step 4. Uncheck
Group items by category
Step 5. Click
Next Accept the license and follow the procedure
- F. Corradini, A. Polini, B. Re, F. Tiezzi: An Operational Semantics of BPMN Collaboration. FACS 2015: 161-180.
- F. Corradini, F. Fornari, A. Polini, B. Re, A. Vandin, F. Tiezzi. BProVe: a Formal Verification Framework for Business Process Models. 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017. Urbana Champaign, Illinois, USA, October 30 – November 3, 2017.
- F. Corradini, F. Fornari, A. Polini, B. Re, A. Vandin, F. Tiezzi. BProVe: Tool Support for Business Process Verification. 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 – Tool Demo. Urbana Champaign, Illinois, USA, October 30 – November 3, 2017.