COLLABORATION VS. CHOREOGRAPHY CONFORMANCE IN BPMN
- Flavio Corradini, Andrea Morichetta, Andrea Polini, Barbara Re, Francesco Tiezzi. Collaboration vs Choreography Conformance in BPMN 2.0: from Theory to Practice. 22nd IEEE Enterprise Distributed Object Computing Conference (EDOC 2018), Stockholm, Sweden, Oct. 16-19, 2018; © 2018 IEEE. [PDF]
The C4 formal framework aims at supporting designers in modelling diagrams, composing them and automatically check if a set of processes composed in collaboration conforms to a prescribed choreography. A distinctive aspect of the tool is that modelers do not need to know the formal notions underlying its functionalities. The tool was developed as a stand-alone solution, but it is also available as an online service accessible via a web page.
Specifically, C4 is able to manage choreography, collaboration or process models in
the .bpmn format. These input models can be generated by a system designer using the Camunda modeller completely integrated in the C4 platform different external
BPMN modelling environments. Indeed, the C 4 platform is compatible with the most known external modelling environments such as Eclipse BPMN Modelling, Camunda and Signavio.
HOW TO USE THE CONFORMANCE CHEKER STAND-ALONE VERSION
Requirement:
- Please install the mCRL2 checker (link) and make it accessible from the shell scripts
Use:
- Download the Stand-alone version also available at this link
- Run the tool with a double click on the C4.jar file or type:
// Java 8
java -jar c4.jar// > Java 8
java --module-path /USER_JavaFX_path/lib --add-modules=javafx.controls,javafx.fxml -jar c4.jar- Select the collaborations and the choreographies to load, for users convenience we provide a list of BPMN input examples that can be used as test cases
- Click on the file pathname to visualize the model preview that can be moded or zoom in/out
- Check the “show LTS” box to visualize the LTS graph
- Click on “generate LTS” button
- Select the desidered equivalence and click on “check equivalence” button
- In case the equivalence is not satisfied a counterexample is visualize
Step-by-Step video
HOW TO USE THE CONFORMANCE CKECKER ONLINE VERSION
Requirements:
- Web Browser
Use:
HOW TO USE THE C4 ONLINE VERSION
Use:
- Click on the link (Use Chrome for a better user experience)
- Follow the video below for the fuctionalities
- Please use the registration form before the login or use existing login with loaded examples: User: “andrea@andrea” Pwd: “andrea”
STEP BY STEP VIDEO:
HOW TO USE THE CONFORMANCE CHEKER STAND-ALONE VERSION
Requirement:
- Please install the mCRL2 checker (link) and make it accessible from the shell scripts
Use:
- Download the Stand-alone version also available at this link
- Run the tool with a double click on the C4.jar file or type:
// Java 8
java -jar c4.jar// > Java 8
java --module-path /USER_JavaFX_path/lib --add-modules=javafx.controls,javafx.fxml -jar c4.jar- Select the collaborations and the choreographies to load, for users convenience we provide a list of BPMN input examples that can be used as test cases
- Click on the file pathname to visualize the model preview that can be moded or zoom in/out
- Check the “show LTS” box to visualize the LTS graph
- Click on “generate LTS” button
- Select the desidered equivalence and click on “check equivalence” button
- In case the equivalence is not satisfied a counterexample is visualize
Step-by-Step video
HOW TO USE THE CONFORMANCE CKECKER ONLINE VERSION
Requirements:
- Web Browser
Use:
HOW TO USE THE C4 ONLINE VERSION
Use:
- Click on the link (Use Chrome for a better user experience)
- Follow the video below for the fuctionalities
- Please use the registration form before the login or use existing login with loaded examples: User: “andrea@andrea” Pwd: “andrea”
STEP BY STEP VIDEO:
