BProVe a novel verification framework for BPMN 2.0. The analysis is based on a formal operational semantics, implemented using MAUDE, defined for the BPMN 2.0 modelling language, and is provided as a freely accessible service that uses open standard formats as input data. Furthermore a plug-in for the Eclipse platform has been developed making available a tool chain supporting users in modelling and visualising, in a friendly manner, the results of the verification.



The architecture of the tool chain that we propose is synthesised in the previous 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, realised as an Eclipse plug-in (extending the Eclipse BPMN2 Modeller), 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.
 Requirements

Download BProVe Tool-Chain

  1. From the menu choose: Help / Install New Software...
  2. Click the  Add button
  3. In the  Add Repository  dialog that appears, paste the BProVe update site http://pros.unicam.it/BProVe_update_site/ click the OK 
  4. Uncheck  Group items by category
  5. Click Next and follow the procedure

Behind the scene

Usage of BProVe Tool-Chain in Eclipse 

Design a BPMN 2.0 model in Eclipse and click the BProVe button to open a menu. Select the model you want to verify, select the path to save the result, then click “Generate”. This step will parse the BPMN 2.0 model into the syntax used by the BPMNOS semantics.

If you want to proceed with some properties verification, press “Yes” and a menu will pop up to allow you to select the property you want to check. The result of the verification will be displayed in a Text Area of the menu. If a graphical counterexample is present, a BPMN 2.0 model will be displayed with highlighted the path that does not verify the property.

Publications

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