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


BProVe usage

  • as a web service accessible by html post requests and by its web interface (http://pros.unicam.it/bprove-web-interface)
  • 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.

Publications

  • F. Corradini, A. Polini, B. Re, F. Tiezzi: An Operational Semantics of BPMN Collaboration. FACS 2015: 161-180. [link]
  • 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. [link]
  • 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. [link]
  • F. Corradini, F. Fornari, A. Polini, B. Re, F. Tiezzi.(2018). A formal approach to modeling and verification of business process collaborations. Science of Computer Programming166, 35-70. [link]
  • F. Fornari, M. La Rosa, A. Polini, B. Re, F. Tiezzi.. Checking Business Process Correctness in Apromore. CAiSE 2018 FORUM – Information Systems in the Big Data Era. Springer, LNBIP, vol. 317, pp. 114-123. Tallinn, Estonia, 11-15 June 2018. [link]