S³ 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. S³ is published as an open-source project under the GPL 2 license. It can be downloaded from the S³ bitbucket repository available at the following link.
User Guide
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.
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 resulting 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 this link. 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.jarThe 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
At this link, S³ can be used as a website integrating Camunda bpmn.io and making available S³ as a toolchain supporting users in modeling and visualization, in a friendly manner, of the results of the verification.
Using the graphical interface the model designer can specify its collaboration using all the facilities of the Camunda Modeler. Successively, by 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) color for safeness means that the collaboration model is safe (resp. unsafe); for soundness, instead, the green color means that the model is sound (and, consequently, message-relaxed sound), the yellow color 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 color 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 coloring the sequence/message edges involved in the violation.
S³ 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 models extracted by BPM Academic Initiative (http://bpmai.org/) and the 50 models resulting from the involvement of practitioners.
