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.
A screencast of this plugin can be found here.