BProVe Architecture

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