1647 LABEL:LastPageFeb. 12, 2020Oct. 27, 2020

# Collaboration vs. Choreography Conformance in BPMN

Flavio Corradini  Computer Science Division, School of Science and Technology,
University of Camerino
<EMAIL_ADDRESS>,  Andrea Morichetta  ,  Andrea Polini  ,
Barbara Re  and  Francesco Tiezzi

###### Abstract.

The 2.0 standard is a widely used semi-formal notation to model distributed
information systems from different perspectives. The standard makes available
a set of diagrams to represent such perspectives. _Choreography_ diagrams
represent global constraints concerning the interactions among system
components without exposing their internal structure. _Collaboration_ diagrams
instead permit to depict the internal behaviour of a component, also referred
as process, when integrated with others so to represent a possible
implementation of the distributed system.

This paper proposes a design methodology and a formal framework for checking
conformance of choreographies against collaborations. In particular, the paper
presents a direct formal operational semantics for both choreography and
collaboration diagrams. Conformance aspects are proposed through two relations
defined on top of the defined semantics. The approach benefits from the
availability of a tool we have developed, named _C_ ${}^{\ \\!\\!4}$, that
permits to experiment the theoretical framework in practical contexts. The
objective here is to make the exploited formal methods transparent to system
designers, thus fostering a wider adoption by practitioners.

###### Key words and phrases:

, Choreography, Collaboration, Conformance, Tool Support.

##  1\. Introduction

The 2.0 standard is a widely used semi-formal notation to model different
perspectives of distributed information systems [OMG11]. Available diagrams
can be used at different stages in the development life-cycle, while focusing
on specific aspects of the system under construction, and also according to
different development strategies [Pas17, ABN+08]. In the context of this work,
particularly relevant are the diagrams referred as _Choreography_ , _Process_
, and _Collaboration_. The first kind of diagram, _Choreography_ , permits to
represent the interactions among cooperating entities (e.g., software
components, organisations, services, etc.), without exposing their internal
structure. A _Process_ diagram, instead, intends to represent the actions and
the choices that a single entity puts in place in order to reach specific
objectives. Finally, a _Collaboration_ diagram permits to represent the
compositions of different processes, which include communication actions. In
such a way, this latter kind of diagram permits to detail both the
communication schema, and the internal actions and choices enabling a correct
cooperation.

In such a setting, organisations that are willing to cooperate can refer to a
choreography specification detailing how they should interact to reach
specific objectives. On the other hand, the cooperation needs to involve
entities (e.g., software systems) that often are already available, or that
will be specifically introduced for the purpose, within each single
organisation. In the first case, the process to be integrated can be
considered as a sort of legacy element that will directly derive from the
specification of the existing entity, while in the latter case it can be
convenient to shape it starting from the global choreography specification
(e.g., using projection mechanisms). The integration of each single process
into an overall specification of the system leads to the collaboration diagram
previously mentioned. Nevertheless, a collaboration that integrates different
processes to reach the objectives specified in a choreography should show a
behaviour somehow related to that defined by the global specification,
independently from the genesis of the involved processes (legacy or defined
for the purpose). Indeed, the choreography acts as a sort of contract among
the participating parties, and each organisation expects that the others will
follow it. The conformance of a given collaboration with respect to a pre-
established choreography becomes then crucial, since it permits to ensure that
the integrated components are able to successfully collaborate, or can be
possibly and reasonably adapted, without invalidating the communication
constraints imposed by the global specification, so to reach the objectives
defined by the choreography itself. In the general context of service-oriented
systems this problem has received a lot of attention [PTDL07, BBM+05, LMX07,
EKdMSvdA08, RFG10, Mar03]. Notwithstanding this effort, there is still a lack
of frameworks and tools supporting the conformance checking between
collaboration and choreography models when the notation is considered.

Given such a gap and in order to fill it, we provide in this paper a novel
framework to check the conformance of choreography diagrams with respect to
collaborations models. In particular, in our approach we do not resort to a
different intermediate language or formalism; instead we rely on a direct
semantics describing the behaviour of both models. Moreover, we do not impose
any syntactic restriction on the usage of the BPMN modelling notation, i.e. we
allow models to have an arbitrary topology. Clearly, the semantics embeds the
peculiarities of the standard when used to model distributed systems (e.g.,
asynchronous communication among components). More specifically, to formally
describe the behaviour of a system the operational semantics associates
Labelled Transition Systems (LTSs) to its models. A collaboration and a
choreography can then be compared to check the satisfaction of specific
behavioural relations, considering the LTSs resulting from the defined
semantic framework. We rely on a conformance relation (based on bisimulation
[Mil89, Sec. 5]) that is sensitive to deadlocks and different forms of non-
determinism, and on another relation (based on traces [Mil89, Sec. 9.4]) that
instead is more relaxed on this respect, and that however can provide useful
information in order to possibly drive the  identification of interventions
permitting to avoid the highlighted issues. The support of both kinds of
relations allows the system designer to decide the desired trade-off between
the strength of the properties ensured by the system, and the breadth of
choice among available system components.

The developed theoretical framework has been implemented in the _$C^{4}$
(Collaboration vs Choreography Conformance Checker for )_ tool. Standard input
formats for the models are accepted by the tool so to enable its integration
with external modelling environments (e.g., Camunda, Signavio and Eclipse 2
Modeller). The tool permits to hide the underlying formal methods permitting
to system designer, not accustomed with formalisms and formal reasoning, to
access and use well established theories.

Summing up, the major contributions of this paper are as follows:  (i)
definition, and implementation in Java, of a formal operational semantics for
choreographies and collaborations, in particular making the integration of
existing process specifications a viable option to form collaborations;  (ii)
definition, and implementation, of two conformance relations;  (iii)
implementation of the $C^{4}$ tool supporting the proposed methodology and
conformance checking framework. This paper is a revised and extended version
of [CMPRT18]. Specifically, we extend our previous work by proposing a new
dedicated design methodology; in consequence, both the formal framework and
the related supporting tool have been revised accordingly. In particular, we
now consider and support also more realistic scenarios in which the
organisations can integrate already available artefacts, equipped with
corresponding process specifications.

_Outline._ Section 2 provides background notions on the modelling notation,
with a particular emphasis on choreography and collaboration diagrams.
Moreover, in this section a running example is introduced; this will be used
in the rest of the paper to clarify various aspects of the proposed framework.
Section 3 discusses the life-cycle of a choreography specification, and how
the developed theoretical framework, and the related tool, fits in such a
setting. Section 4 introduces formal syntax and semantics for both
choreographies and collaborations, and it presents the conformance relations
we have defined. Successively, Section 5 presents the $C^{4}$ tool and
illustrates its practical usage, Section 6 provides a detailed discussion
about subtle points of our conformance checking approach, and Section 7
discusses the scientific works much related to our proposal. Finally, Section
8 concludes the paper and discusses directions for future work.

##  2\. Background Notions

This section first provides some basic notions on elements that can be
included in BPMN choreography and collaboration diagrams, then it introduces a
scenario that will be used as a running example.

|  |
---|---|---
a. | b. | c.
Figure 1. BPMN 2.0 Collaboration and Choreography Elements.

_The BPMN Standard._ This paragraph includes details on the main concepts of
BPMN we use in the following, in particular focusing on the elements reported
in Fig. 1.

Fig. 1.b depicts the modelling elements that can be included in all the
diagrams considered in this paper. Events are used to represent something that
can happen. An event can be a start event, representing the point in which the
choreography/collaboration starts, while an end event is raised when the
choreography/collaboration terminates. Gateways are used to manage the flow of
a choreography/collaboration both for parallel activities and choices.
Gateways act as either join nodes (merging incoming sequence edges) or split
nodes (forking into outgoing sequence edges). Different types of gateways are
available. A parallel gateway (AND) in join mode has to wait to be reached by
all its incoming edges to start, and respectively all the outgoing edges are
started simultaneously in the split case. An exclusive gateway (XOR) describes
choices; it is activated each time the gateway is reached in join mode and, in
split mode, it activates exactly one outgoing edge. An event based gateway is
similar to the XOR-split gateway, but its outgoing branches activation depends
on the occurrence of a catching event in the collaboration and on the
reception of a message in the choreography; these events/messages are in a
race condition, where the first one that is triggered wins and disables the
other ones. Sequence Flows are used to connect collaboration/choreography
elements to specify the execution flow.

In a collaboration or process diagram, also the elements in Fig. 1.a can be
included. Pools are used to represent participants involved in the
collaboration. Tasks are used to represent specific works to perform within a
collaboration by a participant. Intermediate Events represent something that
happens during the flow of the process, such as sending or receiving of a
message. Message Edges are used to visualize communication flows between
different participants, by connecting communication elements within different
pools.

Focusing on the choreography diagram, we underline its ability to specify the
message exchanges between two or more participants. This is done by means of
Choreography Tasks in Fig. 1.c. They are drawn as rectangles divided in three
bands: the central one refers to the name of the task, while the others refer
to the involved participants: the white one is the initiator (sender), while
the gray one is the recipient. Messages can be sent either by one participant
(One-Way tasks) or by both participants (Two-Way tasks).

In selecting the considered BPMN elements, we have mainly focused on the
control flow and communication views. In doing that, we have followed a
pragmatic approach to provide a precise characterization, and tool support,
for a subset of BPMN elements that are largely used in practice.  Indeed, even
though the BPMN specification is quite wide, only a limited part of its
vocabulary is used regularly in designing BPMN models. This is witnessed by
the models included in the BPM Academic Initiative
repository111http://bpmai.org/. Moreover, a previous study we did [MPRWT18]
also confirms that our selection of BPMN elements is expressive enough to
support the majority of the interaction patterns proposed in [BDA05] (see,
[Muz19, Sec. 8.5] for more details).  It is also worth noticing that most of
the elements we have intentionally left out can be expressed in terms of the
elements we include. Indeed, it is common to represent the inclusive gateways
as a combination of exclusive and parallel gateways enumerating all possible
combinations of outgoing edges activation [CDSW18]. Tasks with the loop marker
can be easily represented by embedding standard tasks in a looping behaviour
expressed using two exclusive gateways (one in the split mode and the other
one in the join mode). Moreover, we have left out timing elements, as they are
not precisely specified in choreography diagrams [OMG11, p. 341]. Other
elements, such as those concerning error and compensation handling, are
instead left out in order to keep the formal framework more manageable.
Finally, for what concerns data objects and gateway conditions, we abstract
them since we aim at exhaustively analyzing all executions of a given model,
and not only those resulting from specific input values. The introduction of
data, indeed, can only restrict the behaviour of considered models. Notably,
data modelling is optional in BPMN, as the notation mainly focuses on control
flow and, hence, only modelling constructs of this type are mandatory. In
summary, for the BPMN standard data-related elements remain somehow second
class modelling constructs [MSW11].

|
---
a. Booking choreography
b. Booking collaboration
Figure 2. Booking Running Example.

_Running Example._ The collaboration and the choreography diagrams regarding a
booking system introduced here are successively used in the paper to
illustrate the various aspects of the proposed framework.

_Choreography Example_. The choreography in Fig. 2.a combines the work-
activities of a booking system, a customer and a bank. They interact in order
to book and pay for travel. After accessing to the booking system, the
customer requests an itinerary, and then he/she receives a tentative planning.
Then, the choreography can proceed following two different paths according to
the customer decision. The upper path is triggered when the customer decides
to withdraw the travel proposal; while the lower path is used to accept the
proposal. In particular, when the proposal is accepted, the customer interacts
with the bank for the payment of the ticket, and then the bank sends the
confirmation to the booking system. The latter completes the procedure by
sending the ticket to the customer.

_Collaboration Example_. The collaboration in Fig. 2.b shows the behaviour of
the same participants of the choreography to reach the same goals. After the
customer logs into the booking system, he/she will request some travel
information, and then he/she will receive a proposal from the booking system.
The customer then decides whether to withdraw or accept the proposal; this is
represented through a XOR gateway. According to the decision, either the upper
path, for the proposal withdraw, or the lower path, for the confirmation, is
activated. The booking system waits for the decision of the customer and
behaves accordingly. This is represented through an event-based gateway. In
the case of withdrawing, the two participants terminate with end events. In
case of confirmation, the customer sends the itinerary acceptance to the
booking system and asks for payment to the bank. As soon as the bank processes
the payment, and confirms it to the booking system, the customer receives the
ticket.

##  3\. The _C_ ${}^{\ \\!\\!4}$ Methodology

Choreographies have emerged in the context of distributed computing, and in
particular of Service Oriented Computing, as an approach to describe/specify
application-level protocols to be adopted by different services willing to
cooperate. In particular, the specification defines the messages and their
mutual dependencies, that are, or have to be, exchanged by the participating
parties in order to fulfil the choreography objectives.

In the literature, different approaches to choreography specifications, and
their usage, have been adopted [HH08a, MM03]. The first one considers
choreographies as emerging artefacts that relate to the integration of
services composed to collaboratively reach an objective. The emerging models,
that can be derive to represent the exchanged messages and their order, can be
successively considered to analyse properties of the composition and to
possibly reason on it. Symmetrically, besides such a bottom-up approach, a
top-down approach has also been proposed. In this case, a choreography acts as
a blueprint defining which are the messages that have to be exchanged. The
specification can be used to drive the development of services that will take
part in a possible choreography enactment. In particular, in such a case the
participants, and their composition, have to abide by the communication
constraints defined in the specification. Finally, a hybrid approach can be
conceived. In this case, as in a top-down approach, a choreography is defined
to act as a blueprint for parties interested in collaborating to reach shared
objectives. However, as it is for the case of a bottom-up approach, the
collaborating parties will employ and integrate already available resources,
possibly making adjustments, if feasible, so to correctly reproduce the
behaviour expected by the considered choreography specification.

Figure 3. $C^{4}$ methodology life process.

The $C^{4}$ methodology that is presented here fits best with a hybrid
approach. Fig. 3 represents an ideal life process of a choreography
specification in this setting. In the first state (specification), given an
application domain, a ‘super partes’ organisation defines a choreography
specification that will act as a blueprint for those organisations interested
in participating in possible choreography enactments. The specification
reports the expected message exchanges, and the objectives that partners
participating to the choreography can reach, both singularly and collectively.
For instance, the choreography in Fig. 2.a defines precise prescriptions for a
booking system, a customer and a bank that would like to cooperate to perform
a business transaction that will include a reservation for a resource in
change of the corresponding price, to be paid via a bank transaction.

Once the choreography has been completely specified, it is made available to
interested parties (publication), and can be retrieved in order to implement
services able to play the possibly foreseen roles. The publication can be as
simple as a pdf file stored on a precise location, or be managed using
specific service repositories (see, e.g., [AAP13, CFP+19]).

Once published, choreography can be seen as an opportunity for an organisation
to integrate with others so to do business together (enablement). In such a
sense, an organisation is generally interested in choreographies in which
employing its services, possibly already available, it can play a role. Then
it looks for potential partners in order to pursue the objectives of the
choreography. The goal of such a phase is to enable the choreography so that
an instance of it can be successively enacted. Notably, all the roles foreseen
by the specification must be played by a different organisation. To do this,
each organisation employ a service among the one foreseen by the choreography,
and proposes it as a possible candidate. Different processes can be conceived
to select the participants so to fill all the roles. In this paper, we do not
make any assumption on such a selection; anyway, when all the roles are filled
the choreography is enabled. Nevertheless, before enacting the choreography it
is necessary to check that the composition of the selected services will
conform to the one specified by the choreography. In a BPMN setting, the
choreography specification will have been defined using a BPMN choreography
diagram, while the different services will have been described using process
diagrams, reflecting the actual implementation, that however when they will be
composed will form a BPMN collaboration diagram.

Finally, the transition to the next state of the $C^{4}$ methodology
(enactment) will result in the execution of a choreography instance, and then
in the exchange of the prescribed messages. This should be made possible only
if the resulting collaboration diagram can reach the objectives specified by
the choreography. Instead, if this is not the case, the enactment should be
prevented, and the participants informed of possible issues in the
composition. In fact, as it will be clarified in the next sections, this is
where the $C^{4}$ tool comes into play permitting to check if the participants
involved in an enabled choreography produce a behaviour “fully respecting” the
prescriptions of the choreography model, or instead if issues have been
identified. In particular, the $C^{4}$ tool supports different kinds of
checks, and the corresponding results can help to  identify interventions on
the collaboration to possibly solve the highlighted issues.  A common
intervention could be the definition of adapters for the non-conforming
parties. An adapter is indeed an artefact that carries out a series of
activities that are generally used to fix interoperability issues in a
component-based system. In our case, the adapter will aim at solving issues in
a collaboration that lead to the violation of a conformance relation with
respect to a given choreography. Different works have been proposed in the
literature concerning adaptation in BPMN (see, e.g., [ASGPT18, RH15, HW04,
RS16]). Other possible interventions could also be related to the refinement
of the high-level specification of collaborations with the introduction of
lower-level information (e.g., guards driving the decisions taken by XOR
gateways). In fact, it may happen that the issues in the specification are
caused by the inherent non-determinism present in choreography model for which
guards are left unspecified. In such a case, when concrete data and
expressions are added these issues could simply disappear.

Fig. 4 helps to clarify the steps of the $C^{4}$ methodology in practice. In
the figure, six different processes are represented, possibly implemented by
services delivered by different organisations. In particular, in reference to
the choreography reported in Fig. 2, different options could be admitted for
each role to complete the specification. The process in Fig. 4.a has been
defined to play the role of the bank, while the two processes in Fig. 4.b and
Fig. 4.c have been both selected to play the role of the customer. Finally,
the three processes in Fig. 4.d, Fig. 4.e, and Fig. 4.f have been selected to
play the role of a booking system. In such a situation, six possible different
compositions of processes are possible. Nevertheless, only few of them
actually permit to achieve the objectives of the corresponding choreography,
as it is detailed in Section 4 (see Table 1). In particular, possible
composition problems can relate to structural issues (e.g., non correspondence
on the sets of exchanged messages by the involved processes) or behavioural
issues (e.g., non conformance with respect to specific behavioural relations
of the resulting composition). In such a setting, the $C^{4}$ tool then
permits to prevent the enactment of enabled choreography instances that will
successively result in the emergence of problems during the running stage.  In
these cases the engineer could evaluate possible interventions, such as the
introduction of adapters or the refinement of models so to solve the issues
highlighted by $C^{4}$.

---
a. Bank 1
b. Customer 1
c. Customer 2
d. Booking System 1
e. Booking System 2
f. Booking System 3
Figure 4. Possible processes for the roles in the choreography of Fig. 2.

##  4\. The formal framework

This section presents the formalisations at the basis of our framework,
concerning the semantics of choreography and collaboration diagrams, and their
conformance.

### Choreography and Collaboration Semantics

We first summarise the distinctive aspects of the semantics of the
choreographies and collaborations in relation to the modelling principles, and
then we illustrate their formal definitions.

#### Linguistic Aspects and Design Choices.

Concerning choreography diagrams, we made some specific design choices. In
relation to the _Two-Way choreography task_ , the OMG standard states that it
is “an atomic activity in a choreography process” execution [OMG11, p. 323].
However, this does not mean that the task blocks the whole execution of the
choreography. In fact, participants are usually distributed, and we assume
that other choreography tasks involved in different parallel paths of the
choreography can be executed. Thus, here we intend atomicity to mean that both
messages exchanged in a Two-Way task have to be received before triggering the
execution along the sequence flow outgoing from the task. Therefore, even if
we allow Two-Way tasks in the choreography models, we safely manage them as
pairs of One-Way tasks preserving the same meaning.

A further distinctive aspect of our formal semantics concerns the
_communication model_ that, to be compliant with the standard, is different
for choreographies and collaborations. A BPMN choreography diagram is, indeed,
a description at a high level of abstraction of message exchanges among
participants of a system. The basic element of this kind of model is the
choreography task, which specifies a single message exchange from a sender
participant to a receiver one. According to the BPMN standard [OMG11, p. 315],
a choreography task completes when the receiver participant reads the message.
Hence, a choreography task is a blocking activity, which resumes the execution
only when an exchanged message is received. For this reason, the communication
model of choreographies is deemed to be synchronous. The communication model
of collaborations, instead, is asynchronous. This means that a message sent by
one participant is enqueued by the receiving one, which can then consume and
process it subsequently, while the sender is free to proceed with its
execution. This reflects the distributed nature of collaborations. The use of
two different communication models also impacts on the definition of the
conformance relations as illustrated below.

Finally, we do not require BPMN models to satisfies any structural constraint,
such as the well-structuredness [KtHB00] property required by many approaches
in the Business Process Management domain. In fact, we consider models with an
arbitrary topology, so that the models can have unbalanced workflows.
Therefore, the class of models we consider is the most comprehensive one that
can be designed in BPMN from the structural point of view.

#### Semantics of Choreographies.

To enable a formal treatment of a choreography we defined a Backus Normal Form
(BNF) syntax of its model structure (Fig. 5).

$\begin{array}[]{|@{\ }r@{\ }c@{\ }l@{\ }|}\hline\cr&&\\\\[-5.69046pt]
Ch&::=&{\sf start}({\sf e}_{o})\mid\ {\sf end}({\sf e}_{i},{\sf e}_{c})\mid\
{\sf andSplit}({\sf e}_{i},E_{o})\mid\ {\sf andJoin}(E_{i},{\sf e}_{o})\mid\
{\sf xorSplit}({\sf e}_{i},E_{o})\mid\ {\sf xorJoin}(E_{i},{\sf
e}_{o})\\\\[2.84544pt] &\mid&{\sf task}({\sf e}_{i},{\sf e}_{o},{\sf
p}_{1},{\sf p}_{2},{\sf m})\mid\ {\sf eventBased}({\sf
e}_{i},T_{1},T_{2})\mid\ Ch_{1}\\!\\!\mid\\!Ch_{2}\\\\[0.28436pt]
&&\\\\[-5.69046pt] T&::=&{\sf}({\sf e}_{o},{\sf p}_{1},{\sf p}_{2},{\sf m})\
\mid\ \ T_{1},T_{2}\\\\[2.84544pt] \hline\cr\end{array}$

Figure 5. Syntax of Choreography Structures.

In the proposed grammar, the non-terminal symbol $\mathit{Ch}$ represents
_Choreography Structures_ , while the terminal symbols, denoted by the ${\sf
sans\ serif}$ font, are the considered elements of a model, i.e. events, tasks
and gateways. We are not proposing a new modelling formalism, but we are only
using a textual notation for the elements. With respect to the graphical
notation, the textual one is more manageable for supporting the formal
definition of the semantics and its implementation. Notably, even if our
syntax would allow to write terms that cannot be expressed in BPMN, we
consider here only those terms of the syntax that can be derived from BPMN
models.

Let $\mathbb{E}$ be the set of edge names, in the following ${\sf
e}\in\mathbb{E}$ denotes a sequence edge, while $E\in 2^{\mathbb{E}}$ a set of
edges; we require $|E|>1$ when $E$ is used in joining and splitting gateways.
For the convenience of the reader we refer with ${\sf e}_{i}$ the edge
incoming into an element and with ${\sf e}_{o}$ the edge outgoing from an
element. ${\sf p}$ and ${\sf m}$ denote names uniquely identifying a
participant and a message, respectively. The correspondence between the syntax
used here and the graphical notation of illustrated in Section 2 is as
follows.

  * •

${\sf start}({\sf e}_{o})$ represents a start event with outgoing edge ${\sf
e}_{o}$.

  * •

${\sf end}({\sf e}_{i},{\sf e}_{c})$ represents an end event with incoming
edge ${\sf e}_{i}$ and a (spurious) edge ${\sf e}_{c}$ representing the
complete status of the end event.

  * •

${\sf andSplit}({\sf e}_{i},E_{o})$ (resp. ${\sf xorSplit}({\sf
e}_{i},E_{o})$) represents an AND (resp. XOR) split gateway with incoming edge
${\sf e}_{i}$ and outgoing edges $E_{o}$.

  * •

${\sf andJoin}(E_{i},{\sf e}_{o})$ (resp. ${\sf xorJoin}(E_{i},{\sf e}_{o})$)
represents an AND (resp. XOR) join gateway with incoming edges $E_{i}$ and
outgoing edge ${\sf e}_{o}$.

  * •

${\sf task}({\sf e}_{i},{\sf e}_{o},{\sf p}_{1},{\sf p}_{2},{\sf m})$
represents a one-way task with incoming edge ${\sf e}_{i}$ and outgoing edge
${\sf e}_{o}$ sending a message ${\sf m}$ from ${\sf p}_{1}$ to ${\sf p}_{2}$.
As explained above, the two-way tasks are rendered in our formal framework as
pairs of one-way tasks, hence they are not explicitly included in the syntax.

  * •

${\sf eventBased}({\sf e}_{i},T_{1},T_{2})$ represents an event-based gateway
with incoming edge ${\sf e}_{i}$, and a list of (at least two) tasks
$T_{1},T_{2}$ to be processed. It is worth noticing that the definition of the
task list $T$ is composed by elements of the same structure of the one-way
task except for the incoming edge, which is subsumed in the structure of the
event-based gateway. When convenient, we shall regard a task list simply as a
set.

  * •

$Ch_{1}\\!\\!\mid\\!Ch_{2}$ represents a composition of elements in order to
render a choreography structure in terms of a collection of elements.

To achieve a compositional definition, each sequence edge of the model is
split in two parts: the part outgoing from the source element and the part
incoming into the target element. The two parts are correlated by means of
unique sequence edge names in the model.

Let us consider the BPMN choreography model in Fig 2.a. The textual
representation of its structure is as follow (for reader’s convenience, we use
${\sf e}_{i}$, with $i$ a natural number, to denote sequence edges, and ${\sf
p}_{c}$ for _Customer_ , ${\sf p}_{bs}$ for _Booking System_ and ${\sf
p}_{bk}$ for _Bank_):

$\begin{array}[]{l}{\sf start}({\sf e}_{1})\ \mid\ {\sf task}({\sf e}_{1},{\sf
e}_{2},{\sf p}_{c},{\sf p}_{bs},\mathsf{login})\ \mid\ {\sf task}({\sf
e}_{2},{\sf e}_{3},{\sf p}_{c},{\sf p}_{bs},\mathsf{request})\ \mid\\\ {\sf
task}({\sf e}_{3},{\sf e}_{4},{\sf p}_{bs},{\sf p}_{c},\mathsf{reply})\ \mid\
{\sf xorSplit}({\sf e}_{4},\\{{\sf e}_{5},{\sf e}_{6}\\})\ \mid\ {\sf
task}({\sf e}_{5},{\sf e}_{7},{\sf p}_{c},{\sf p}_{bs},\mathsf{abort})\ \mid\
{\sf end}({\sf e}_{7},{\sf e}_{8})\ \mid\\\ {\sf task}({\sf e}_{6},{\sf
e}_{9},{\sf p}_{c},{\sf p}_{bs},\mathsf{book})\ \mid\ {\sf task}({\sf
e}_{9},{\sf e}_{10},{\sf p}_{c},{\sf p}_{bk},\mathsf{pay})\ \mid\ {\sf
task}({\sf e}_{10},{\sf e}_{11},{\sf p}_{bk},{\sf
p}_{bs},\mathsf{confirmation})\ \mid\\\ {\sf task}({\sf e}_{11},{\sf
e}_{12},{\sf p}_{bs},{\sf p}_{c},\mathsf{ticket})\ \mid\ {\sf end}({\sf
e}_{12},{\sf e}_{13})\end{array}$

The operational semantics we propose is given in terms of configurations of
the form $\langle Ch,\sigma\rangle$, where $Ch$ is a choreography structure,
and $\sigma$ is the execution state storing for each edge the current number
of tokens marking it. Specifically, a state
$\sigma:\mathbb{E}\rightarrow\mathbb{N}$ is a function mapping edges to
numbers of tokens. The state obtained by updating in the state $\sigma$ the
number of tokens of the edge ${\sf e}$ to ${\sf n}$, written as
$\sigma\cdot\\{{\sf e}\mapsto{\sf n}\\}$, is defined as follows:
$(\sigma\cdot\\{{\sf e}\mapsto{\sf n}\\})({\sf e}^{\prime})$ returns ${\sf n}$
if ${\sf e}^{\prime}={\sf e}$, otherwise it returns $\sigma({\sf
e}^{\prime})$. The _initial state_ , where all edges are unmarked is denoted
by $\sigma_{0}$ formally, $\sigma_{0}({\sf e})=0\ \ \forall{\sf
e}\in\mathbb{E}$. The transition relation over configurations, written
$\xrightarrow[]{l}$ and defined by the rules in Fig. 6, formalizes the
execution of a choreography in terms of marking evolution and message
exchanges. Labels $l$ represent computational steps and are defined as:
$\tau$, denoting internal computations; and ${\sf p}_{1}\rightarrow{\sf
p}_{2}:{\sf m}$, denoting an exchange of message ${\sf m}$ from participant
${\sf p}_{1}$ to ${\sf p}_{2}$. Notably, despite the presence of labels, this
has to be thought of as a reduction semantics, because labels are not used for
synchronization (as instead it usually happens in labeled semantics), but only
for keeping track of the exchanged messages in order to enable the conformance
checking discussed later on. Since choreography execution only affects the
current state, for the sake of presentation, we omit the choreography
structure from the target configurations of transitions. Thus, a transition
$\langle Ch,\sigma\rangle\xrightarrow[]{l}\langle Ch,\sigma^{\prime}\rangle$
is written as $\langle Ch,\sigma\rangle\xrightarrow[]{l}\sigma^{\prime}$.

Before commenting on the rules, we introduce the auxiliary functions they
exploit. Specifically, function
$\mathit{inc}:\mathbb{S}\times\mathbb{E}\rightarrow\mathbb{S}$ (resp.
$\mathit{dec}:\mathbb{S}\times\mathbb{E}\rightarrow\mathbb{S}$), where
$\mathbb{S}$ is the set of states, allows updating a state by incrementing
(resp. decrementing) by one the number of tokens marking an edge in the state.
Formally, they are defined as follows: $inc(\sigma,{\sf e})=\sigma\cdot\\{{\sf
e}\mapsto\sigma({\sf e})+1\\}$ and $dec(\sigma,{\sf e})=\sigma\cdot\\{{\sf
e}\mapsto\sigma({\sf e})-1\\}$. These functions extend in a natural ways to
sets of edges as follows: $inc(\sigma,\emptyset)=\sigma$ and
$inc(\sigma,\\{{\sf e}\\}\cup E)=inc(inc(\sigma,{\sf e}),E)$; the cases for
$dec$ are similar.

<EMAIL_ADDRESS>\<EMAIL_ADDRESS><EMAIL_ADDRESS>5.69046pt\ \lx@intercol\hfil\hskip
8.5359pt&&\\\\[-5.69046pt] \hskip 5.69046pt\
\lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf start}({\sf
e}_{o}),\sigma_{0}\rangle\xrightarrow[]{\tau}inc(\sigma_{0},{\sf
e}_{o})\end{array}\hfil\hskip
8.5359pt&&\quad(\mathit{Ch\textrm{-}Start})\\\\[17.07182pt] \hskip 5.69046pt\
\lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf end}({\sf e}_{i},{\sf
e}_{c}),\sigma\rangle\xrightarrow[]{\tau}inc(dec(\sigma,{\sf e}_{i}),{\sf
e}_{c})\end{array}\hfil\hskip 8.5359pt&\sigma({\sf
e}_{i})>0&\quad(\mathit{Ch\textrm{-}End})\\\\[17.07182pt] \hskip 5.69046pt\
\lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf andSplit}({\sf
e}_{i},E_{o}),\sigma\rangle\xrightarrow[]{\tau}inc(dec(\sigma,{\sf
e}_{i}),E_{o})\end{array}\hfil\hskip 8.5359pt&\sigma({\sf
e}_{i})>0&\quad(\mathit{Ch\textrm{-}AndSplit})\\\\[17.07182pt] \hskip
5.69046pt\ \lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf
andJoin}(E_{i},{\sf
e}_{o}),\sigma\rangle\xrightarrow[]{\tau}inc(dec(\sigma,E_{i}),{\sf
e}_{o})\end{array}\hfil\hskip 8.5359pt&\\!\\!\\!\\!\forall{\sf e}\in
E_{i}.\sigma({\sf e})>0&\quad(\mathit{Ch\textrm{-}AndJoin})\\\\[17.07182pt]
\hskip 5.69046pt\ \lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf
xorSplit}({\sf e}_{i},\\{{\sf e}\\}\cup
E_{o}),\sigma\rangle\xrightarrow[]{\tau}inc(dec(\sigma,{\sf e}_{i}),{\sf
e})\end{array}\hfil\hskip 8.5359pt&\sigma({\sf
e}_{i})>0&\quad(\mathit{Ch\textrm{-}XorSplit})\\\\[17.07182pt] \hskip
5.69046pt\ \lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf
xorJoin}(\\{{\sf e}\\}\cup E_{i},{\sf
e}_{o}),\sigma\rangle\xrightarrow[]{\tau}inc(dec(\sigma,{\sf e}),{\sf
e}_{o})\end{array}\hfil\hskip 8.5359pt&\sigma({\sf
e})>0&\quad(\mathit{Ch\textrm{-}XorJoin})\\\\[17.07182pt] \hskip 5.69046pt\
\lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf task}({\sf e}_{i},{\sf
e}_{o},{\sf p}_{1},{\sf p}_{2},{\sf m}),\sigma\rangle\xrightarrow[]{{\sf
p}_{1}\rightarrow{\sf p}_{2}:{\sf m}}inc(dec(\sigma,{\sf e}_{i}),{\sf
e}_{o})\end{array}\hfil\hskip 8.5359pt&\begin{array}[]{l}\sigma({\sf
e}_{i})>0\\\ \end{array}&\quad(\mathit{Ch\textrm{-}Task})\\\\[17.07182pt]
\hskip 5.69046pt\ \lx@intercol\begin{array}[]{l}\\!\\!\\!\\!\langle{\sf
eventBased}({\sf e}_{i},{\sf}({\sf e}_{o},{\sf p}_{1},{\sf p}_{2},{\sf m})\cup
T),\sigma\rangle\xrightarrow[]{{\sf p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}inc(dec(\sigma,{\sf e}_{i}),{\sf e}_{o})\end{array}\hfil\hskip
8.5359pt&\sigma({\sf
e}_{i})>0&\quad(\mathit{Ch\textrm{-}EventG})\\\\[17.07182pt]
\vrule\lx@intercol\hfil\begin{array}[]{l}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 7.23631pt\hbox{$\displaystyle\penalty 1\langle
Ch_{1},\sigma\rangle\xrightarrow[]{l}\sigma^{\prime}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.19997pt,depth=0.19997pt,width=55.86433pt\hbox{\kern 2.40002pt$\ \
(\mathit{Ch\textrm{-}Int_{1}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\langle
Ch_{1}\\!\\!\mid\\!Ch_{2},\sigma\rangle\xrightarrow[]{l}\sigma^{\prime}$}}}}\\\
\end{array}\qquad\begin{array}[]{l}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 7.23631pt\hbox{$\displaystyle\penalty 1\langle
Ch_{2},\sigma\rangle\xrightarrow[]{l}\sigma^{\prime}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.19997pt,depth=0.19997pt,width=55.86433pt\hbox{\kern 2.40002pt$\ \
(\mathit{Ch\textrm{-}Int_{2}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\langle
Ch_{1}\\!\\!\mid\\!Ch_{2},\sigma\rangle\xrightarrow[]{l}\sigma^{\prime}$}}}}\\\
\end{array}\hfil\lx<EMAIL_ADDRESS>\hline\cr\end{array}$ Figure 6. Choreography Semantics.

We now briefly comment on the operational rules in Fig. 6. Rule
$\mathit{Ch\textrm{-}Start}$ starts the execution of a choreography when it is
in its initial state (i.e., all edges are unmarked). The effect of the rule is
to increment the number of tokens in the edge outgoing from the start event.
Rule $\mathit{Ch\textrm{-}End}$ instead is enabled when there is at least a
token in the incoming edge of the end event, which is then moved to the
spurious edge to keep track that a token ended up in the event. Rule
$\mathit{Ch\textrm{-}AndSplit}$ is applied when there is at least one token in
the incoming edge of an AND split gateway; as result of its application the
rule decrements the number of tokens in the incoming edge and increments that
in each outgoing edge. Rule $\mathit{Ch\textrm{-}AndJoin}$ decrements the
tokens in each incoming edge and increments the number of tokens of the
outgoing edge, when each incoming edge has at least one token. Rule
$\mathit{Ch\textrm{-}XorSplit}$ is applied when a token is available in the
incoming edge of an XOR split gateway, the rule decrements this token and
increments the tokens in one of the outgoing edges. Rule
$\mathit{Ch\textrm{-}XorJoin}$ is activated every time there is a token in one
of the incoming edges, which is then moved to the outgoing edge. Rule
$\mathit{Ch\textrm{-}Task}$ is activated when there is a token in the incoming
edge of a choreography task, so that the application of the rule produces a
message exchange label and moves the token from the incoming edge to the
outgoing one. Rule $\mathit{Ch\textrm{-}EventG}$ is activated each time there
is a token in the incoming edge, which is moved to the outgoing edge of one
task in the enclosed list, and produces a message exchange label. Different
message exchanges can take place; the selection of the executed task from the
list specified in the gateway is non-deterministic, in order to properly model
the race condition regulating the behaviour of the event-based gateway.
Finally, rules $\mathit{Ch\textrm{-}Int_{1}}$ and
$\mathit{Ch\textrm{-}Int_{2}}$ deal with interleaving.

Let $Ch_{i}$ be the choreography structure defined in Example 4. The initial
configuration of the collaboration is $\langle Ch_{i},\sigma_{0}\rangle$,
where $\sigma_{0}({\sf e}_{i})=0\ \ \forall\,i\in\\{1,\ldots,13\\}$. The state
$\sigma_{1}$ obtained by applying the rule $\mathit{Ch\textrm{-}Start}$, which
marks the edge ${\sf e}_{1}$, is obtained as follows:
$\sigma_{1}=inc(\sigma_{0},{\sf e}_{1})$.

#### From Processes to Collaborations.

According to the $C^{4}$ methodology described in Section 3, a choreography is
enacted by collaborations resulting from the combination of sets of processes.
We formalise here the notions of process, collaboration, and process
composition.

The BNF syntax of the process model structure is given in Fig. 7. The non-
terminal symbol $P$ represents _Process Structures_ , while terminal symbols
denote, as usual, the considered elements. In a process model there are three
types of tasks, i.e. non-communicating (${\sf task}$), receiving (${\sf
taskRcv}$) and sending (${\sf taskSnd}$), and also two intermediate events,
i.e. receiving (${\sf interRcv}$) and sending (${\sf interSnd}$). Each
receiving/sending elements specifies an exchanged message, while an event-
based gateway specifies a list of (at least two) messages, each one enriched
with the outgoing edge enabled by the message reception. When convenient, we
shall regard a message list simply as a set.

Let us consider the BPMN process model in Fig 4.b. The textual representation
of its structure is as follow:

$\begin{array}[]{l}{\sf start}({\sf e}_{1}^{\prime})\ \mid\ {\sf taskSnd}({\sf
e}_{1}^{\prime},{\sf e}_{2}^{\prime},{\sf login})\ \mid\ {\sf taskSnd}({\sf
e}_{2}^{\prime},{\sf e}_{3}^{\prime},{\sf request})\ \mid\ {\sf taskRcv}({\sf
e}_{3}^{\prime},{\sf e}_{4}^{\prime},{\sf reply})\ \mid\\\ {\sf xorSplit}({\sf
e}_{4}^{\prime},\\{{\sf e}_{5}^{\prime},{\sf e}_{6}^{\prime}\\})\ \mid\ {\sf
taskSnd}({\sf e}_{5}^{\prime},{\sf e}_{7}^{\prime},{\sf abort})\ \mid\ {\sf
end}({\sf e}_{7}^{\prime},{\sf e}_{8}^{\prime})\ \mid\ {\sf taskSnd}({\sf
e}_{6}^{\prime},{\sf e}_{9}^{\prime},{\sf book})\ \mid\\\ {\sf taskSnd}({\sf
e}_{9}^{\prime},{\sf e}_{10}^{\prime},{\sf pay})\ \mid\ {\sf taskRcv}({\sf
e}_{11}^{\prime},{\sf e}_{12}^{\prime},{\sf ticket})\ \mid\ {\sf end}({\sf
e}_{12}^{\prime},{\sf e}_{13}^{\prime})\end{array}$

$\begin{array}[]{|@{\ }rcl@{\ }|}\hline\cr&&\\\\[-5.69046pt] P&::=&{\sf
start}({\sf e}_{o})\mid{\sf end}({\sf e}_{i},{\sf e}_{c})\mid{\sf
andJoin}(E_{i},{\sf e}_{o})\mid{\sf xorSplit}({\sf e}_{i},E_{o})\mid{\sf
andSplit}({\sf e}_{i},E_{o})\mid{\sf xorJoin}(E_{i},{\sf
e}_{o})\\\\[2.84544pt] &\mid&{\sf task}({\sf e}_{i},{\sf e}_{o})\mid\ {\sf
taskRcv}({\sf e}_{i},{\sf e}_{o},{{\sf m}})\mid\ {\sf taskSnd}({\sf
e}_{i},{\sf e}_{o},{{\sf m}})\mid\ {\sf interRcv}({\sf e}_{i},{\sf
e}_{o},{{\sf m}})\mid\ {\sf interSnd}({\sf e}_{i},{\sf e}_{o},{{\sf
m}})\\\\[2.84544pt] &\mid&{\sf eventBased}({\sf e}_{i},M_{1},M_{2})\ \mid\
P_{1}\\!\\!\mid\\!P_{2}\\\\[2.84544pt] M&::=&({\sf m},{\sf e}_{o})\ \ \mid\ \
M_{1},M_{2}\\\\[2.84544pt] \hline\cr\end{array}$

Figure 7. Syntax of Processes Structures.

The BNF syntax of the collaboration model structure is given in Fig. 8, where
the non-terminal symbol $C$ represents _Collaboration Structures_. Each
process involved in a collaboration is identified by a participant name,
denoted by ${\sf p}$. The exchange of messages in a collaboration is modeled
by means of _message edges_. Here, they are represented by triples of the form
$({\sf p}_{1},{\sf p}_{2},{\sf m})$ indicating, in order, the sending
participant, the receiving participant and the message. Accordingly, an event-
based gateway specifies a list of (at least two) message edges.

Let us consider the BPMN collaboration model in Fig 2.b. The textual
representation of its structure is as follow:

$C_{bk}\ \mid\ C_{bs}\ \mid\ C_{c}$

where:

$\begin{array}[]{l@{\ }l}\\\ C_{bk}::=&{\sf start}({\sf
e}_{1}^{\prime\prime\prime})\ \mid\ {\sf taskRcv}({\sf
e}_{1}^{\prime\prime\prime},{\sf e}_{2}^{\prime\prime\prime},({\sf p}_{c},{\sf
p}_{bk},\sf pay))\ \mid\\\ &{\sf taskSnd}({\sf
e}_{2}^{\prime\prime\prime},{\sf e}_{3}^{\prime\prime\prime},({\sf
p}_{bk},{\sf p}_{bs},\sf confirmation))\ \mid\ {\sf end}({\sf
e}_{3}^{\prime\prime\prime},{\sf e}_{4}^{\prime\prime\prime})\\\ \end{array}$
$\begin{array}[]{l@{\ }l}C_{bs}::=&{\sf start}({\sf e}_{1}^{\prime\prime})\
\mid\ {\sf taskRcv}({\sf e}_{1}^{\prime\prime},{\sf
e}_{2}^{\prime\prime},({\sf p}_{c},{\sf p}_{bs},\sf login))\ \mid\ {\sf
taskRcv}({\sf e}_{2}^{\prime\prime},{\sf e}_{3}^{\prime\prime},({\sf
p}_{c},{\sf p}_{bs},\sf request))\ \mid\\\ &{\sf taskSnd}({\sf
e}_{3}^{\prime\prime},{\sf e}_{4}^{\prime\prime},({\sf p}_{bs},{\sf p}_{c},\sf
reply))\ \mid\\\ &{\sf eventBased}({\sf e}_{4}^{\prime\prime},({\sf
p}_{c},{\sf p}_{bs},\sf abort,{\sf e}_{5}^{\prime\prime}),({\sf p}_{c},{\sf
p}_{bs},\sf book,{\sf e}_{6}^{\prime\prime}))\ \mid\ {\sf end}({\sf
e}_{5}^{\prime\prime},{\sf e}_{7}^{\prime\prime})\ \mid\\\ &{\sf taskRcv}({\sf
e}_{6}^{\prime\prime},{\sf e}_{8}^{\prime\prime},({\sf p}_{bk},{\sf
p}_{bs},\sf confirmation))\ \mid\ {\sf taskSnd}({\sf
e}_{8}^{\prime\prime},{\sf e}_{9}^{\prime\prime},({\sf p}_{bs},{\sf p}_{c},\sf
ticket))\ \mid\\\ &{\sf end}({\sf e}_{9}^{\prime\prime},{\sf
e}_{10}^{\prime\prime})\\\ &\\\ C_{c}::=&{\sf start}({\sf e}_{1}^{\prime})\
\mid\ {\sf taskSnd}({\sf e}_{1}^{\prime},{\sf e}_{2}^{\prime},({\sf p}_{{\sf
p}_{bk}},{\sf p}_{bs},\mathsf{login}))\ \mid\ {\sf taskSnd}({\sf
e}_{2}^{\prime},{\sf e}_{3}^{\prime},({\sf p}_{{\sf p}_{bk}},{\sf
p}_{bs},\mathsf{request}))\ \mid\\\ &{\sf taskRcv}({\sf e}_{3}^{\prime},{\sf
e}_{4}^{\prime},({\sf p}_{bs},{\sf p}_{{\sf p}_{bk}},\mathsf{reply}))\ \mid\
{\sf xorSplit}({\sf e}_{4}^{\prime},\\{{\sf e}_{5}^{\prime},{\sf
e}_{6}^{\prime}\\})\ \mid\\\ &{\sf taskSnd}({\sf e}_{5}^{\prime},{\sf
e}_{7}^{\prime},({\sf p}_{{\sf p}_{bk}},{\sf p}_{bs},\mathsf{abort}))\ \mid\
{\sf end}({\sf e}_{7}^{\prime},{\sf e}_{8}^{\prime})\ \mid\ {\sf taskSnd}({\sf
e}_{6}^{\prime},{\sf e}_{9}^{\prime},({\sf p}_{{\sf p}_{bk}},{\sf
p}_{bs},\mathsf{book}))\ \mid\\\ &{\sf taskSnd}({\sf e}_{9}^{\prime},{\sf
e}_{10}^{\prime},({\sf p}_{{\sf p}_{bk}},{\sf p}_{bk},\mathsf{pay}))\ \mid\
{\sf taskRcv}({\sf e}_{11}^{\prime},{\sf e}_{12}^{\prime},({\sf p}_{bk},{\sf
p}_{bs},\mathsf{ticket}))\ \mid\ {\sf end}({\sf e}_{12}^{\prime},{\sf
e}_{13}^{\prime})\end{array}$

$\begin{array}[]{|@{\ }rcl@{\ }|}\hline\cr&&\\\\[-5.69046pt] C&::=&{\sf
start}({\sf e}_{o})\mid{\sf end}({\sf e}_{i},{\sf e}_{c})\mid{\sf
andJoin}(E_{i},{\sf e}_{o})\mid{\sf xorSplit}({\sf e}_{i},E_{o})\mid{\sf
andSplit}({\sf e}_{i},E_{o})\mid{\sf xorJoin}(E_{i},{\sf
e}_{o})\\\\[2.84544pt] &\mid&{\sf task}({\sf e}_{i},{\sf e}_{o})\mid\ {\sf
taskRcv}({\sf e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf m}))\mid\ {\sf
taskSnd}({\sf e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf
m}))\\\\[2.84544pt] &\mid&{\sf interRcv}({\sf e}_{i},{\sf e}_{o},({\sf
p}_{1},{\sf p}_{2},{\sf m}))\mid\ {\sf interSnd}({\sf e}_{i},{\sf e}_{o},({\sf
p}_{1},{\sf p}_{2},{\sf m}))\mid\ {\sf eventBased}({\sf
e}_{i},\mathit{ME}_{1},\mathit{ME}_{2})\ \mid\
C_{1}\\!\\!\mid\\!C_{2}\\\\[2.84544pt] \mathit{ME}&::=&({\sf p}_{1},{\sf
p}_{2},{\sf m},{\sf e}_{o})\ \ \mid\ \
\mathit{ME}_{1},\mathit{ME}_{2}\\\\[2.84544pt] \hline\cr\end{array}$

Figure 8. Syntax of Collaboration Structures.

When composing processes in order to form collaborations, we must properly
connect via a message edge each task (or intermediate event) of a process
sending a given message with a corresponding receiving element belonging to
another process, and vice versa. Hence, the resulting collaboration should not
contain disconnected communicating elements. To formalise this property, we
need to introduce the auxiliary functions ${out}(C)$ and ${in}(C)$, which
return, respectively, the (multi)sets of message edges outgoing from and
incoming into a communicating element in the collaboration $C$:

$\begin{array}[]{l}{out}(C)=\left\\{\begin{array}[]{@{}l@{\ }l}\\{({\sf
p}_{1},{\sf p}_{2},{\sf m})\\}&\begin{array}[]{l}\mathrm{if}\ C\\!=\\!{\sf
taskSnd}({\sf e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf m}))\\\ \
\mathrm{or}\ C\\!=\\!{\sf interSnd}({\sf e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf
p}_{2},{\sf m}))\end{array}\\\\[11.38092pt]
{out}(C_{1})\\!\uplus\\!{out}(C_{2})&\begin{array}[]{l}\mathrm{if}\
C\\!=\\!C_{1}\\!\\!\mid\\!C_{2}\end{array}\\\\[5.69046pt]
\emptyset&\begin{array}[]{l}\mathrm{otherwise}\end{array}\end{array}\right.\\\\[36.98866pt]
{in}(C)=\left\\{\begin{array}[]{@{}l@{\ }l}\\{({\sf p}_{1},{\sf p}_{2},{\sf
m})\\}&\begin{array}[]{l}\mathrm{if}\ C\\!=\\!{\sf taskRcv}({\sf e}_{i},{\sf
e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf m}))\\\ \ \mathrm{or}\ C\\!=\\!{\sf
interRcv}({\sf e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf
m}))\end{array}\\\\[11.38092pt]
{in}(\mathit{ME})&\begin{array}[]{l}\mathrm{if}\ C\\!=\\!{\sf eventBased}({\sf
e}_{i},\mathit{ME})\end{array}\\\\[5.69046pt]
{in}(C_{1})\uplus{in}(C_{2})&\begin{array}[]{l}\mathrm{if}\
C\\!=\\!C_{1}\\!\\!\mid\\!C_{2}\end{array}\\\\[5.69046pt]
\emptyset&\begin{array}[]{l}\mathrm{otherwise}\end{array}\end{array}\right.\\\\[42.67912pt]
{in}(({\sf p}_{1},{\sf p}_{2},{\sf m},{\sf e}_{o}))=\\{({\sf p}_{1},{\sf
p}_{2},{\sf
m})\\}\qquad\qquad{in}(\mathit{ME}_{1},\mathit{ME}_{2})={in}(\mathit{ME}_{1})\uplus{in}(\mathit{ME}_{2})\end{array}$

where $\uplus$ denotes the multiset union operator.

We can now formally define the well-composedness property for collaborations.

[Well-composed collaboration] Let $C$ be a collaboration, $C$ is well-composed
if ${out}(C)={in}(C)$ and $\forall({\sf p}_{1},{\sf p}_{2},{\sf
m})\in{out}(C)\cup{in}(C)\ .\ {\sf p}_{1}\neq{\sf p}_{2}$.

Let consider the processes _a_ , _b_ and _d_ in Fig. 4. By associating them
the participant names ${\sf p}_{bk}$, ${\sf p}_{c}$ and ${\sf p}_{bs}$,
respectively, and by composing them we obtain the collaboration model $C_{1}$
in Fig 2.b. This is well-composed, because we have:

$\begin{array}[]{l@{}l@{}l}{out}(C_{1})={in}(C_{1})&=&\\{({\sf p}_{bk},{\sf
p}_{bs},\mathsf{confirmation}),({\sf p}_{bs},{\sf p}_{c},\mathsf{reply}),({\sf
p}_{bs},{\sf p}_{c},\mathsf{ticket}),({\sf p}_{c},{\sf
p}_{bs},\mathsf{login}),\\\ &&\ \ ({\sf p}_{c},{\sf
p}_{bs},\mathsf{request}),({\sf p}_{c},{\sf p}_{bs},\mathsf{abort}),({\sf
p}_{c},{\sf p}_{bs},\mathsf{book}),({\sf p}_{c},{\sf
p}_{bk},\mathsf{pay})\\}\end{array}$

Now, let us consider to replace the process _d_ by the process _e_ in Fig 4,
which adds an extra behaviour sending an acknowledge message that we suppose
targeted to the customer participant. In this case, however, the resulting
composition is the collaboration $C_{2}$ that is not well-composed. Indeed,
the set ${out}(C_{2})$ contains the message edge $({\sf p}_{bs},{\sf
p}_{c},ack)$ that is not in ${in}(C_{2})$. Graphically, this corresponds to a
malformed BPMN model with a message edge outgoing from a task of a pool but
not connected with a task of another pool.

Before presenting our formalisation of collaboration creation via processes
composition, we need to introduce few notations and auxiliary functions.
Firstly, notation $\overline{\cdot}$ stands for tuples, with $\mid{\cdot}\mid$
denoting the tuple length and $\cdot\downarrow_{i}$ denoting the i-th element
of the tuple. For example, $\overline{{\sf p}}$ represents a tuple of
participant names $\langle{\sf p}_{1},\ldots,{\sf p}_{n}\rangle$, with $n\geq
0$, and hence $\mid{\overline{{\sf p}}}\mid=n$ and $\overline{{\sf
p}}\downarrow_{i}={\sf p}_{i}$ for $i\in\\{1,\ldots,n\\}$. Secondly, since the
operator $\mid$ is associative, we can generalise it to an n-ary operator and
use the notation $\prod$ to represent its iterated version. For example,
$\prod_{i=1}^{n}C_{i}=C_{1}\mid\ldots\mid C_{n}$. Finally, we will resort to
the auxiliary functions $S$ and $R$ that, given a message, return the sender
and the receiver participant, respectively. $S$ and $R$ are written as
collections of pairs of the form ${\sf m}\mapsto{\sf p}$. We use $\emptyset$
to denote the empty message function (i.e., $\emptyset({\sf m})$ is undefined
for any ${\sf m}$), and $S_{1}\sqcup S_{2}$ (resp. $R_{1}\sqcup R_{2}$) to
denote the union of $S_{1}$ and $S_{2}$ (resp. $R_{1}$ and $R_{2}$) when they
have disjoint domain. We will also generalise $\sqcup$ to the n-ary operator
$\bigsqcup$.

Let us now to formally define how a set of processes can be associated to
process names and composed together in order to form a collaboration, which is
defined according to the syntax given in Fig. 8.

[Processes composition function] Let $\overline{P}$ and $\overline{{\sf p}}$
be a tuple of processes and a tuple of participant names, respectively; their
composition is defined by the function $\mathcal{C}$ as follows:

$\mathcal{C}(\overline{P},\overline{{\sf
p}})=\prod_{i=1}^{n}\mathcal{N}(\overline{P}\downarrow_{i},\mathcal{S}(\overline{P},\overline{{\sf
p}}),\mathcal{R}(\overline{P},\overline{{\sf p}}))$

with $\mid{\overline{P}}\mid=\mid{\overline{{\sf p}}}\mid=n$. Functions
$\mathcal{S}$ and $\mathcal{R}$, computing the message functions for the given
processes and the corresponding names, are defined as follows:

$\begin{array}[]{l}\mathcal{S}(\overline{P},\overline{{\sf
p}})=\bigsqcup_{i\in\\{1,\ldots,n\\}}\mathcal{S}(\overline{P}\downarrow_{i},\overline{{\sf
p}}\downarrow_{i})\quad\mathrm{with}\
\mid{\overline{P}}\mid=\mid{\overline{{\sf p}}}\mid=n\\\\[8.5359pt]
\mathcal{S}(P_{1}\mid P_{2},{\sf p})=\mathcal{S}(P_{1},{\sf
p})\sqcup\mathcal{S}(P_{2},{\sf p})\\\\[8.5359pt] \mathcal{S}({\sf
taskSnd}({\sf e}_{i},{\sf e}_{o},{\sf m}),{\sf p})=\mathcal{S}({\sf
interSnd}({\sf e}_{i},{\sf e}_{o},{{\sf m}}),{\sf p})=\\{{\sf m}\mapsto{\sf
p}\\}\\\\[8.5359pt] \mathcal{S}(P,{\sf p})=\emptyset\quad\mathrm{for\ any}\ P\
\mathrm{different\ from}\ {\sf taskSnd}\ \mathrm{and}\ {\sf
interSnd}\end{array}$
$\begin{array}[]{l}\mathcal{R}(\overline{P},\overline{{\sf
p}})=\bigsqcup_{i\in\\{1,\ldots,n\\}}\mathcal{R}(\overline{P}\downarrow_{i},\overline{{\sf
p}}\downarrow_{i})\quad\mathrm{with}\
\mid{\overline{P}}\mid=\mid{\overline{{\sf p}}}\mid=n\\\\[8.5359pt]
\mathcal{R}(P_{1}\mid P_{2},{\sf p})=\mathcal{R}(P_{1},{\sf
p})\sqcup\mathcal{R}(P_{2},{\sf p})\\\\[8.5359pt] \mathcal{R}({\sf
taskRcv}({\sf e}_{i},{\sf e}_{o},{\sf m}),{\sf p})=\mathcal{R}({\sf
interRcv}({\sf e}_{i},{\sf e}_{o},{{\sf m}}),{\sf p})=\\{{\sf m}\mapsto{\sf
p}\\}\\\\[8.5359pt] \mathcal{R}({\sf eventBased}({\sf e}_{i},M),{\sf
p})=\mathcal{R}(M,{\sf p})\\\\[8.5359pt] \mathcal{R}(({\sf m},{\sf
e}_{o}),{\sf p})=\\{{\sf m}\mapsto{\sf
p}\\}\qquad\mathcal{R}((M_{1},M_{2}),{\sf p})=\mathcal{R}(M_{1},{\sf
p})\sqcup\mathcal{R}(M_{2},{\sf p})\\\\[8.5359pt] \mathcal{R}(P,{\sf
p})=\emptyset\quad\mathrm{for\ any}\ P\ \mathrm{different\ from}\ {\sf
taskRcv},\ {\sf interRcv}\ \mathrm{and}\ {\sf eventBased}\end{array}$

Finally, the naming function $\mathcal{N}$ is defined by the following
relevant cases (in the remaining cases, the function acts as an homomorphism):

$\begin{array}[]{l}\mathcal{N}(P_{1}\mid
P_{2},S,R)=\mathcal{N}(P_{1},S,R)\,\mid\,\mathcal{N}(P_{2},S,R)\\\\[8.5359pt]
\mathcal{N}({\sf taskSnd}({\sf e}_{i},{\sf e}_{o},{\sf m}),S,R)={\sf
taskSnd}({\sf e}_{i},{\sf e}_{o},(S({\sf m}),R({\sf m}),{\sf
m}))\quad\mathrm{if}\ S({\sf m})\neq R({\sf m})\\\\[8.5359pt] \mathcal{N}({\sf
interSnd}({\sf e}_{i},{\sf e}_{o},{{\sf m}}),S,R)={\sf interSnd}({\sf
e}_{i},{\sf e}_{o},(S({\sf m}),R({\sf m}),{\sf m}))\quad\mathrm{if}\ S({\sf
m})\neq R({\sf m})\\\\[8.5359pt] \mathcal{N}({\sf taskRcv}({\sf e}_{i},{\sf
e}_{o},{\sf m}),S,R)={\sf taskRcv}({\sf e}_{i},{\sf e}_{o},(S({\sf m}),R({\sf
m}),{\sf m}))\quad\mathrm{if}\ S({\sf m})\neq R({\sf m})\\\\[8.5359pt]
\mathcal{N}({\sf interRcv}({\sf e}_{i},{\sf e}_{o},{{\sf m}}),S,R)={\sf
interRcv}({\sf e}_{i},{\sf e}_{o},(S({\sf m}),R({\sf m}),{\sf
m}))\quad\mathrm{if}\ S({\sf m})\neq R({\sf m})\\\\[8.5359pt] \mathcal{N}({\sf
eventBased}({\sf e}_{i},M),S,R)={\sf eventBased}({\sf
e}_{i},\mathcal{N}(M,S,R))\\\\[8.5359pt] \mathcal{N}(({\sf m},{\sf
e}_{o}),S,R)=(S({\sf m}),R({\sf m}),{\sf m},{\sf e}_{o})\quad\mathrm{if}\
S({\sf m})\neq R({\sf m})\end{array}$

Intuitively, function $\mathcal{C}$ extracts from the processes to be composed
the information concerning sending and receiving participants for all
exchanged messages, and uses this information for enriching the message edges
of each process. Specifically, function $\mathcal{S}$ identifies as a sender
of a message a participant that performs a sending task or a sending
intermediate event with that message as an argument, while function
$\mathcal{R}$ identifies as a receiver of a message a participant performing a
receiving task, a receiving intermediate event or a an event-based gateway on
the message. If the function $\mathcal{C}$ returns a collaboration, this is
well-composed; otherwise the function is undefined, meaning that the processes
given in input cannot be correctly composed to form a collaboration. This is
formalised by the following proposition.

######  Proposition 1.

Let $\overline{P}$ and $\overline{{\sf p}}$ be a tuple of processes and a
tuple of participant names, respectively; if
$\mathcal{C}(\overline{P},\overline{{\sf p}})=C$ then $C$ is well-composed.

######  Proof 4.1.

The proof proceeds by contradiction (see the Appendix).

Let $P_{a}$, $P_{b}$ and $P_{d}$ be the textual representation of processes
_a_ , _b_ and _d_ in Fig. 4. Their composition is formally defined as
$\mathcal{C}(\langle P_{a},P_{b},P_{d}\rangle,\langle{\sf p}_{bk},{\sf
p}_{c},{\sf p}_{bs}\rangle)=(C_{bk}\ \mid\ C_{bs}\ \mid\ C_{c})$, with
$C_{bk}$, $C_{bs}$ and $C_{c}$ defined in Example 4.

#### Semantics of Collaborations.

The operational semantics we propose for collaborations is given in terms of
configurations of the form $\langle C,\sigma,\delta\rangle$, where: $C$ is a
collaboration structure; $\sigma$ is the first part of the execution state,
storing for each sequence edge the current number of tokens marking it; and
$\delta$ is the second part of the execution state, storing for each message
edge the current number of message tokens marking it. Specifically,
$\delta:\mathbb{M}\rightarrow\mathbb{N}$ is a function mapping message edges
to numbers of message tokens; so that $\delta{({\sf p}_{1},{\sf p}_{2},{\sf
m})}={\sf n}$ means that there are ${\sf n}$ messages of type ${\sf m}$ sent
by ${\sf p}_{1}$ and stored in the ${\sf p}_{2}$’s queue. Update and initial
state for $\delta$ are defined in a way similar to $\sigma$’s definitions.

The transition relation $\xrightarrow[]{l}$ over collaboration configurations
formalizes the execution of a collaboration in terms of edge and message
markings evolution. It is defined by the rules in Fig. 9; for the sake of
presentation, we omit the rules concerning start/end events and gateways, as
they are the same of those for choreographies (reported in Fig. 6). As usual,
we omit the collaboration structure from the target configuration of
transitions.

<EMAIL_ADDRESS>\<EMAIL_ADDRESS><EMAIL_ADDRESS>5.69046pt\ \lx@intercol\hfil\hskip
8.5359pt&&\\\\[-5.69046pt] \hskip 5.69046pt\
\lx@intercol\begin{array}[]{l}\langle{\sf eventBased}({\sf e}_{i},({\sf
p}_{1},{\sf p}_{2},{\sf m},{\sf e}_{o})\cup
M),\sigma,\delta\rangle\xrightarrow[]{{\sf p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}\langle inc(dec(\sigma,{\sf e}_{i}),{\sf e}_{o}),dec(\delta,({\sf
p}_{1},{\sf p}_{2},{\sf m}))\rangle\end{array}\hfil\hskip
8.5359pt&\begin{array}[]{l}\sigma({\sf e}_{i})>0,\\\ \delta{({\sf p}_{1},{\sf
p}_{2},{\sf
m})}\\!\\!>\\!\\!0\end{array}&\quad(\mathit{C\textrm{-}EventG})\\\\[17.07182pt]
\hskip 5.69046pt\ \lx@intercol\begin{array}[]{l}\langle{\sf task}({\sf
e}_{i},{\sf e}_{o}),\sigma,\delta\rangle\xrightarrow[]{\tau}\langle
inc(dec(\sigma,{\sf e}_{i}),{\sf e}_{o}),\delta\rangle\end{array}\hfil\hskip
8.5359pt&\begin{array}[]{l}\sigma({\sf
e}_{i})>0\end{array}&\quad(\mathit{C\textrm{-}Task})\\\\[17.07182pt] \hskip
5.69046pt\ \lx@intercol\begin{array}[]{l}\langle{\sf taskRcv}({\sf e}_{i},{\sf
e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf
m})),\sigma,\delta\rangle\xrightarrow[]{{\sf p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}\langle inc(dec(\sigma,{\sf e}_{i}),{\sf e}_{o}),dec(\delta,({\sf
p}_{1},{\sf p}_{2},{\sf m}))\rangle\end{array}\hfil\hskip
8.5359pt&\begin{array}[]{l}\sigma({\sf e}_{i})>0,\\\ \delta{({\sf p}_{1},{\sf
p}_{2},{\sf
m})}\\!\\!>\\!\\!0\end{array}&\quad(\mathit{C\textrm{-}TaskRcv})\\\\[17.07182pt]
\hskip 5.69046pt\ \lx@intercol\begin{array}[]{l}\langle{\sf taskSnd}({\sf
e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf
m})),\sigma,\delta\rangle\xrightarrow[]{\tau}\langle inc(dec(\sigma,{\sf
e}_{i}),{\sf e}_{o}),inc(\delta,({\sf p}_{1},{\sf p}_{2},{\sf
m}))\rangle\end{array}\hfil\hskip 8.5359pt&\begin{array}[]{l}\sigma({\sf
e}_{i})>0\end{array}&\quad(\mathit{C\textrm{-}TaskSnd})\\\\[17.07182pt] \hskip
5.69046pt\ \lx@intercol\begin{array}[]{l}\langle{\sf interRcv}({\sf
e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf
m})),\sigma,\delta\rangle\xrightarrow[]{{\sf p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}\langle inc(dec(\sigma,{\sf e}_{i}),{\sf e}_{o}),dec(\delta,({\sf
p}_{1},{\sf p}_{2},{\sf m}))\rangle\end{array}\hfil\hskip
8.5359pt&\begin{array}[]{l}\sigma({\sf e}_{i})>0,\\\ \delta{({\sf p}_{1},{\sf
p}_{2},{\sf
m})}\\!\\!>\\!\\!0\end{array}&\quad(\mathit{C\textrm{-}InterRcv})\\\\[17.07182pt]
\hskip 5.69046pt\ \lx@intercol\begin{array}[]{l}\langle{\sf interSnd}({\sf
e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf
m})),\sigma,\delta\rangle\xrightarrow[]{\tau}\langle inc(dec(\sigma,{\sf
e}_{i}),{\sf e}_{o}),inc(\delta,({\sf p}_{1},{\sf p}_{2},{\sf
m}))\rangle\end{array}\hfil\hskip 8.5359pt&\begin{array}[]{l}\sigma({\sf
e}_{i})>0\end{array}&\quad(\mathit{C\textrm{-}InterSnd})\\\\[17.07182pt]
\hline\cr\end{array}$ Figure 9. Collaboration Semantics (excerpt of rules).

We now briefly comment on the operational rules. Rule
$\mathit{C\textrm{-}EventG}$ is activated when there is a token in the
incoming edge of an event-based gateway and there is a message ${\sf m}$ to be
consumed, so that the application of the rule moves the token from the
incoming edge to the outgoing edge corresponding to the received message,
whose number of message tokens in the meantime is decreased (i.e., a message
from the corresponding queue is consumed). Rule $\mathit{C\textrm{-}Task}$
deals with simple tasks, acting as a pass through. Rule
$\mathit{C\textrm{-}TaskRcv}$ is activated not only when there is a token in
the incoming edge, like the one related to simple tasks, but also when there
is a message to be consumed. Similarly, rule $\mathit{C\textrm{-}TaskSnd}$,
instead of consuming, adds a message in the corresponding queue. It is worth
noticing that rule $\mathit{C\textrm{-}TaskSnd}$ produces transitions labelled
by $\tau$, meaning that sending actions are not observable. This is because in
our conformance checking approach we compare the execution of a choreography
task only with the reception of the corresponding message in the
collaboration. We formalise this below in this section, and we provide a more
thorough discussion about this distinctive aspect of our proposal in Section
6. Rule $\mathit{C\textrm{-}InterRcv}$ (resp. $\mathit{C\textrm{-}InterSnd}$)
follows the same behavior of rule $\mathit{C\textrm{-}TaskRcv}$ (resp.
$\mathit{C\textrm{-}TaskSnd}$).

### Conformance Checking

This section discusses about the relations we propose for checking the
conformance between choreographies and collaborations. We then present how
they work in practice.

#### Bisimulation-Based and Trace-Based Conformance.

Here we present the Bisimulation-Based Conformance (BBC) and the Trace-Based
Conformance (TBC) relations we have defined. The two relations are inspired by
well-established behavioural equivalences [Mil89], largely used in the
literature and revised to deal with characteristics.

Before providing the formal definition of BBC, we introduce the necessary
notation. $\mathbb{C}h$ and $\mathbb{C}$ represents the sets of all
choreography and collaboration configurations, respectively. Moreover, weak
transitions are defined as follows: $\xRightarrow{}$ denotes the reflexive and
transitive closure of $\xrightarrow[]{\tau}$, i.e. zero or more
$\tau$-transitions; $\xRightarrow{l}$ denotes
$\xRightarrow{}\xrightarrow[]{l}\xRightarrow{}$. We exploit functions
$labels(C)$ and $labels(Ch)$ returning the sets of all communication labels
that can be potentially generated by the collaboration $C$ and the
choreography $Ch$, respectively. These functions are inductively defined on
the syntax of collaboration and choreography structures in a straightforward
way. For example, in case of choreographies we have the definition case
$labels({\sf task}({\sf e}_{i},{\sf e}_{o},{\sf p}_{1},{\sf p}_{2},{\sf
m}))=\\{{\sf p}_{1}\rightarrow{\sf p}_{2}:{\sf m}\\}$, meaning that if a
choreography contains a task element, then its label set contains the label
corresponding the message exchange described by the task.

At the collaboration level the definition of conformance requires the use of
the hiding operator $C/L$, defined by the rules in Fig. 10. This operator, as
usual, transforms into $\tau$ all the actions in the set $L$, in order to
consider them as internal actions in the conformance relation.

$\begin{array}[]{|@{\ \ }r@{\ }|}\hline\cr\\\\[-8.5359pt] {tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
6.61111pt\hbox{$\displaystyle\penalty 1\langle
C,\sigma,\delta\rangle\xrightarrow[]{\textit{l}}\langle\sigma^{\prime},\delta^{\prime}\rangle$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.19997pt,depth=0.19997pt,width=69.78557pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\raisebox{-2.84544pt}{$\langle
C/L,\sigma,\delta\rangle\xrightarrow[]{\textit{l}}\langle\sigma^{\prime},\delta^{\prime}\rangle$}$}}}}\
\;\textit{l}\notin L\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 7.24863pt\hbox{$\displaystyle\penalty 1\langle
C,\sigma,\delta\rangle\xrightarrow[]{\textit{l}}\langle\sigma^{\prime},\delta^{\prime}\rangle$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.19997pt,depth=0.19997pt,width=71.0606pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\raisebox{-2.84544pt}{$\langle
C/L,\sigma,\delta\rangle\xrightarrow[]{\tau}\langle\sigma^{\prime},\delta^{\prime}\rangle$}$}}}}\
\;\textit{l}\in L\par\\\\[17.07182pt] \hline\cr\end{array}$ Figure 10. Hiding
Operator.

[BBC Relation] A relation $\mathcal{R}\subseteq(\mathbb{C}h\times\mathbb{C})$
is a weak Bisimulation Conformance if, for any $\langle
Ch,\sigma_{ch}\rangle\in\mathbb{C}h$ and $\langle
C,\sigma_{c},\delta\rangle\in\mathbb{C}$ such that $\langle
Ch,\sigma_{ch}\rangle\ \mathcal{R}\ \langle C,\sigma_{c},\delta\rangle$, it
holds:

  * •

for all ${\sf p}_{1},{\sf p}_{2},m$ and $\sigma_{ch}^{\prime}$, if $\langle
Ch,\sigma_{ch}\rangle$ $\xrightarrow[]{{\sf p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}\sigma_{ch}^{\prime}$
then $\langle C,\sigma_{c},\delta\rangle$ $\xRightarrow{{\sf
p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}\langle\sigma_{c}^{\prime},\delta^{\prime}\rangle$ for some
$\sigma_{c}^{\prime},\delta^{\prime}$ s.t. $\langle
Ch,\sigma_{ch}^{\prime}\rangle\ \mathcal{R}\ \langle
C,\sigma_{c}^{\prime},\delta^{\prime}\rangle$;

  * •

for all ${\sf p}_{1},{\sf p}_{2},m,\sigma_{c}^{\prime}$ and $\delta^{\prime}$,
if $\langle C,\sigma_{c},\delta\rangle$ $\xrightarrow[]{{\sf
p}_{1}\rightarrow{\sf p}_{2}:{\sf
m}}\langle\sigma_{c}^{\prime},\delta^{\prime}\rangle$
then $\langle Ch,\sigma_{ch}\rangle$ $\xRightarrow{{\sf p}_{1}\rightarrow{\sf
p}_{2}:{\sf m}}\sigma_{ch}^{\prime}$ for some $\sigma_{ch}^{\prime}$ s.t.
$\langle Ch,\sigma_{ch}^{\prime}\rangle\ \mathcal{R}\ \langle
C,\sigma_{c}^{\prime},\delta^{\prime}\rangle$;

  * •

for all $\sigma_{ch}^{\prime}$, if $\langle Ch,\sigma_{ch}\rangle$
$\xrightarrow[]{\ \tau\ }\sigma_{ch}^{\prime}$
then $\langle C,\sigma_{c},\delta\rangle$ $\xRightarrow{\quad\
}\langle\sigma_{c}^{\prime},\delta^{\prime}\rangle$ for some
$\sigma_{c}^{\prime},\delta^{\prime}$ s.t. $\langle
Ch,\sigma_{ch}^{\prime}\rangle\ \mathcal{R}\ \langle
C,\sigma_{c}^{\prime},\delta^{\prime}\rangle$;

  * •

for all $\sigma_{c}^{\prime}$ and $\delta^{\prime}$, if $\langle
C,\sigma_{c},\delta\rangle$ $\xrightarrow[]{\ \tau\
}\langle\sigma_{c}^{\prime},\delta^{\prime}\rangle$
then $\langle Ch,\sigma_{ch}\rangle$ $\xRightarrow{\quad\
}\sigma_{ch}^{\prime}$ for some $\sigma_{ch}^{\prime}$ s.t. $\langle
Ch,\sigma_{ch}^{\prime}\rangle\ \mathcal{R}\ \langle
C,\sigma_{c}^{\prime},\delta^{\prime}\rangle$.

A choreography $\langle Ch,\sigma_{ch}\rangle$ and a collaboration $\langle
C,\sigma_{c},\delta\rangle$ _conform_ if there exists a weak Bisimulation
Conformance relation $\mathcal{R}$ such that
$\langle Ch,\sigma_{ch}\rangle\ \mathcal{R}\ \langle
C/(labels(C)\\!\setminus\\!labels(Ch)),\sigma_{c},\delta\rangle$. The proposed
BBC relation considers to conform collaborations that are able to simulate
step by step choreographies, and vice versa. In particular, if the
choreography performs a message exchange, in the collaboration we expect to
observe the reception of the message, possibly preceded or followed by any
number of internal actions, and then the two continuations have to be in
relation. Analogously, if we observe a message reception in the collaboration,
the choreography has to reply with the corresponding weak transition.
Moreover, if one of the two models performs an internal action, the
counterpart can react with a weak transition $\xRightarrow{}$. The definition
of conformance is quite close to a standard bisimulation relation, except for
the use of the hiding operator at the collaboration level. Specifically, the
hiding is used to ignore all additional behaviors in the collaboration that
are not explicitly expressed, and hence regulated, in the choreography. In
this way, even if a collaboration performs some additional communications, if
it is able to (bi)simulate with the given choreography, they do conform. The
different communication models defined in the semantics of choreographies and
collaborations significantly affects the conformance checking. We thoroughly
discuss the motivations underlying our choice of comparing the execution of
tasks in the choreography with message receptions in the collaboration in
Section 6, when all involved technicalities have been introduced and practical
examples of the application of our conformance checking notion have been
shown.  Notably, as discussed in Section 3, our approach is hybrid and its
goal is to encourage the reuse of existing process models as much as possible.
For this reason we have based our conformance checking on weak bismulation
rather than a stronger notion of weak equivalence, as e.g. branching
bisimulation. Indeed, we do not aim at ensuring a strong conformance between
models, but we just focus on the correct exchange of messages abstracting from
internal actions. Hence, for our purposes, a stronger relation would act in a
too discriminatory way.

BBC guarantees that the collaboration takes decisions, concerning the
execution flow, exactly as what is specified in the choreography. Sometimes
this condition may be too restrictive and the system designer would prefer to
adopt a weaker relation (examples of these situations are described in the
following subsection). To this aim, in our work we also introduce the more
relaxed TBC relation. Intuitively, in this case two models conform if and only
if they can perform exactly the same weak sequences of actions. In the
definition below, we deem a label to be _visible_ if it is of the form ${\sf
p}_{1}\rightarrow{\sf p}_{2}:{\sf m}$. Notationally, the transition $\langle
Ch,\sigma\rangle$ $\xRightarrow{s\ }\sigma^{\prime}$, where $s$ is a sequence
of visible labels $l_{1}l_{2}\ldots l_{n}$, denotes the sequence $\langle
Ch,\sigma\rangle$ $\xRightarrow{l_{1}\ }$ $\langle Ch,\sigma_{1}\rangle$
$\xRightarrow{l_{2}\ }$ $\langle Ch,\sigma_{2}\rangle$ …$\xRightarrow{l_{n}\
}$ $\langle Ch,\sigma^{\prime}\rangle$ of weak transitions. Transition
$\langle C,\sigma,\delta\rangle$ $\xRightarrow{s\
}\langle\sigma^{\prime},\delta^{\prime}\rangle$ is similarly defined.

[TBC Relation.] A choreography $\langle Ch,\sigma_{ch}\rangle$ and a
collaboration $\langle C,\sigma_{c},\delta\rangle$ _trace conform_ if, given
$C^{\prime}=C/(labels(C)\\!\setminus\\!labels(Ch))$, for any sequence $s$ of
visible labels it holds:

  * •

$\langle Ch,\sigma_{ch}\rangle$ $\xRightarrow{s\ }\sigma_{ch}^{\prime}$
implies $\langle C^{\prime},\sigma_{c},\delta\rangle$ $\xRightarrow{s\
}\langle\sigma_{c}^{\prime},\delta^{\prime}\rangle$ for some
$\sigma_{c}^{\prime}$ and $\delta^{\prime}$;

  * •

$\langle C^{\prime},\sigma_{c},\delta\rangle$ $\xRightarrow{s\
}\langle\sigma_{c}^{\prime},\delta^{\prime}\rangle$ implies $\langle
Ch,\sigma_{ch}\rangle$ $\xRightarrow{s\ }\sigma_{ch}^{\prime}$ for some
$\sigma_{ch}^{\prime}$.

The TBC relation guarantees that the collaboration is able to produce the same
sequences of messages of the choreography, and vice versa, without controlling
presence of deadlock states and distinguishing different decision points and
non-determinism forms. Concerning this latter point, BBC can recognize
dominated non-determinism, where a participant (non-deterministically) takes a
decision using a XOR gateway and the other behaves accordingly, from non-
dominated non-determinism, based on a race condition among the messages
managed by an event-based gateway. As it usually happens for these classes of
behavioural relations, models that conform according to BBC also conform
according to TBC.

#### Conformance at work.

Cases | Bank | Customer | Booking System | Well-composed | TBC | BBC
---|---|---|---|---|---|---
1 | a | b | d | yes | false | false
2 | a | b | e | no | — | —
3 | a | b | f | no | — | —
4 | a | c | d | no | — | —
5 | a | c | e | yes | true | true
6 | a | c | f | yes | true | false
Table 1. Possible Processes Combination

To demonstrate in practice the characteristics of the conformance relations,
focusing on the management of non-determinism and asynchronous messages, we
test them considering the various process model presented in Fig. 4, where
three participants are involved.

Combining the processes reported in Fig. 4 we have six different possibilities
to enable the choreography, according to different selections of the processes
for the customer and the booking system roles. As shown in Table 1, these
combinations will lead to different results with respect to the actual
capability to enact the choreography. In particular, both syntactically and
semantically related issues can emerge.

The combinations of processes in cases 2, 3 and 4 violate the notion of well-
composedness. In cases 2 and 3 the Booking system $e$ and $f$ contain an extra
ack message not correctly managed by Customer 1. Case 4 instead is in the
opposite situation, where Customer 2 is expecting an ack message not correctly
managed by Booking System 1. Cases 1, 5 and 6 are different, as the processes
once combined satisfy the notion of well-composedness given in the Definition
8, which guarantees the correct matching of all messages between the
processes. However, when compared to the choreography, just one of these cases
satisfies the BBC, while the other two satisfy only the TBC conformance
notion.

The conformance checking results reported in the table show in detail the
differences between BBC and TBC. The designer can select the more appropriate
relation that fits more his needs, taking into account that BBC provides more
guarantees on the correct behaviour between the two models, while TBC ensures
only that both models produce the same sequences of messages.

The proposed methodological approach, described in Section 3, drove our
choices for the behavioural equivalences to use for conformance checking.
Indeed, in a hybrid context, the reuse and the integration of existing
processes, or their replacement without altering the global behaviour of the
system, are the key factors for a collaborative environment that needs to
satisfy an established specification. In such a situation, the use of the
bisimulation equivalence can guarantee the faithful correspondence of the
emerging behaviour of the composed collaboration with respect to the
choreography specification. However, such equivalence sometimes could be too
restrictive, since the collaboration is not always able to replicate the
choreography specification. At this point, the TBC equivalence plays a
fundamental role in discriminating on the possibility to use the
collaboration, possibly with some adjustments, or not. The TBC does not
guarantee the same stringent behavioural properties of the BBC (e.g., absence
of deadlocks), but still it can distinguish two models according to their
admitted sequences of actions. So, the modeler is conscious that the violation
of the BBC establishes in general the incompatibility between the achieved
collaboration and the high-level behaviour prescribed by the choreography.
Anyway, having the TBC satisfied leaves some possibilities that the
collaboration, after a refactoring process, can satisfy the given
choreography.

An evident example of this situation is depicted in Table 1 at case 6, where
the resulting composition of processes _a_ -_c_ -_f_ is TBC but not BBC. The
three processes can expose the same sequences of actions defined by the
specification, but a deadlock can emerge. In fact, the customer and the
booking system processes can make different choices in their exclusive
gateways and, hence, the booking system will be blocked waiting for a message
forever, consequently invalidating the BBC. Unfortunately, the violation of
the BBC indicates that, as it is, the collaboration is not conformant with the
choreography specification. However, the satisfaction of the TBC  suggests
that the process behaviours in the collaboration model could still be fixed
with a refactoring process. As mentioned in Section 3, this is the case in
which it can be possible to solve the issue adapting the behaviour of process
_f_ , so that it will not take an internal choice different from that taken by
c. In such a case we could introduce an adapter that shields the process _f_
and, at the right time, it uses an event-based gateway to wait for the message
from _c_ indicating whether the customer intends to accept or cancel the
itinerary proposal. Then, the adapter will interact with process _f_ using
local and/or lower level mechanisms (e.g., by setting the value of a data
object exploited in the conditions added to the exclusive gateway, or, at mere
implementation level, by invoking a method to provide the information about
the customer decision), so to drive the booking system process towards the
right path in the exclusive gateway. Notably, in this way the structure of _f_
remains unchanged.

There are situations in which a collaboration that only satisfies TBC can
easily be transformed in order to satisfy BBC by just refining the conditions
on gateways, and without making any additional assumption on the knowledge
needed by the involved processes so to take the corresponding paths. Fig. 11
depicts a model regulating the shopping of alcohol between a Customer and a
Bar. The process starts with the selection by the customer of a type of drink;
if it is alcoholic the bar needs further information about the age of the
customer before serving the drink. Vice versa, no check is requested in case
of nonalcoholic drinks. Checking this choreography with the corresponding
collaboration depicted in Fig. 12, we have that only the TBC equivalence
holds. This result suggests that the collaboration is not respecting the
behaviour specified in the choreography, since the exclusive gateways in the
customer and bar processes without any condition could lead to choices that
violate the behaviour specification, allowing e.g. the customer to skip the
age check. With a deeper examination, and a successive refinement consisting
in the inclusion of expressions in the gateways, it is possible to improve the
model in order to fix the issue and consequently satisfy the BBC equivalence.

Figure 11. Alcohol Shopping Choreography. Figure 12. Alcohol Shopping
Collaboration. Figure 13. Alcohol Shopping Collaboration Refinement.

The result of the refinement is reported in Fig. 13, which shows the same
processes of Fig. 12 but enriched with expressions based on shared information
messages, i.e. _Type_ and _Age_. The introduction of such expressions reduces
the possible behaviours of the collaboration model, thus avoiding those
situations leading to executions that deviate from the ones prescribed by the
choreography. It is worth mentioning that the case of processes _a_ -_c_ -_f_
cannot be reasonably solved using the same solution, at least from a pragmatic
point of view. Indeed, in such a case an additional communication would have
been needed to share, before the two exclusive gateways, the decision of the
customer. But, clearly, this would have been absolutely artificial, resulting
in a collaboration where the customer has to send twice the same information.

##  5\. From Theory to Practice: _C_ ${}^{\ \\!\\!4}$ tool

The $C^{4}$ formal framework presented so far it has been implemented as a
web-based toolchain222The tool is available on-line at the following link
_http://pros.unicam.it/c4/_ that permits to cover the entire choreography life
process reported in Section 3. The tool supports system designers in modelling
diagrams, and in the verification of conformance between a set of modelled
processes composed to form a collaboration and a prescribed choreography. A
distinctive aspect of the tool is its ability to hide the underlining formal
technicalities, so to be usable also to those designers and software engineers
that,  even though they should clearly have high-level modeling and analysis
skills, are not so much familiar with formalisms and verification techniques
details.

Figure 14. $C^{4}$ Supporting Tool.

It is worth noticing that $C^{4}$ has multiple users that, according to their
role, are involved in different moments of the process. These are modellers,
possibly belonging to a super partes organisation, that are in charge of
producing choreography diagrams, which in a given application context act as
blueprints. Again, the $C^{4}$ users are modellers when they represent the
(process) behaviours that organisations can bring within compositions.
Moreover, the users are system integrators when they compose, in automatic
way, the process models provided by the participating organisations in order
to create collaboration diagrams, which then are automatically compared
against choreography diagrams.

Fig. 14 depicts the internal components of the $C^{4}$ tool, and its
interfaces with the user. Specifically, $C^{4}$ is able to manage
choreography, collaboration and process models in the _.bpmn_ format. These
input models can be generated by a system designer using the Camunda modeller,
which has been fully integrated in the $C^{4}$ platform (Fig. 15(a)), or other
external modelling environments. Indeed, the $C^{4}$ platform is compatible
with the most common modelling environments, such as Eclipse Modelling,
Camunda and Signavio. Once the user has selected the models to consider, it is
possible to further manipulate them. In particular the $C^{4}$ framework
permits to compose processes according to the approach formalised in
Definition 8. The result of such an activity will be a new collaboration
diagram containing the selected processes that are connected through messages
matched with respect to their names and flow directions.

Generated collaborations can be then checked with respect to selected
choreography diagrams. The access to such a functionality is provided via a
dedicated GUI (Fig. 15(b)). Here the user can select both the choreography and
the collaboration models that have to be compared. Designed models are saved
by the editor on a remote folder based repository, and can then be loaded by
the user selecting them through the dedicated GUI.

(a) Models Selection.

(b) Conformance Checker.

Figure 15. $C^{4}$ Graphical User Interface.

At this point, clicking on the submit button, the $C^{4}$ tool parses the
models and generates the corresponding LTS graphs for both the choreography
and the collaboration models. The parsing of the input files is based on the
Camunda APIs, while the LTSs are generated by means of a Java implementation
of the direct semantics defined in Section 4.

Once the LTSs are generated, $C^{4}$ saves the results in two _.aut_ files
[FGK+96]. It is now possible to run the conformance checker with respect to a
conformance relation that has to be selected by the user through a drop-down
list. The conformance checking is implemented using mCRL2 [GM14], which has
been 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 consists in a boolean message that reports the value
true in case the collaboration conforms the choreography with respect to the
selected conformance relation, or false in case the conformance does not hold.
In the latter case, the corresponding counterexample is returned. Notably, the
$C^{4}$ conformance checker (Fig. 15(b)) allows to have a preview of the LTS
graph or download it in the _.aut_ format. This enables the possibility to run
the verification using other model checkers. The tool is also available as a
stand-alone solution, only with respect to the model checking functionality.

_$C^{4}$ tool at work on the booking example._ In order to show the usage of
the proposed approach, here we focus on the checking of the well-composed
collaborations depicted in Table 1. The objective is to check if the generated
collaborations are valid implementations of the choreography in Fig. 2.a,
considering both the BBC and TBC relations.

Analysing the first case in Table 1 we realise that by combining the processes
_a_ -_b_ -_d_ reported in Fig 4 we obtain the collaboration in Fig. 2.b. Now
checking the collaboration in Fig. 2.b with respect to the choreography in
Fig. 2.a we obtain in return the violations for both conformance relations.
More specifically, considering TBC the following counterexample is reported:

c$\xrightarrow[]{}$bs: login, c$\xrightarrow[]{}$bs: request,
bs$\xrightarrow[]{}$c: reply, c$\xrightarrow[]{}$bk: pay

where $c$, $bs$ and $bk$ stand for the customer, booking system and bank
participant names, respectively. This trace is allowed by the collaboration
model and not by the choreography model. It shows that the reasonable
behaviour ‘book and then pay’ is not respected in the collaboration, which
indeed permits to pay a reservation before booking it. This undesired
behaviour is due to the non-blocking nature of the collaboration sending task,
which permits to the customer to send the payment immediately after the
booking request, without waiting for any acknowledgement from the booking
system. This would not be a problem in case of a collaboration with only two
participants, or more generally when the receiver of the two messages is the
same. In this case the order in which the messages will be processed is
managed by the behaviour of the receiver. Instead, in our running scenario the
_book_ and the _pay_ messages are received by two different participants.
Notably, using an adapter that shields process _b_ adding the capability of
waiting for the _ack_ message we could solve the issue. However, this is
clearly an artificial situation and in the general case not satisfying TBC is
an indication that the development of an adapter is probably a rather complex
and expensive activity.

Figure 16. Booking Collaboration conformant to the Choreography.

The problem, instead, does not manifest in the composition in case 5 of Table
1. The resulting collaboration is shown in Fig. 16. In this example an $ack$
message between the $book$ and $pay$ messages has been included. This
guarantees that the booking phase completes before giving to the customer the
possibility to proceed with the payment. In fact, by checking the conformance
between this collaboration and the choreography in Fig 2.a, the $C^{4}$ tool
states that the collaboration is a correct implementation of the choreography,
as the two models conform according to both TBC and BBC. Notably, the added
message is not foreseen by the choreography specification, nonetheless it
permits to further constrain the collaboration so to obtain a behaviour
satisfying both conformance relations. In such a case, before the conformance
checking, the hiding operator (used in the definition of our conformance
relations) will replace the $ack$ message by a $\tau$ action in the
composition of the various participants in the collaboration.

The last well-composed collaboration is represented by case 6 of Table 1. This
case differs from the previous case 5 just for the gateway in the booking
system process. The resulting collaboration is not conformant to the
choreography according to the BBC relation. The produced counterexample
permits to detect a deadlock related to the presence of two external choices.
Notice that the collaboration satisfies instead the TBC relation, since the
produced traces are the ones expected in the choreography specification, and
as shown in Section 4 the usage of an adapter can be in this case a viable
solution to satisfy the BBC relation.

##  6\. Discussion

In the previous sections we have shown how the different communication models
of choreography and collaboration models affect the definition of our
conformance checking, and the effects of its application to practical
examples.

According to the BPMN standard, collaborations rely on an asynchronous
communication model, as it typically happens in distributed systems. In such
an asynchronous model of communication, to compare the behaviour of two
systems, as observable are usually considered only the output capabilities of
the systems, i.e. the sending actions. The intuition is that an ‘asynchronous
observer’ cannot directly observe the receipt of data that has been sent. This
notion of observable action has led to the definition of asynchronous variants
of behavioural equivalences (as, e.g., in the labeled bisimulation introduced
for the asynchronous $\pi$-calculus [ACS98]).

In this work, however, we are interested in comparing the behaviour of a
collaboration model with that of a BPMN choreography model (not another BPMN
collaboration). As explained at the beginning of this section, we consider the
semantics of choreography diagrams as given in the BPMN standard. Therefore,
our comparison between choreography and collaboration models is driven by the
specificities of BPMN and in particular, for what concern the communication
model, by the fact that choreography tasks require synchronous communication.
Specifically, the standard states that a choreography task completes when the
receiver participant reads the message [OMG11, p. 315]. Therefore, in our
approach the effective completion of the message exchange in the choreography
is compared with the reception of the corresponding message in the
collaboration. This permits ensuring that the order of receives in the
collaboration execution respects the order of message receptions prescribed by
the choreography model, as requested by the BPMN standard. This would not be
possible by only observing sending actions. For example, let us consider the
choreography model in Fig. 17, where the participant $\mathsf{A}$ sends in
sequence two messages, $\mathsf{m1}$ and $\mathsf{m2}$, to the participant
$\mathsf{B}$. If we compare this model with the collaborations in Fig. 18
considering only send actions, the conformance checking is always successful,
because the participant $\mathsf{A}$ sends message $\mathsf{m2}$ after
$\mathsf{m1}$ in all four cases. However, in case (b) the messages are always
received in the opposite order (hence, the collaboration execution corresponds
to first completing the message exchange of $\mathsf{task2}$ before completing
that of $\mathsf{task1}$), in case (c) one of the two messages is never
received, and in case (d) the reception order may be correct or not depending
on the interleaving of the $\mathsf{B}$’s tasks. Therefore, all these three
latter cases lead to a conformance result undesirable according to the
requirements of the BPMN standard. Instead, our conformance checking approach
identifies these three collaborations as not conformant with the choreography.

The focus on the BPMN notation and its specificities, in particular those
requiring to observe the reception of messages, is a distinctive aspect of our
work. Indeed, related works either do not consider different communication
models for choreography and collaboration specifications, or focus on
choreography languages different from BPMN 2.0 choreography diagrams. For
example, [BB11] abstracts from a specific choreography specification language,
and considers as choreography specifications finite state machines, LTL
formulae or CTL formulae, without any reference to the peculiarities of the
BPMN choreography semantics.

Figure 17. Simple example of choreography. |
---|---
(a) | (b)
|
(c) | (d)
Figure 18. Four examples of collaborations.

It is worth noticing that we only observe receiving actions in collaboration
diagrams, rather than both sends and receives. The motivation of this design
choice is twofold. On the one hand, we are driven by a pragmatic approach:
observing both kinds of actions will lead to a definition of conformance
checking too discriminating for practical use. To explain this point, let us
consider again the choreography model in Fig. 17, and compare it with the
collaboration (a) in Fig. 18. Observing both sending and receiving actions,
the conformance checking would fail, because we can have a collaboration
execution where both $\mathsf{A}$’s sends are executed before the receptions
of the two messages by $\mathsf{B}$, while in this setting the sending of
$\mathsf{m2}$ should take place after the reception of $\mathsf{m1}$. However,
since there is no correlation between the sending of $\mathsf{m2}$ and the
reception of $\mathsf{m1}$, we believe that this interpretation of conformance
checking turns out to be too restrictive. Indeed, to fix the issue we would
add an extra-choreography message from $\mathsf{B}$ to $\mathsf{A}$ in order
to acknowledge that $\mathsf{m1}$ has been received. Our notion of conformance
checking permits avoiding to introduce such, unnecessary, ack message. The
other motivation concerning the observation of only receiving actions is more
technical and, again, strictly connected to the peculiarities of the BPMN
standard. Indeed, differently from most choreography languages, and in
particular the formal ones, BPMN supports a wide variety of workflow
operators, some of which can complicate the formal treatment. This is, for
instance, the case of the event-based gateway (see, e.g., [CMRT19]). If one
would like to observe the sending actions, many collaborations that are
faithful to a given choreography involving an event-based gateway would be
discarded by the conformance checking. Let us consider for example the
choreography in Fig. 19(a), which represents a typical use of the event-based
gateway: the participant $\mathsf{A}$ sends in parallel a message to
$\mathsf{B}$ and another to $\mathsf{C}$, and then waits for one answer, the
first message reception disables the reception of the other one. The
collaboration reported in Fig. 19(b) represents a typical, and natural,
implementation of this behaviour, where the particpant $\mathsf{A}$ exploits
the event-based gateway. However, by observing the send actions, these two
models are not conformant, because at collaboration level there will be always
one message between $\mathsf{m3}$ and $\mathsf{m4}$ that will not be read by
$\mathsf{A}$, and this message cannot be matched by any task execution at
choreography level. Instead, our conformance checking approach properly
recognizes these models as conformant.

|
---|---
(a) | (b)
Figure 19. Choreography and collaboration models involving the event-based
gateway.

On the other hand, the interplay between the observation of only receives and
the presence of additional interactions in the collaboration that are not
explicitly expressed in the choreography may lead to subtle behaviours. We
clarify this point with the example in Fig. 20, modelling a common request-
response scenario. The choreography (a) is clearly conformant with the
collaboration (b), which is the expected implementation of this simple
behaviour, and not conformant with (c), because the response message
$\mathsf{m2}$ can be read before the request message $\mathsf{m1}$. However,
the conformance is also satisfied for the collaboration (d): in fact, despite
$\mathsf{m2}$ can be sent before $\mathsf{m1}$, the additional exchange of
message $\mathsf{m}$ imposes the correct order of execution of the receives.
This behaviour can be considered acceptable when the message sent by
$\mathsf{B}$ is not correlated to that of $\mathsf{A}$, but it may be
undesirable when $\mathsf{m2}$ has to be considered as a response to the
request $\mathsf{m1}$. Thus, this is an application-dependent aspect that, to
be possibly investigated, requires to consider the correlation between the
content of the exchanged messages (e.g., in the example we should check that
part of the payload of $\mathsf{m2}$ results from the evaluation of the
information included in $\mathsf{m1}$).

|
---|---
(a) | (b)
|
(c) | (d)
Figure 20. Interplay between receive-only checking and interactions extra
choreography.

##  7\. Related Works

This section discusses the advantages and differences in our approach with
respect to alternative proposals. The discussion is organized over different
paragraphs; each one devoted to a specific aspect considered relevant for
$C^{4}$.

_On the Choice of the Modelling Notation_. Researchers have worked in the
definition and the study of modelling notations for the representation of
collaborative systems for many years now. In particular, the topic has
received much attention in the field of service-oriented applications, where
many modelling languages have been proposed. Among the first proposals, we can
certainly mention the OASIS standard WS-BPEL [OAS07], for the specification of
collaborations referred as “abstract orchestrations”, and the W3C standard WS-
CDL [KBR04], for the representation of choreographies. These specifications
have inspired the OMG standard [OMG11] that has inherited many concepts from
theme. In the literature, many proposals are available for conformance
relations among models defined in different notations [PTDL07, BBM+05, LMX07,
EKdMSvdA08, RFG10, Mar03]. However, the lack of a solid framework for the
conformance verification related to the BPMN standard has motivated our
effort.

_From Choreographies to Code_. In the development of collaborative systems,
much effort has been devoted to the study of model transformation approaches
in particular in the line of model-driven engineering strategies. In
particular, choreographies specifications have been fruitfully used in the
generation of component stubs/skeletons embedding constraints of the message
flow. In [HH08b], the authors propose a top-down approach, where, starting
from a choreography they derive a UML profile respecting the global
specification with the final aims to derive WS-BPEL processes. In [NWM17] the
authors provide a semi-automatic RESTful implementation of choreographies
interactions. Nevertheless the above approaches do not provide any formal
guarantee to ensure that the resulting system conforms to the interactions
prescribed by the specification. Another line of research works, focussing on
session types and behavioural contracts [HLV+16], provides formal guarantees
that permit to achieve a correct-by-construction top-down approach. However,
the formalisms used in these works for the global specification of
choreographies are much less rich than the BPMN notation (e.g., they do not
support arbitrary topology, such gateways as the event-based and parallel
ones, different communication models for collaborations and choreography,
etc.), hence their practical application is far from that enabled by the BPMN
standard. Furthermore, a top-down approach in a real context is not always the
best choice, since organisations have already their processes regulating their
activities. For this reason, we propose a hybrid methodology that incentives
the reuse and integration of already existing processes, providing a complete
framework able to deal directly with BPMN models and with the capability of
providing formal evidence of their conformance.

_Conformance_. In the literature, conformance is referred with different
terminologies depending on the context in which it is used. Possible
synonymous are compliance or compatibility, but generally, they are never
explicitly defined on the standard. Different works [GMS06, MM03, SLM+10,
ADW08, KRFRM13, LRMGD12, KR12, KRM+12] define notion of compliance between
processes or collaborations exploiting domain-specific regulations and rules.
In general, these works express behavioural constraints using some form of
temporal logics, rather than using equivalences among models. The usage of
additional languages requires the system designer to study further
technicalities in order to exploit the proposed checking technique.
Alternative approaches base the analysis only considering local views [WDW12,
HDvdA+05, DDGB09]. Somehow this is a simplification of the problem that does
not guarantee the conformance for the composition.

Our work differs from the ones mentioned above since it relies on models, at
both global and local level, and propose a conformance check between different
layers of specification abstraction without requiring any formal knowledge to
the system designer. Our conformance checking is based on LTSs, since our
methodology aims at reusing standard bisimulation and trace equivalences
supported by existing equivalence checkers. Thus, the novelty of our proposal
is not in the equivalence checking between LTSs, per se, but it is in how
these LTSs are produced starting from standard BPMN models. The passage from
BPMN models and LTSs is indeed defined by our operational semantics, which
takes into account the peculiarities of BPMN that instead are overlooked by
other works (see Section 6). Furthermore, all the specific characteristics of
our conformance relations (e.g., the use of hiding) have been already taken
into account during the LTS generation. This relieves us of the duty of
developing an ad-hoc conformance checker.

_Direct Semantics._ Many attempts trying to give a semantics to the notation
are present in the literature. The majority of these approaches provide
semantics in terms of translation to other formalization languages such as
Petri-nets or similar formalisms. Providing semantics by translation can
generate divergences with the expected behaviour of the elements. Between the
target specification languages, we found process algebras [BGG+06, SB09,
SBS06], formal languages [NPZ12, PS12, MS13, GPSY16], transition-based models
(e.g., Petri-Nets) [DDO08, BB11, BFF09, CPR15], or session types [CDP11].
Although all these formalisms have been used to formalise the BPMN semantics,
there is a general lack of support related to the communication model. The
main issues are related to the difficulty to distinguish messages from control
flow in the formalisation, and to deal with both synchronous and asynchronous
communication at the same time. Therefore, studying these aspects directly on
BPMN does not leave any room for ambiguity, and increases the potential for
formal reasoning on BPMN. In $C^{4}$ we rely on a direct semantics for both
collaboration and choreography models. The $C^{4}$ semantics is given in terms
of features and constructs of , rather than in terms of their low-level
encoding into another formalism that is equipped with its own syntax and
semantics. This permits to avoid any possible bias that would result from the
encoding in another formalism. The direct semantics proposed in this paper is
inspired by [CPRT15], and by its extended version in [CFP+18]. Differences
mainly refer to configuration states that are here defined according to a
global perspective. Moreover, the formalisation now includes choreography
diagrams, which were overlooked in the previous semantics definition.

_Conformance vs Communication models._ The definition of semantics using other
languages can bring to underspecified situations that can alter the
conformance checking results. For this reason, we use a direct approach that
permits to focus on specific features of that would be ignored by using
available Petri Nets-based semantics. Evidence of this divergence can be
noticed in the definition of gateways. Following the mapping to Petri Nets
proposed in [DDO08], it is not possible to distinguish different types of non-
determinism resulting from event-based or exclusive gateways [CMRT19]. Indeed
these two elements have different effects: the event-based gateway produces
non-dominated non-determinism (roughly, no one in the model has complete
knowledge on the decision that will be taken), while the exclusive gateway
produces dominated non-determinism (roughly, the decision is taken by one
party and followed by the others). Differently from the translation-based
approaches, our approach permits to distinguish the dominated and non-
dominated non-determinism produced by the gateways, as prescribed by the
standard. This is somehow similar to [BGG+06, QZCY07], which rely on the
concept of internal and external choices defined in the CSP process algebra.
Notably, the different kinds of non-determinism have an impact on the
conformance relations, as detailed in Table 1.

Another fundamental aspect for the definition of the conformance is the
asynchronous communication of collaborations versus the synchronous one of the
choreographies. In the literature, to deal with asynchronous communication,
either additional constructs are used, such as buffers [PS12] or dedicate
language structures [SB09, GPSY16], or simply reducing the asynchronous
communication model to the synchronous one. The notions of conformances that
we propose in $C^{4}$ allows the user to compare models assuming different
communication strategies without making any assumption on the different
management of the messages. Our conformance notion directly manages this
aspect, as widely discussed in Section 6.

_Tool Support._ Verchor [GPSY16] is a tool similar to $C^{4}$. In this case,
the main objective is to use the conformance notion to check the realizability
of a set of peers obtained from a projection of a given choreography. Another
tool, more focused on business properties, is VBPMN [KPS17]. Here the
verification makes use of the well-known model checker CADP. While VBPMN can
deal only with the analysis of single processes, $C^{4}$ is able to manage the
conformance checking of collaborations w.r.t. choreographies. In $C^{4}$ the
presence of an integrated system for the storing, design and verification of
BPMN models allows non-domain experts to check the conformance of their models
without any previous notion of the formal definitions.

##  8\. Conclusions and Future Work

This paper considers the theoretical and practical relevance of checking the
conformance of models related to the global specification of application-level
protocols (choreographies) and their possible implementation through the
composition of processes (collaborations). The specific context is that of the
standard, which nowadays is the most used notation for specifying inter-
organisational processes. To perform such conformance checking, the paper
proposes a direct semantics in the structural operational style, and defines
two different equivalence relations between choreographies and process
collaborations. The resulting formal framework has also been practically
implemented in the $C^{4}$ toolchain, which permits to support all phases
needed to derive inter-organisational process-based systems. The tool is
available as a web-based service, as well as a standalone application.

In the next future, we intend to extend the framework further, so to possibly
check temporal properties on choreographies and collaborations.  Another
extension of the framework we intend to investigate concerns the treatment of
additional BPMN elements, in order to cover a more comprehensive set of
elements. Similarly, we also plan to investigate the impact of using in our
approach other notions of equivalences that are weaker than the weak
bisimulation and stronger than the weak trace equivalence (e.g. weak failure
equivalence). Moreover, concerning the repository storing the published
choreographies and the available processes, we foresee for this repository
further developments and a better integration with $C^{4}$.  Such integration
would make it also possible to run, in a structured manner, an empirical
evaluation of the proposed methodology so to complement the validity of the
approach, which up to now is mainly based on comparison with the literature.
A further interesting line of research that we intend to follow refers to the
usage of inter-organisational models to facilitate the integration of existing
services, so to make easier the development of the considered collaborative
systems.  Moreover, we intend to investigate on the relation that may exist
between the used notions of conformance and the ability to solve issues
detected in a collaboration. Indeed, as shown in the paragraph Conformance at
work in Section 4, when BBC is not satisfied, the satisfaction of TBC can
leave some possibilities to solve the issue in the collaboration in order to
achieve the BBC conformance. However, the TBC could not provide enough
guarantees to generate an adapter or define a refinement to solve the issue,
and on the other hand there could be situations in which, even if the TBC is
not satisfied, it is easy to solve the issue. Therefore, we believe that a
deeper formal investigation is necessary to precisely define the requirements
ensuring the existence of a solution for a given collaboration issue. Finally,
we aim at continuously improving the $C^{4}$ implementation, in particular in
relation to the introduction of (semi-)automatic mechanisms for the generation
of adapters starting from the counterexamples returned by the conformance
checking.

## References

  * [AAP13] Midhat Ali, Guglielmo De Angelis, and Andrea Polini.  Servicepot - an extensible registry for choreography governance.  In SOSE, pages 113–124. IEEE Computer Society, 2013.
  * [ABN+08] Aitor Aldazabal, Terry Baily, Felix Nanclares, Andrey Sadovykh, Christian Hein, and Tom Ritter.  Automated model driven development processes.  In Model Driven Tool and Process Integration, pages 361 – 375. Fraunhofer IRB Verlag, 2008.
  * [ACS98] Roberto M. Amadio, Ilaria Castellani, and Davide Sangiorgi.  On bisimulations for the asynchronous pi-calculus.  Theor. Comput. Sci., 195(2):291–324, 1998.
  * [ADW08] Ahmed Awad, Gero Decker, and Mathias Weske.  Efficient compliance checking using bpmn-q and temporal logic.  In BPM, volume 5240 of LNCS, pages 326–341. Springer, 2008.
  * [ASGPT18] Marco Autili, Amleto Di Salle, Francesco Gallo, Claudio Pompilio, and Massimo Tivoli.  On the Model-driven Synthesis of Adaptable Choreographies  2245, pages 12–17, Models Workshop, 2018.
  * [BB11] Samik Basu and Tevfik Bultan.  Choreography conformance via synchronizability.  In World wide web, pages 795–804. ACM, 2011.
  * [BBM+05] Matteo Baldoni, Cristina Baroglio, Alberto Martelli, Viviana Patti, and Claudio Schifanella.  Verifying the conformance of web services to global interaction protocols: A first step.  In Formal Techniques for Computer Systems and Business Processes, volume 3670 of LNCS, pages 257–271. Springer, 2005.
  * [BDA05] Alistair Barros, Marlon Dumas, and Arthur H.M. ter Hofstede.  Service interaction patterns.  In BPM, volume 3649 of LNCS, pages 302–318. Springer, 2005.
  * [BFF09] Tevfik Bultan, Chris Ferguson, and Xiang Fu.  A tool for choreography analysis using collaboration diagrams.  In ICWS, pages 856–863. IEEE, 2009.
  * [BGG+06] Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, and Gianluigi Zavattaro.  Choreography and orchestration conformance for system design.  In Coordination, volume 4038 of LNCS, pages 63–81. Springer, 2006.
  * [CDSW18] Josep Carmona, Boudewijn van Dongen, Andreas Solti, and Matthias Weidlich.  Conformance Checking, Springer, 2018.
  * [CDP11] Giuseppe Castagna, Mariangiola Dezani, and Luca Padovani.  On global types and multi-party sessions.  In FMOODS/FORTE, volume 6722 of LNCS, pages 1–28. Springer, 2011.
  * [CFP+18] Flavio Corradini, Fabrizio Fornari, Andrea Polini, Barbara Re, and Francesco Tiezzi.  A formal approach to modeling and verification of business process collaborations.  Science of Computer Programming, 166:35–70, 2018.
  * [CFP+19] Flavio Corradini, Fabrizio Fornari, Andrea Polini, Barbara Re, and Francesco Tiezzi.  Reprository: a repository platform for sharing business process models.  In BPM (PhD/Demos), volume 2420 of CEUR Workshop Proceedings, pages 149–153. CEUR-WS.org, 2019.
  * [CMRT19] Flavio Corradini, Andrea Morichetta, Barbara Re, and Francesco Tiezzi.  Walking through the semantics of exclusive and event-based gateways in BPMN choreographies.  In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pages 163–181, 2019.
  * [CPR15] Flavio Corradini, Andrea Polini, and Barbara Re.  Inter-organisational Business Process Verification in Public Administration.  Business Process Management Journal, 21(5), 2015.
  * [CPRT15] Flavio Corradini, Andrea Polini, Barbara Re, and Francesco Tiezzi.  An operational semantics of BPMN collaboration.  In FACS, volume 9539 of LNCS, pages 161–180. Springer, 2015\.
  * [CMPRT18] Flavio Corradini, Andrea Morichetta, Andrea Polini, Barbara Re, and Francesco Tiezzi.  Collaboration vs. Choreography Conformance in BPMN 2.0: From Theory to Practice.  In Enterprise Distributed Object Computing, pages 95 – 104, IEEE Computer Society 2018.
  * [DDGB09] Remco Dijkman, Marlon Dumas, and Luciano García-Bañuelos.  Graph matching algorithms for business process model similarity search.  In BPM, volume 5701 of LNCS, pages 48–63. Springer, 2009\.
  * [DDO08] Remco M. Dijkman, Marlon Dumas, and Chun Ouyang.  Semantics and analysis of business process models in BPMN.  Information and Software Technology, 50(12):1281–1294, 2008.
  * [EKdMSvdA08] Marwane El Kharbili, Ana Karla A de Medeiros, Sebastian Stein, and Wil MP van der Aalst.  Business process compliance checking: Current state and future challenges.  MobIS, 141:107–113, 2008.
  * [FGK+96] Jean Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescu, and Mihaela Sighireanu.  CADP a protocol validation and verification toolbox.  In CAV, volume 1102 of LNCS. Springer, 1996.
  * [GM14] Jan Friso Groote, and Mohammad Reza Mousavi.  Modeling and analysis of communicating systems.  MIT press, 2014.
  * [GMS06] Guido Governatori, Zoran Milosevic, and Shazia Sadiq.  Compliance checking between business processes and business contracts.  In EDOC, pages 221–232. IEEE, Computer Society, 2006.
  * [GPSY16] Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Lina Ye.  Verchor: a framework for the design and verification of choreographies.  IEEE Transactions on Services Computing, 9(4):647–660, 2016.
  * [HDvdA+05] Jan Hidders, Marlon Dumas, Wil MP van der Aalst, Arthur HM ter Hofstede, and Jan Verelst.  When are two workflows the same?  In Australasian symposium on theory of computing, volume 41, pages 3–11. Australian Computer Society, Inc., 2005.
  * [HH08a] B. Hofreiter, and C. Huemer.  A model-driven top-down approach to inter-organisational systems: From global choreography models to executable bpel.  In 10th IEEE Conference on E-Commerce Technology and the Fifth IEEE Conference on Enterprise Computing, E-Commerce and E-Services, pages 136–145, 2008.
  * [HH08b] Birgit Hofreiter, and Christian Huemer.  A model-driven top-down approach to inter-organisational systems: From global choreography models to executable BPEL.  In CEC/EEE, pages 136–145. IEEE, IEEE Computer Society, 2008\.
  * [HLV+16] Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro.  Foundations of Session Types and Behavioural Contracts.  ACM Comput. Surv., 49(1):3:1–3:36, 2016.
  * [HW04] Hohpe Gregor, and Woolf Bobby.  Enterprise integration patterns: Designing, building, and deploying messaging solutions  Addison-Wesley Professional, 2004.
  * [KBR04] N. Kavantzas, D. Burdett, and G. Ritzinger.  Web Services Choreography Description Language version 1.0.  Technical report, W3C, 2004.
  * [KtHB00] Bartek Kiepuszewski, Arthur H. M. ter Hofstede, and Christoph Bussler.  On Structured Workflow Modelling.  In CAiSE, volume 1789 of LNCS, pages 431–445. Springer, 2000\.
  * [KPS17] Ajay Krishna, Pascal Poizat, and Gwen Salaün.  Vbpmn: Automated verification of bpmn processes.  In iFM, pages 323–331. Springer, 2017.
  * [KR12] David Knuplesch, and Manfred Reichert.  Ensuring business process compliance along the process life cycle.  Technical report, Universität Ulm, 2012.
  * [KRFRM13] David Knuplesch, Manfred Reichert, Walid Fdhila, and Stefanie Rinderle-Ma.  On enabling compliance of cross-organisational business processes.  In BPM, volume 8094 of LNCS, pages 146–154. Springer, 2013\.
  * [KRM+12] David Knuplesch, Manfred Reichert, Jürgen Mangler, Stefanie Rinderle-Ma, and Walid Fdhila.  Towards compliance of cross-organisational processes and their changes.  In BPM, volume 132 of LNCS, pages 649–661. Springer, 2012\.
  * [LMX07] Ying Liu, Sebastian Muller, and Ke Xu.  A static compliance-checking framework for business process models.  IBM Systems Journal, 46(2):335–361, 2007.
  * [LRMGD12] Linh Thao Ly, Stefanie Rinderle-Ma, Kevin Göser, and Peter Dadam.  On enabling integrated process compliance with semantic constraints in process management systems.  Information Systems Frontiers, 14(2):195–219, 2012.
  * [Mar03] Axel Martens.  On compatibility of web services.  Petri Net Newsletter, 65(12-20):100, 2003.
  * [Mil89] R. Milner.  Communication and Concurrency, volume 84.  Prentice-Hall, Inc., 1989.
  * [MM03] Daniel J Mandell, and Sheila A McIlraith.  A bottom-up approach to automating web service discovery, customization, and semantic translation.  In WWW Workshop on E-Services and the Semantic Web, 2003.
  * [MPRWT18] Chiara Muzi, Luise Pufahl, Lorenzo Rossi, Mathias Weske, and Francesco Tiezzi.  Formalising BPMN Service Interaction Patterns.  In PoEM, volume 335 of LNBIP, pages 3–20. Springer, 2018.
  * [MSW11] Andreas Meyer, Sergey Smirnov, and Mathias Weske.  Data in business processes  Universitätsverlag Potsdam 50, 2011.
  * [MS13] Carlos Molina, and Santosh Shrivastava.  Establishing conformance between contracts and choreographies.  In CBI, pages 69–78. IEEE, 2013.
  * [MR08] Michael zur Muehlen, and Jan Recker.  How much language is enough? Theoretical and practical use of the business process modeling notation.  In Advanced Information Systems Engineering vol. 5074, Springer, LNCS, 2008, pp. 465–479.
  * [Muz19] Muzi, Chiara.  Formalisation of BPMN Models: a Focus on Correctness Properties.  University of Camerino, Phd Thesis, a.a. 2019/2020.
  * [NPZ12] Huu Nghia Nguyen, Pascal Poizat, and Fatiha Zaïdi.  A symbolic framework for the conformance checking of value-passing choreographies.  In ICSOC, volume 2012 of LNCS, pages 525–532. Springer, 2012\.
  * [NWM17] Adriatik Nikaj, Mathias Weske, and Jan Mendling.  Semi-automatic derivation of restful choreographies from business process choreographies.  Software & Systems Modeling, pages 1–14, 2017.
  * [OAS07] OASIS WSBPEL TC.  Web Services Business Process Execution Language Version 2.0.  Technical report, OASIS, April 2007.
  * [OMG11] OMG.  Business Process Model and Notation (BPMN V 2.0), 2011.
  * [Pas17] Oscar Pastor.  Model-driven development in practice: From requirements.  In Theory and Practice of Computer Science, volume 10139 of LNCS, pages 405–410. Springer, 2017.
  * [PS12] Pascal Poizat and Gwen Salaün.  Checking the realizability of BPMN 2.0 choreographies.  In Symposium on Applied Computing, pages 1927–1934. ACM, 2012.
  * [PTDL07] Michael P Papazoglou, Paolo Traverso, Schahram Dustdar, and Frank Leymann.  Service-oriented computing: State of the art and research challenges.  Computer, 40(11), 2007.
  * [QZCY07] Zongyan Qiu, Xiangpeng Zhao, Chao Cai, and Hongli Yang.  Towards the theoretical foundation of choreography.  In WWW, pages 973–982. ACM, 2007.
  * [RFG10] Mohsen Rouached, Walid Fdhila, and Claude Godart.  Web services compositions modelling and choreographies analysis.  International Journal of Web Services Research (IJWSR), 7(2):87–110, 2010.
  * [RH15] Ritter Daniel, and Holzleitner Manuel.  Integration adapter modeling.  In International Conference on Advanced Information Systems Engineering,  volume 9097 of LNCS, pages 468–482, Springer, 2015.
  * [RS16] Jan Ritter Danielm Sosulski.  Exception handling in message-based integration systems and modeling using BPMN  International Journal of Cooperative Information Systems volume 25, pages 1650004, World Scientific, 2016.
  * [SB09] Gwen Salaün, and Tevfik Bultan.  Realizability of choreographies using process algebra encodings.  In iFM, volume 5423 of LNCS, pages 167–182. Springer, 2009\.
  * [SBS06] Gwen Salaün, Lucas Bordeaux, and Marco Schaerf.  Describing and reasoning on web services using process algebra.  Int. J. of Business Process Integration and Management, 1(2):116–128, 2006.
  * [SLM+10] David Schumm, Frank Leymann, Zhilei Ma, Thorsten Scheibler, and Steve Strauch.  Integrating compliance into business processes.  Multikonferenz Wirtschaftsinformatik 2010, page 421, 2010.
  * [WDW12] Matthias Weidlich, Remco Dijkman, and Mathias Weske.  Behaviour equivalence and compatibility of business process models with complex correspondences.  The Computer Journal, 55(11):1398–1418, 2012.

## Appendix

We report here the proof of the proposition concerning the well-composedness
of the collaboration produced by the function $\mathcal{C}$.

See 1

######  Proof 8.1.

The proof proceeds by contradiction. Suppose that there exist $\overline{P}$
and $\overline{{\sf p}}$ such that $\mathcal{C}(\overline{P},\overline{{\sf
p}})=C$ and $C$ is not well-composed. By Def. 8, we have six cases (below
notation $\in^{n}$ means that the number of times an element occurs in the
multiset is $n$):

  1. (1)

$\exists({\sf p},{\sf p},{\sf m})\in{out}(C).$ This means that $C$ contains a
term ${\sf taskSnd}({\sf e}_{i},{\sf e}_{o},({\sf p},{\sf p},{\sf m}))$ or a
term ${\sf interSnd}({\sf e}_{i},{\sf e}_{o},({\sf p},{\sf p},{\sf m}))$. Le
us consider the former case, the other is similar. According to the
definitions of $\mathcal{C}$ and $\mathcal{N}$, the sending task results from
the evaluation of ${\sf taskSnd}({\sf e}_{i},{\sf e}_{o},(S({\sf m}),R({\sf
m}),{\sf m}))$ for some $S$ and $R$ such that $S({\sf m})=R({\sf m})={\sf p}$.
However, by definition of $\mathcal{N}$, $S({\sf m})\neq R({\sf m})$, which is
a contradiction.

  2. (2)

$\exists({\sf p}_{1},{\sf p}_{2},{\sf m})\in{out}(C)\ .\
\not\\!\\!\exists({\sf p}_{1},{\sf p}_{2},{\sf m})\in{in}(C)$ This means that
$C$ contains a term ${\sf taskSnd}({\sf e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf
p}_{2},{\sf m}))$ or a term ${\sf interSnd}({\sf e}_{i},{\sf e}_{o},({\sf
p}_{1},{\sf p}_{2},{\sf m}))$. Le us consider the former case, the other is
similar. According to the definitions of $\mathcal{C}$ and $\mathcal{N}$, the
sending task results from the evaluation of ${\sf taskSnd}({\sf e}_{i},{\sf
e}_{o},(S({\sf m}),R({\sf m}),{\sf m}))$ for some $S$ and $R$ such that
$S({\sf m})={\sf p}_{1}$ and $R({\sf m})={\sf p}_{2}$. The latter means that
$R$ has the form $\\{{\sf m}\mapsto{\sf p}_{2}\\}\sqcup R^{\prime}$ for some
$R^{\prime}$; according to the definition of $\mathcal{R}$, the pair $\\{{\sf
m}\mapsto{\sf p}_{2}\\}$ is produced by either $\mathcal{R}({\sf taskRcv}({\sf
e}_{i}^{\prime},{\sf e}_{o}^{\prime},{\sf m}),{\sf p}_{2})$, $\mathcal{R}({\sf
interRcv}({\sf e}_{i}^{\prime},{\sf e}_{o}^{\prime},{{\sf m}}),{\sf p}_{2})$
or $\mathcal{R}({\sf eventBased}({\sf e}_{i}^{\prime\prime},(({\sf m},{\sf
e}_{o}^{\prime\prime}),M)),{\sf p}_{2})$, with ${\sf taskRcv}$, ${\sf
interRcv}$ or ${\sf eventBased}$ term in $C$. Let us consider the case where
$C$ contains the term ${\sf taskRcv}({\sf e}_{i}^{\prime},{\sf
e}_{o}^{\prime},{\sf m})$; the other two cases are similar. By definition of
$\mathcal{N}$, and using the functions $S$ and $R$ above, we have
$\mathcal{N}({\sf taskRcv}({\sf e}_{i}^{\prime},{\sf e}_{o}^{\prime},{\sf
m}),S,R)={\sf taskRcv}({\sf e}_{i}^{\prime},{\sf e}_{o}^{\prime},(S({\sf
m}),R({\sf m}),{\sf m}))={\sf taskRcv}({\sf e}_{i}^{\prime},{\sf
e}_{o}^{\prime},({\sf p}_{1},{\sf p}_{2},{\sf m}))$. By applying function $in$
to this term, we obtain ${in}({\sf taskRcv}({\sf e}_{i}^{\prime},{\sf
e}_{o}^{\prime},({\sf p}_{1},{\sf p}_{2},{\sf m})))=\\{({\sf p}_{1},{\sf
p}_{2},{\sf m})\\}$, hence $({\sf p}_{1},{\sf p}_{2},{\sf m})\in{in}(C)$,
which is a contradiction.

  3. (3)

$\exists({\sf p}_{1},{\sf p}_{2},{\sf m})\in{out}(C)\ .\ \exists({\sf
p}_{1},{\sf p}_{2},{\sf m})\in^{2}{in}(C)$. According to the definition of
function $in$, this means that two terms of the form ${\sf taskRcv}({\sf
e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf m}))$, ${\sf interRcv}({\sf
e}_{i},{\sf e}_{o},({\sf p}_{1},{\sf p}_{2},{\sf m}))$ or ${\sf
eventBased}({\sf e}_{i},(({\sf p}_{1},{\sf p}_{2},{\sf m},{\sf e}_{o}),M))$
are in $C$. Thus, according to the definition of $\mathcal{N}$, two terms of
the form ${\sf taskRcv}({\sf e}_{i},{\sf e}_{o},{\sf m})$, ${\sf