Correctness Checking for BPMN Collaborations with Sub-Processes 

 


DOCUMENTS
Correctness Checking for BPMN Collaborations with Sub-Processes

DESCRIPTION

verifies the correctness of multi-layered BPMN collaboration diagrams in particular with respect to safeness and soundness. The tool is based on a client-server architecture composed by a client, developed in Html/Javascript and embedding the Camunda bpmn.io modeller, and a web-service, developed in Java using the RESTful technology. 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 semantics defined in Sec. 3.2, as described in Sec. 4.1 of our manuscript available below. 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.

TOOL

The  integration within Camunda modelling environment is available here: S³ Verifier [TRY IT!!!].

 

WEB-SERVICE ACCESS:

S3 WS can be accessed as restful service using the preferred modelling environment. The service is available via HTTP requests at this link :

http://pros.unicam.it:8080/S3/rest/BPMN/Verifier

The web service takes in input an xml specification of the BPMN model and gives in output a textual result.

The result message is a string structured as follows:

[SOUNDNESS CODE]

[--sequenceFlowID or --messageFlowID \n]*
" && "

[SAFENES CODE]

[--sequenceFlowID or --messageFlowID \n]*

Where 
SOUNDNESS CODE can be:

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

SAFENESS CODE can be:

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