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. Examples of this component are: Apromore and Eclipse BPMN Modeller.
The Modelling Environment 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.
The remaining components constitute what we call the BProVe framework which incorporates two different model checking techniques for analysing properties over models. The MAUDE Model Checker component consists of a running instance of MAUDE loaded with those MAUDE modules implementing the BPMN semantics, and the LTL MAUDE model checker . Instead the MULTIVESTA component enables the interaction with the statistical model checker MULTIVESTA which uses the simulation of a model formalized in BPMNOS MAUDE Semantics.
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. Examples of this component are: Apromore and Eclipse BPMN Modeller.
The Modelling Environment 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.
The remaining components constitute what we call the BProVe framework which incorporates two different model checking techniques for analysing properties over models. The MAUDE Model Checker component consists of a running instance of MAUDE loaded with those MAUDE modules implementing the BPMN semantics, and the LTL MAUDE model checker . Instead the MULTIVESTA component enables the interaction with the statistical model checker MULTIVESTA which uses the simulation of a model formalized in BPMNOS MAUDE Semantics.
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.
- More info about MultiVeStA can be found at https://sysma.imtlucca.it/tools/multivesta
