Correctness Checking for BPMN Collaborations with Sub-Processes 

is a verification tool for checking Safeness, Soundness and message-relaxed Soundness properties of BPMN collaboration models including the exchange of messages and sub-processes.

  is published as an open source project under the GPL 2 license. It can be downloaded from the bitbucket repository available at the following link.

Usage

  • As a web service developed in Java using the RESTful technology;
  • As a stand-alone version (jar executable file) that uses BPMN open standard format as input data and returns verification results in a JSON format;
  • As a website integrating Camunda bpmn.io and making available S³  as a toolchain supporting users in modelling and visualizing, in a friendly manner, the results of the verification.

Accessing S3 Web Service

The web-service contains the core of the system, and has the duty of taking in input the .bpmn representation of a BPMN model and sending back the results of safeness and soundness checks. Once the service receives the input file of the designed model, S³ parses it using the Camunda API and builds the corresponding LTS. The LTS is generated according to the formal semantics. This step, as well as the subsequent verification task, are implemented in Java. The output of the web-service is based on the result of the verification of safeness, soundness, and message-disregarding soundness, together with the corresponding counterexamples.

S3 WS can be accessed as RESTful service via HTTP requests at this link:

http://pros.unicam.it:8080/S3/model/verifier/

The web service can be tested with any client and takes in input an xml specification of the BPMN model and gives in output a Json result.

The result message is a string structured as follows:

{"models": [{
    "elements": NUMMBER OF ELEMENTS WITHIN THE COLLABORATION,
    "safe": {
        "id": ,
        "messages": [],
        "sequences": []
    },
    "sound": {
        "id": ,
        "messages": [],
        "sequences": []
    },
    "time":VERIFICATION TIME IN NANOSECONDS,
}]}

Where SOUNDNESS ID can be:

0 --> "Unsound for dead token"
1 --> "Unsound for proper completion violation"
2 --> "Message disregarding sound"
3 --> "Sound"

SAFENESS ID can be:

4 --> "Safe"
5 --> "Unsafe"

Using S3 jar

S3 can be executed locally using the jar file available at the following link:

S3.jar

Once downloaded the jar file, execute the following script in the system console from the file path:

// Java 8
java -jar S3.jar


// > Java 8
java --module-path /USER_JavaFX_path/lib --add-modules=javafx.controls,javafx.fxml -jar S3.jar

The executable version of S3 shows a window where to load the desired .bpmn file and to verify the model properties. After launching the verification, the bottom text area will show the results in a Json format.

To notice: select the right model before to press the Verify button.

Using S3 integrated in Camunda bpmn.io 

S3 can be used as a website integrating Camunda bpmn.io and making available   as a tool chain supporting users in modelling and visualisation, in a friendly manner, of the results of the verification.

TRY IT ON-LINE: http://pros.unicam.it:8080/S3/modeler/

Using the graphical interface the model designer can specify its collaboration using all the facilities of the Camunda modeller. Successively, clicking on the button at the top-right corner the verification can be run. The verification results of safeness and soundness will be summarised by a ‘traffic light’ reporting: the green (resp. red) colour for safeness means that the collaboration model is safe (resp. unsafe); for soundness, instead, the green colour means that the model is sound (and, consequently, message-relaxed sound), the yellow colour corresponds to the warning situation, as the model is unsound but message- relaxed sound (hence, a manual check by the designer is required), finally the red colour means that the model is unsound for both notions.

To support the designer in solving issues raised by the verification, in case of a negative outcome an additional button depicting a lens gives the possibility to show the corresponding counterexample, which will be displayed directly on the model by colouring the sequence/message edges involved in the violation.

Validation

Models used to validate the proposed verification framework are made available in the repository available at the following link.

It includes the models used in the evaluation in the large such as a dataset of 887 collaboration model extracted by BPM Academic Initiative (http://bpmai.org/) and the 50 models resulting by the involvement of practitioners.