↑ Return to Features

Verify BPMN correctness with BProVe

Authors: Flavio Corradini, Fabrizio Fornari, Andrea Polini, Barbara Re, Francesco Tiezzi, Andrea Vandin, Marcello La Rosa

This plugin integrates the BProVe tool, to enable the verification of syntactic correctness properties of a BPMN model such as soundness and safeness. For example, one can check that the model is free from behavioral anomalies such as deadlocks (a process instance may get stuck) or livelocks (a process instance may run forever in a loop). Additionally, more specific properties (called “domain dependent properties”) can be defined 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 the proper evolution of process activities.

The plugin can verify single process models as well as collaboration diagrams including multiple pools. 


To use this plugin, 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.

A screencast of this plugin can be found here.