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


The BProVe architecture is synthesised in the following figure.
From the left side of the figure to the right, we can see three main components: Modelling Environment, BProVe WebService, and BProVe Framework. The Modelling Environment component represents the tool used to design BPMN models and to specify which properties of the model the user wants to verify. This component is connected to the BProVe WebService and interacts with it via HTTP requests. A BPMN model and a property to verify are automatically sent to the Web service, which handles the requests by parsing the BPMN model and the property into the syntax accepted by the BProVe Framework. In particular, the result of parsing the property is an LTL formula. The BProVe Framework component is based on a running instance of MAUDE loaded with the MAUDE modules implementing the BPMN semantics and the LTL MAUDE model checker.

BProVe usage

  • 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.

BProVe Stand-Alone

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.

Requirements

  • Java 1.7+

 

 


BProVe in Eclipse

Installation

Step 1. From the menu choose: Help / Install New Software...

Step 2. Click the  Add button

Step 3. In the  Add Repository  dialog that appears, paste the BProVe update site http://pros.unicam.it/BProVe_update_site/ click the OK 

Step 4. Uncheck  Group items by category

Step 5. Click Next Accept the license and follow the procedure

 

 

Usage 

Once installed, you can access BProVe by clicking over the BProVe icon (as shown in the following figure). The interface and the usage are the same described for the BProVe standalone.

Video Tutorial

Below a BProVe tutorial for its integration in Eclipse is reported.

Requirements


BProVe in Apromore

The current version of the BPRoVe ​is available as an Apromore plugin for the editor environment. You can access one of the available Apromore nodes to test its functionalities.

Usage

From the Apromore Editor, open a BPMN model and click on the BProVe icon. A window pops up to select the properties to verify from a drop-down menu. The result of the verification together with the time required to verify the property is reported in the “Verification Result” area. If the result is negative the process trace which violates the property will be highlighted in red.

Video Tutorial

Below a BProVe tutorial for its integration in Eclipse is reported.


BProVe – Web Service

The BProVe Web Service is accessible by means of html post requests. A JSON string must be defined and sent to the web service to access its functionalities. A guide for interacting with the BProVe Web Service is available.


Behind the scene

  • We developed two implementation of the BPMN 2.0 Operational Semantics in Maude. One, the most direct implementation, reports for each rule of the semantics one or more Maude rewriting rules. The second instead is an improved version which allows to perform faster verifications thanks to some development tricks in Maude; those changes do not affect the meaning of the semantics.
  • A parser from BPMN to Maude has been developed for both the versions.
  • Both the BPMN Operational Semantics versions, and the parsers, are stored in a Git Repository https://PROSLab@bitbucket.org/proslabteam/bpmnos.git.
  • To run them you need to download Maude (http://maude.cs.uiuc.edu/) and follow the README file reported in each folder.

Testing

BProVe has been largely tested over 2569 models included in the BPMN Academic Initiative (http://bpmai.org/). The tests confirm that it is not seldom to find models that violate relevant behavioural properties, also after their release. In addition the experiments confirm that our approach seems to be applicable in practice to realistic BPMN models.

Fraction of Models Satisfying Soundness and Safeness.

Average time (in ms), clustered in classes according to number of elements in the model.


Publications