C4 TOOL – COLLABORATION VS CHOREOGRAPHY CONFORMANCE CHECKING IN BPMN 2.0


The C4 formal framework  aims at supporting modelers to automatically check whether a 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. In this regards, even if we  support the BPMN modelling standard, we widely tested its compatibility with models designed by Eclipse BPMN Modeler, Camunda and Signavio.

                                                                                      
C4 Stand-alone                              C4 Online                                Input Examples


HOW TO USE THE C4 STAND-ALONE VERSION

Requirement:

  • Please install the mCRL2 checker (link) and make it accessible from the shell scripts

Use:

  1. Download the Stand-alone version also available at this link
  2. Run the tool with a double click on the C4.jar file or type “java -jar C4.jar” on the terminal
  3. 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
  4. Click on the file pathname to visualize the model preview that can be moded or zoom in/out
  5. Check the “show LTS” box to visualize the LTS graph
  6. Click on “generate LTS” button
  7.  Select the desidered equivalence and click on “check equivalence” button
  8.  In case the equivalence is not satisfied a counterexample is visualize

Step-by-Step video

 


HOW TO USE THE C4 ONLINE VERSION

Requirements:

  • Web Browser

Use:

  • Click on the link    
  • Follow the procedure from point 3 described for the Stand-Alone version