Technical report 


The BPMN 2.0 standard is nowadays largely used to model distributed components both in academic and industrial contexts. The notation makes possible to represent
systems from different perspectives. A global perspective, using choreography diagrams, to describe the interactions between components without exposing their internal structure, and a local perspective, using collaboration diagrams, where the
internal behavior of a component can be highlighted.
With this tool we propose a formal approach for checking conformance of choreographies, representing global constraints, with related collaborations, representing possible implementations. In particular, we provide a direct formal operational semantics for both BPMN collaboration and choreography diagrams, and we formalize the conformance concept by means of two relations defined on top of the semantics.
We have developed the C 4 tool to support the approach into practice.


The C4 formal framework is implemented as a Java tool 1 supporting modelers in automatically checking 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 a service accessible, or integrable as a plug-in in existing modeling tools, through a RESTful interface. In this regards, even if we support any BPMN modeling environments, we widely tested its compatibility with Eclipse BPMN Modeling, Camunda and Signavio. Fig. 9 depicts the internal components of the C4 tool and the interfaces with the modeler. Specifically, C4 takes as input a choreography and a collaboration in the .bpmn format. Input models can be generated by the modeler using different BPMN modeling environments, or can be retrieved from public repositories. The input files can be loaded in the C4 tool using a dedicated GUI modeler can load multiple files, both for choreographies and collaborations. The inclusion of this feature was driven by the necessity of checking the conformance between different versions of the same model, avoiding to load each time a new file. The loaded models are listed in two text-areas and by clicking in one of them, a graphical preview of the model is showed  automatically. Once the input files have been selected the C4 tool parses the models and generates the corresponding LTS graphs for both the choreography and the collaboration. The parsing of the input files is based on the Camunda API. The API has been used as it is for the collaboration models, while it has been extended (to include
choreography tasks) for the choreographies. The LTSs are computed by means a Java implementation of the direct semantics.
Once generated the LTSs, C4 saves the results in two .aut files and automatically open the BPMN Checker where the desired conformance relations can be checked. The conformance checking is achieved by resorting to the mCRL2 equivalence checker, that is fully integrated in the C 4 tool. Notably, the standard bisimulation and trace equivalences supported by mCRL2 can be directly used at this stage, as all the specific characteristics of our conformance relations (e.g., the use of hiding), have been already taken into account during the LTS generation.
The verification results are visualized using a green/red indicator that states the satisfiability/unsatisfiability of the conformance relation. In case of dissatisfaction, C 4 returns back a counterexample. Notably, the usage of the .aut format for storing the LTS graphs enable the integration with other checkers that could be used in the future for further analysis.

The C4 tool is downloadable here:  [TRY IT!!!].