Data-Aware Interaction
in Distributed and Collaborative Workflows:
Modeling, Semantics, Correctness
David Knuplesch and Rüdiger Pryss and Manfred Reichert
Institute of Databases and Information Systems
Ulm University, Germany
Email: {david.knuplesch,ruediger.pryss,manfred.reichert}@uni-ulm.de
Abstract—IT support for distributed and collaborative work-
flows and related interactions between business partners is
becoming increasingly important. For modeling such partner
interactions as flow of message exchanges, different top-down
approaches, covered under the term interaction modeling, are
provided. Like for workflow models, correctness constitutes a
fundamental challenge for interaction models as well; e.g., to
ensure the boundedness and absence of deadlocks and lifelocks.
Due to their distributed execution, in addition, interaction models
should be message-deterministic and realizable, i.e., the same
conversation (i.e. sequence of messages) should always lead to
the same result, and it should be ensured that partners always
have enough information about the messages they must or may
send in a given context. So far, most existing approaches have
addressed correctness of interaction models without explicitly
considering the data exchanged through messages and used for
routing decisions. However, data support is crucial for collabo-
rative workflows and interaction models respectively. This paper
therefore enriches interaction models with the data perspective.
In particular, it defines the behavior of data-aware interaction
models based on Data-Aware Interaction Nets, which use elements
of both Interaction Petri Nets [1] and Workflow Nets with Data [2].
Finally, formal correctness criteria for Data-Aware Interaction
Nets are derived, guaranteeing the boundedness and absence of
deadlocks and lifelocks, and ensuring message-determinism as
well as realizability.
I. INTRODUCTION
Workflow management is of utmost importance for compa-
nies that want to efficiently handle their workflows as well as
their interactions with partners and customers [3]. Despite the
varying issues relevant for the IT support of distributed and
collaborative workflows [4], common aspects to be considered
include the support of appropriate modeling techniques as
well as the definition of formal execution semantics, en-
suring proper and correct partner interactions (i.e., message
exchanges).
Workflow management methods and techniques tackling
these challenges consider a choreography as a specification
of message exchanges between the partners of a collaborative
workflow. Respective approaches provide a global view on dis-
tributed workflows and support partners in defining their intra-
organizational workflows (partner processes for short). The
latter can be transformed into distributed, executable work-
flows. When executing the latter, their interplay is expressed
in terms of a conversation (i.e., a sequence of exchanged
messages) that follows the global behavior specified by the
choreography.
Currently, there exist two different paradigms for model-
ing choreographies: interconnection modeling and interaction
modeling.Interconnection modeling uses message exchange
as link between partner processes or public views on them. In
particular, this paradigm does not allow modeling the message
exchange separately from the partner processes. Hence, it is
considered as a bottom-up approach. Approaches enabling in-
terconnection modeling include BPMN Collaboration Diagram
[5], BPEL4Chor [6], and Compositions of Open Nets [7]. By
contrast, interaction modeling provides a top-down approach.
An Interaction Model specifies the flow of message exchanges
without having any knowledge about the partner processes.
Moreover, the models of the partner processes are created
taking the interaction model into account. Nevertheless, com-
mon interaction models use the same patterns as workflow
models (e.g. parallel and conditional branchings), but instead
of tasks they refer to the messages exchanged. Approaches
enabling interaction modeling include iBPMN [8], BPMN
Choreography Diagrams [5], Service Interaction Patterns [9],
and WSCDL [10].
This paper focuses on the correctness of interaction models.
Related issues discussed in the literature include boundedness
and absence of deadlocks and lifelocks, as well as the realiz-
ability of interaction models [1], [7], [11], [12]. Realizability
postulates that partners always can compute which messages
they must or may send in a given execution context. Fig. 1 (1)
outlines a simple example of a non-realizable choreography
with four partners A, B, C, and Dand two messages m1
and m2. This interaction model specifies that after sending
message m1from Ato B, message m2must be sent from Cto
D. Obviously, only Aor Bknows when Cmust send message
m2, but Cdoes not have this knowledge. Consequently, this
interaction model is not realizable. A necessary precondition
for realizability is message-deterministic behavior, i.e. the
same conversation (i.e. sequence of messages) should always
lead to the same result. An example of an interaction model,
which is not message-deterministic, is shown in Fig. 1 (2);
this interaction model comprises partners A, B, and Cand
messages m1, m2, m3,and m4. After sending the first message
m1, either the upper or the bottom branch has to be chosen.
In any case, the next message m2must be sent from Bto
C. Depending on the branch chosen. However, Cthen either
must send m3to Bor m4to A. From the perspective of
C, it cannot be determined, which of the two interpretations
shall be applied. By contrast, Bmay know the chosen branch
(e.g., the upper one). Hence, Cmight send m4to A, while B
waits for m3, or vice versa. A property similar to realizability
is clear termination. It requires that a partner always can
compute whether or not he will be sender or receiver of
messages anymore. An example of an interaction model,
which is not clearly terminating, is shown in Fig. 1 (3).
This interaction model comprises partners A, B, and Cand
messages m1, m2, m3,and m4. After sending the first message
m1from Ato B,Bcan either send message m2to Aor
message m4to C. When choosing the first option (i.e. B
sends m2to A), Amust send m3to Cafterwards. In turn,
when choosing the second option (i.e. Bsends m4to C),
the execution is terminated, although Amay still wait for the
arrival of message m2. Note, that from the perspective of A
nothing has changed since m1was sent.
A
B
C
D
C
B
A
B
B
C
B
C
C
A
m1m2
m2m3
m2m4
m1
1 2
A
B
B
A
B
C
A
C
m2
m4
m3
m1
3
Sender
Legend:
A
B
m1
Receiver
Message
Fig. 1. Violating realizability, message-determinism, clear termination [1]
However, existing approaches for interaction modeling do
not adequately support the data perspective. Either related
execution semantics ignore the data perspective or there is
a lack of appropriate correctness criteria, especially if routing
decisions are based on message data.
This paper deals with fundamental correctness issues when
making interaction models data-aware. Section II provides an
example from the healthcare domain to emphasize the need
of data-awareness in interaction models. Section II further
discusses challenges to be tackled when considering the data
perspective. Section III then introduces our formal framework
for data-aware interaction modeling. First, an interaction
meta-model is provided in terms of the Data-Aware Chore-
ography (DAChor). The behavior of a DAChor is described
by a transformation to Data-Aware Interaction Nets (DAI
Nets). These combine Interaction Petri Nets [1] and Workflow
Nets with Data [2]. Based on Data-Aware Interaction Nets,
the set of allowed conversations (i.e., message exchanges) is
derived and used to introduce formal correctness criteria for
DAI Nets and DAChor respectively. These criteria guarantee
for the boundedness and absence of deadlocks and lifelocks,
and ensure message-determinism, realizability, and clear ter-
mination. Section IV discusses related work and Section V
concludes with a summary and outlook.
II. EXAMPLE, CHALLENGES, CONTRIBUTION
This section introduces a simplified real-world scenario.
The scenario was elaborated in the context of several case
studies we conducted in the healthcare domain. The case
studies highlighted the relevance of the data perspective in
interaction models. Thus, the scenario we selected emphasizes
the challenges arising from the support of data-awareness in
interaction models. It describes the transport of a patient to
and from a unit performing a Positron Emission Tomography
(PET) scan. A PET scan, is a kind of nuclear medicine
imaging not performed by the respective hospital itself in our
scenario. Thus, if a PET scan is ordered for a patient, patient
transportation to the provider of the PET scan is required. In
this context, the hospital has to inform the provider of the
PET scan about the patient’s status, such that this provider
can decide on preparations required. Furthermore, we require
a patient to be examined just before the transport to exclude
potential risks, if he is in a critical condition.
This simple scenario involves three partners: The
Hospital responsible for the patient and ordering the PET
scan, the Transportation (Transp.) Provider
transporting the patient, and the PET provider performing
the PET scan. The interaction starts with the Hospital
requesting the PET scan (Request PET). In the context of
this request, the Hospital informs the PET Provider
about the status of the patient. In turn, the PET provider
confirms the time when the scan is scheduled (Confirm),
and then requests the Transp. Provider to perform the
transport (Request Trans.).
●If the patient is in a critical condition, the Transp.
Provider requests the Hospital to examine the
patient to check whether he is transportable (Request
Exam.). Based on the Result of this examination, the
Hospital informs the Transp. Provider about,
whether to continue or abort the interaction.
●If the interaction is continued or the patient is not in a
critical condition, the Transp. Provider informs the
PET provider after picking up the patient and arriving
at the PET unit (Arrival). After the PET scan is per-
formed, the PET provider requests retransport of the
Transp. Provider (Retransport). Finally, the
Transp. Provider informs the Hospital about
the return of the patient (Return).
Obviously, properly modeling the interactions of this scenario
requires support for routing decisions based on the data of the
messages exchanged. More precisely, in the given scenario,
there is a decision referring to data of the first message
exchanged (i.e. whether or not the patient is in a critical
condition). Another decision refers to the message sent by
the hospital and indicating whether or not the request shall
be cancelled. Hence, we use a notation based on BPMN 2.0
[5] and iBPMN [1], but enrich it with so-called virtual data
objects. We denote this notation as Data-Aware Choreography
(DAChor) and use it to model our scenario in Fig. 2. Virtual
data objects have a data domain and can be used as variables
Transp. Provider
Hospital
Request Exam.
{abort, continue}
Hospital
Transp. Provider
Result
PET Provider
Transp. Provider
Retransport
Transp. Provider
PET Provider
Arrival
Transp. Provider
PET Provider
Cancel PET
Status
{uncritical, critical}
{uncritical, critical}
Hospital
PET Provider
Request PET
Date
PET Provider
Transp. Provider
Request Trans.
x
Order
{abort, continue}
x
Order=continue
Date
Hospital
PET Provider
Confirmation
xReturn
Transp. Provider
Hospital
Order=abort
Date
Hospital
PET Provider
Confirmation
x
x
Date
Hospital,
Transp. Provider
PET Provider
Confirmation+
Status=uncritical
Status=critical
Status=critical
Status=uncritical
Data Domain
Sender
Receivers
Interaction Class
Data Assignment
Interaction
Virtual Data Object
Legend:
Alternative 1
Alternative 2
Name
Data Domain
Fig. 2. Patient transportation scenario as DAChor
when defining conditions for routing decisions. Note that these
virtual data objects are not used to model information flow.
Thus, the data assignment relation denotes which data of an
interaction is assigned to a virtual data object. Note that such
a data assignment relation can only lead from an interaction
to a virtual data object, but not vice versa. Further, an inter-
action is assigned to a message class denoting the message
type. From the message class, the sender, the receivers, and
the data domain are inherited (e.g., boolean). Finally, when
executing a choreography, messages of the related message
class correspond to interactions.
Having a closer look at our scenario, one can recognize
that it neither ensures realizability nor clear termination. If
the Hospital requests canceling the PET scan, the PET
provider is not informed accordingly and hence may still
wait for the message; i.e., no clear termination is ensured.
However, if Alternative 2 is applied, the PET provider will
be informed and clear termination can be ensured. Further,
realizability is violated for the given interaction model, since
Transp. Provider does not know whether the patient is
in a critical condition. Thus, Transp. Provider cannot
determine whether to request an examination. In order to en-
sure realizability, it is not sufficient to only check whether this
information was directly sent to the Transp. Provider.
Consider Alternative 1, which ensures realizability by also
sending the confirmation to Transp. Provider, in case
the patient is in a critical condition. Obviously, implicit knowl-
edge of Transp. Provider about the value of virtual data
object Status is enough to ensure realizability. This makes
the definition of proper correctness criteria for data-aware
interaction models Section III very challenging.
Before defining correctness criteria for DAChors, their be-
havior has to be formalized. In [1], Decker et al. define the
behavior of iBPMN Choreographies based on their transfor-
mation to Interaction Petri Nets (IP Nets). However, IP Nets
are unaware of data. This raises the challenge to first enrich
IP Nets as well as their behavior with data to Data-Aware
Interaction Nets (DAI Nets). Following this, an appropriate
transformation is introduced.
The main contribution of this paper is to introduce a formal
framework for data-aware interaction models in distributed and
collaborative settings that puts emphasis on correctness. Espe-
cially, our framework considers particular correctness criteria
for interaction models (e.g. realizability, clear termination). It
should be clear, that the latter exceed classic correctness and
soundness criteria that are known from workflows and com-
mon service orchestrations through interconnection models
[7], [13], [14]. Further contributions include the introduction
of DAChors and DAI Nets as well as the transformation from
DAChors to DAI Nets and the definition of the behavior of
the latter.
III. FORMAL FRAMEWORK
This section introduces our formal framework for ensuring
correctness of data-aware interaction models. First, the
scope of an interaction model is described as interaction
domain and in terms of messages (cf. Def. 1 and Def. 2
in Section III-A). Second, Data-Aware Choreographies
(DAChors) are introduced as formal meta-model for data-
aware interaction modeling (cf. Def. 3 in Section III-B).
In Section III-D, the semantics of DAChors is described
based on their transformation to Data-Aware Interaction
Nets (DAI Nets). DAI Nets combine Interaction Petri Nets
(IP Nets) [1] and Workflow Nets with Data (WFD Nets) [2]
(cf. Def. 5 in Section III-C). Their behavior is described in
terms of markings and execution traces (cf. Def. 8–10 in
Section III-E). Def. 12 introduces conversations representing
the observable parts of an execution trace (i.e., exchanged
messages). Finally, partner views are defined (cf. Def. 14).
Based on traces, conversations, and views, we then introduce
correctness criteria for DAI Nets and DAChors respectively
fundament of ▼1
assigned
to ▲
Interaction Domain
Data-Aware
Choreography
Data-Aware
Interaction Net
Place Transition Option
Silent
Transition
Interaction
Transition
Trace
Message
View
Role
mapped
to ▼
element
of ▲
may
fire ▲
receiver
►
sender
►
view
of ▲
projected
onto ►
Interaction
Conversation
assigned
to ▲
mapped
to ▼
Message
Class
mapped
to ▼
Marking
Determinism
. Message-
Determinism
*
*
*
*
*
*
*
*
** *
1
Soundness
Subsequent
Markings .
1
1
**
*
Virtual
Data Object
mapped
to ▼
current
value ▲
Data
Domain ◄ has
assigned
to ▲
Virtual
Data Object Gateway,
Event
assigned
to ▲
*1
projected
onto ►
*
1
Realizability
*
* *
*
**
*
*
1 1
*
*
*
*
1
1
*
1
*
*
Clear
Termination
lead
◄ to
source
of ►
takes ▲1
1
1
1
*
pass by ►
*
Def. 1
Def. 2
Def. 3+4
Def. 8
Def. 9
Def. 10
Def. 5+6
Def. 11
Def. 12
Def. 13
Def. 14
Def. 15
Def. 9
Def. 7
Def. 7
Def. 7
Fig. 3. Overview of our formal framework
(cf. Def. 11, Def. 13, and Def. 15). Fig. 3 provides an
overview of the main elements of our formal framework and
their relations.
A. Interaction Domains and Messages
This section defines the basic elements of data-aware in-
teraction modeling in terms of an interaction domain. The
latter contains roles to differentiate the partners as well as
message classes and related data domains. Further, the notion
of message is introduced as an instance of a message class
(cf. Def. 1 and Example 1).
Definition 1 (Interaction Domain).An interaction domain is
a tuple I=(R,D, C, domC, sC, rC, ), with
●Ris a set of roles,
●Dis a set of data domains, whereby each D∈Dhas
finitely many values in it
●Cis a set of message classes,
●domC∶C→Dis a function assigning to each message
class a data domain,
●sC∶C→Rassigns the sender to each message class,
●rC∶C→2Rassigns the set of receivers to each mes. cl.,
●is the empty value.
Further, we define ΩI∶={}∪⋃
D∈DDas the set of all values.
Based on Def. 1, we introduce the notion of message in
Def. 2. A message constitutes an instance of a message class.
Furthermore, we introduce several sets of messages.
Definition 2 (Messages).Let I=(R,D, C, domC, sC, rC, )
be an interaction domain. Then: A message in Iis a tuple
µ=(c, x)∈C×ΩI, with
●c∈Cis the corresponding message class, and
●x∈domC(c)is the message content transferred.
Furthermore, we define:
●Σc∶={(c′, x)∈C×ΩI∣c′=c∧x∈domC(c′)}as set of
all messages corresponding to message class c∈C,
●ΣI∶=⋃c∈CΣcas set of all messages corresponding to
interaction domain I,
●ΣR→∶={(c, v)∈ΣI∣sC(c)=R}as set of all messages
sent by role R∈R,
●Σ→R∶={(c, v)∈ΣI∣R∈rC(c)} as set of all messages
received by role R,
●ΣR∶=ΣR→∪Σ→Ras set of all messages corresponding
to role R, i.e. sent or received by R
B. Data-Aware Choreography
Based on the interaction domain from Def. 1, we define the
notion of data-aware choreography (DAChor). DAChor en-
riches BPMN choreography models with virtual data objects,
a data-assignment relation, and guards.
Definition 3 (Data-Aware Choreography; DAChor).
Let I=(R,D, C, domC, sC, rC, )be an interaction
domain. Then: A a Data-Aware Choreogra-
phy (DAChor) over Iis a tuple DAC =
(N, I, G, es, Ee, Gs
+, Gm
+, Gs
d×, Gs
e×, Gm
×, V, class, →,⇢, domV, grd),
with
●Nis the set of nodes being the disjoint conjunction of the
set of interactions Iand the set of gateways and events G.
In turn, the latter is the disjoint conjunction of the start
event {es}, the set of end events Ee, the set of AND-splits
Gs
+, the set of AND-mergers Gm
+, the set of data-based
Example 1 (Basic Notations).Consider the interaction model from of the patient transportation scenario from Fig. 2. Its
interaction domain is I=(R,D, C, domC, sC, rC, )with:
R={Hospital,PET Provider,Transp. Provider}
D={D={}, DStatus ={uncritical, critical}, DOrder ={abort, continue}, DDate ={1.1.1900,...,31.12.2099}
C={Request PET,Confirmation,Request Trans.,Request Exam.,Result,Arrival,Retransport,Return,Confirmation+,Cancel PET}
sC(Request PET)=Hospital rC(Request PET)={PET provider}
sC(Confirmation)=PET provider rC(Confirmation)={Hospital}
sC(Request Trans.)=PET provider rC(Request Trans.)={Transp. Provider}
sC(Request Exam.)=Transp. Provider rC(Request Exam.)={Hospital}
sC(Result)=Hospital rC(Result)={Transp. Provider}
sC(Arrival)=Transp. Provider rC(Arrival)={PET provider}
sC(Retransport)=PET provider rC(Retransport)={Transp. Provider}
sC(Return)=Transp. Provider rC(Return)={Hospital}
sC(Confirmation+)=PET provider rC(Confirmation+)={Hospital, Transp. Provider}
sC(Cancel PET)=Transp. Provider rC(Cancel PET)={PET provider}
domC(Request PET)=DStatus domC(Confirmation)=DDate
domC(Request Trans.)=DDate domC(Request Exam.)=D
domC(Result)=DOrder domC(Arrival)=D
domC(Retransport)=DdomC(Return)=D
domC(Confirmation+)=DDate domC(Cancel PET)=D
ΣI={ (Request PET, uncritical),(Request PET, critical),(Result, abort),(Result, continue),(Request Exam., ),(Arrival, ),
(Confirmation,1.1.1900),...,(Confirmation,31.12.2099),(Confirmation+,1.1.1900),...,(Confirmation+,31.12.2099),
(Request Trans.,1.1.1900),...,(Request Trans.,31.12.2099),(Retransport, ),(Return, ),(Cancel PET, )}
XOR-splits Gs
dx, the set of event-based XOR-splits Gs
ex,
and the set of XOR-mergers Gm
x,
●Vis the set of virtual data objects,
●class ∶I→Cassigns a message class to each interac-
tion,
●→⊆(N−Ee)×(N−{es})is the interaction flow relation,
●⇢⊆I×Vis the data-assignment relation,
●domV∶V→Dis a function assigning a domain to each
virtual data object,
●grd ∶(→)→GV, is a function assigning a guard to each
interaction flow.
The set of guards GVis defined as the set of propositional
logic formulas over propositions of the form v=sor
v∈{s1, s2,...,sn}. Thereby, v∈Vis a virtual data object
and s, s1, s2,...,sn∈domV(v)are values of the related data
domain. If a guard g∈GVuses a virtual data object v∈V,
we denote this as v∈
∼g. Note that a guard can be constantly
true. In this case, we omit it in the graphical representation of
a DAChor (cf. Fig 2). In the following, we introduce the well-
formedness of DAChors. Then, Example 2 provides a formal
description of our scenario from Fig. 2.
Definition 4 (Well-Formed DAChor).A DAChor is well-
formed, iff each following property holds:
●the start event, each interaction, and each merge node
have exactly one successor, i.e., ∀n∈{es}∪I∪Gm
+∪Gm
×∶
∣{n′∈N∣n→n′}∣=1
●each split node has at least one successor, i.e.,
∀gs∈Gs
+∪Gs
d×∪Gs
e×∶∣{n∈N∣gs→n}∣≥1
●each end event, each interaction, and each split node have
exactly one predecessor, i.e., ∀n∈Ee∪I∪Gs
+∪Gs
d×∪Gs
e×∶
∣{n′∈N∣n′→n}∣=1
●each merge node has at least one predecessor, i.e.,
∀gm∈Gm
+∪Gm
×∶∣{n∈N∣n→gm}∣≥1
●each event-based XOR-split is solely followed by interac-
tions, i.e., ∀gs
e×∈Gs
e×∶{n∈N∣gs
e×→n}⊆I
●guards of interaction flows are constantly
true unless the source of an inter-
action flow is a data-based XOR-split, i.e.,
grd ((n1, n2))≠true ⇔n1∈Gs
d×
●the data of an interaction is solely assigned to variables
of the same data domain, i.e.,
∀i∈I, ∀v∈V∶i⇢v⇒domC(class(i))=domV(v).
●there exists no cycle that solely consists of gateways, i.e.,
∄g0, g1,...gn∈G∶g0→g1→⋅⋅⋅→gn→g0.
C. Data-Aware Interaction Net
We introduce the notion of Data-Aware Interaction Net
(DAI Net). It combines IP Nets [1] and WFD Nets [2]:
Hence, the main elements of a DAI Net are places and
transitions. To add data, these elements are enriched with
variables and guards on transitions as known from WFD Nets.
Furthermore, DAI Nets allow assigning message classes to
transitions. Like in IP Nets, respective transitions are denoted
as interaction transitions. Finally, all other transitions are
called silent transitions.
Definition 5 (Data-Aware Interaction Net;
DAI Net).Let I=(R,D, C, domC, sC, rC, )
be an interaction domain. Then: A tuple
#=(P, pin, Po, Pfi, T, TS, TI, V, class, →,⇢, domV, grd)is
called Data-Aware Interaction Net (DAI Net) over I, where
●Pis the set of places; Pcan be partitioned into the initial
place pin, the set of ordinary places Po, and the set of
final places Pfi,
●Tis the set of transitions; Tcan be partitioned into the
sets of silent transitions TSand the set of interaction
transitions TI,
●Vis the set of variables,
●class ∶TI→Cis a function assigning a message class
to each interaction transition,
●→⊆((P−Pfi)×T)∪(T×(P−{pin}))is the flow relation,
●⇢⊆TI×Vis the data-assignment relation. It expresses
that the data of an interaction transition is assigned to
the related variable,
Example 2 (DAChor).Consider the scenario from Fig. 2. Based on its interaction domain I(cf. Example 1) we can now
describe the given scenario as DAChor DAC =(N, I, G, es, Ee, Gs
+, Gm
+, Gs
d×, Gs
e×, Gm
×, V, class, →,⇢, domV, grd):
I={i1,...,i8}, Ee={e1
e, e2
e}, Gs
d×={gs1
d×, gs2
d×}, Gm
×={gm
×}, Gs
+=Gm
+=Gs
e×=∅, V ={Status,Order},⇢={(i1,Status),(i5,Order)}
→={(es, i1),(i1, i2),(i2, i3),(i3, gs1
d×),(gs1
d×, i4),(gs1
d×, gm
×),(i4, i5),(i5, gs2
d×),(gs2
d×, e1
e),(gs2
d×, gm
×),(gm
×, i6,),(i6, i7),(i7, i8),(i8, e2
e)}
class(i1)=Request PET class(i2)=Confirmation class(i3)=Request Trans. class(i4)=Request Exam.
class(i5)=Result class(i6)=Arrival class(i7)=Retransport class(i8)=Return
domV(Status)=Dstatus grd ((gs1
d×, i4))=Status =critical grd ((gs1
d×, gm
×))=Status =uncritical
domV(Order)=Dorder grd ((gs2
d×, e1
e))=Order =abort grd ((gs2
d×, gm
×))=Order =continue
●domV∶V→Dis a function assigning a data domain to
each variable,
●grd ∶T→GV, is a function assigning a guard (cf. Def 3)
to each interaction flow relation.
Further, we define
●Σ#∶=⋃i∈TIΣclass(i)as the set of all messages corre-
sponding to #
●P→t∶={p∈P∣p→t}as the set of all places preceding t
●P←t∶={p∈P∣t→p}as the set of all places succeeding t
●P↮t∶={p∈P∣p↛t∧t↛p}as the set of the faraway
places of t
Definition 6 (Well-Formed DAI Net).A DAI Net is well-
formed, iff each following property holds:
●each transition has at least one preceding and one
succeeding place, i.e., ∀t∈T∶∃p1, p2∈P∶p1→t→p2
●the data of an interaction transition is solely assigned to
variables of the same data domain, i.e., ∀ti∈TI,∀v∈
V∶ti⇢v⇒domC(class(ti))=domV(v).
●there exists no cycle solely consisting of places and silent
transitions, i.e., ∄p0, p1,...pn∈P, t0, t1,...tn∈TS∶
p0→t0→p1→t1→⋅⋅⋅→pn→tn→p0.
D. Mapping DAChors to DAI Nets
In Section III-C, we introduced DAI Nets to define the
behavior of DAChors. Thus, we now define a mapping from
data-aware choreographies to DAI Nets. This mapping is
based on the approach proposed by Decker et al. [1] who
define the behavior of iBPMN Choreographies through their
transformation to IP Nets.
Definition 7 (Mapping DAChors to DAI Nets).Let
DAC =(N, I, G, es, Ee, Gs
+, Gm
+, Gs
d×, Gs
e×, Gm
×, V, class, →
,⇢, domV, grd)be a DAChor (cf. Def. 3). Then, DAC
can be mapped to a DAI Net #that is defined as #∶=
(P, pin, Po, Pfi, T, TS, TI, V, class′,→′,⇢′, domV, grd′),
whereby
P∶={p(n1,n2)∣(n1, n2)∈→∧n1∉Gs
e×}
pin ∶=p(es,n)∈P, whereby es→n∈N
Pfi ∶={p(n,ee)∣p(n,ee)∈P∧ee∈Ee}⊆P
Po∶=P−({pin}∪Pfi)
T+∶={tg+∣g+∈Gs
+∪Gm
+}
Ts
×∶={ts
(gs
×,n)∣gs
×∈Gs
d× ∧n∈N∧gs
×→n}
Tm
×∶={tm
(n,gm
×)∣gm
×∈Gm
×∧n∈N∧n→gm
×}
TI∶={ti∣i∈I}, TS∶=T+∪Ts
×∪Tm
×, T ∶=TS∪TI
class′(ti)∶=class(i)
→′∶={(p(n1,n2), tn2)∣n1→n2∧n1∉Gs
e×
∧n2∈I∪Gs
+∪Gm
+}
∪{(tn1, p(n1,n2))∣n1→n2∧n1∈I∪Gs
+∪Gm
+}
∪{(p(n1,n2), tm
(n1,n2))∣n1→n2∧n2∈Gm
×}
∪{(tm
(n0,n1), p(n1,n2))∣n0→n1→n2∧n1∈Gm
×}
∪{(p(n1,n2), ts
(n2,n3))∣n1→n2→n3∧n2∈Gs
d×}
∪{(ts
(n1,n2), p(n1,n2))∣n1→n2∧n1∈Gs
d×}
∪{(p(n0,n1), tn2)∣n0→n1→n2∧n1∈Gs
e×}
⇢′∶={(ti, v)∣(i, v)∈⇢}
grd′(t)∶={grd ((gs
×, n)),iff t=t(gs
×,n)∈Ts
×
true,else
Theorem 1 states that the mapping from DAChors to DAI
Nets preserves well-formedness as prooven in [15]. The ap-
plication to our example is shown in Example 3 and Fig. 4.
Theorem 1. Preservation of Well-Formedness
Let DAC be a DAChor that is mapped to a DAI Net #. If
DAC is well-formed, then #also is well-formed.
E. Behavior of DAI Nets
Since DAI Nets are based on both WFD Nets and IP
Nets, we use token semantics (i.e., tokens assigned to places
and token changes) to define their behavior. Together with
the values of variables, tokens define the marking of a DAI
Net. Each Interaction Net starts with an initial marking, with
exactly one token being placed in the initial place pin and
each variable having the empty value . A marking is called
final, if all tokens belong to final places of Pfi. A transition t
is activated under marking m, iff all directly preceding places
of tcontain at least one token, and the guard of tis evaluable
and evaluates to true.
Definition 8 (DAI Net Markings and Activated Transi-
tions).Let #=(P, pin, Po, Pfi, T, TS, TI, V, class, →,⇢
, domV, grd)be a DAI Net. Then: A marking of #is a tuple
m=(⊙, val)composing two functions with
●⊙ ∶ P→N0assigns to each place the number of
corresponding tokens,
●val ∶V→ΩIassigns to each variable its current value;
val(v)is either the empty value or an element of the
variable’s domain, i.e., val(v)∈domV(v)∪{}.
Additionally, for each DAI Net #we define:
●the set of all markings M#, whereby
M#∶={m=(⊙, val)∣mis marking of #}
Example 3 (Transformation).The DAChor DAC =(N, I, G, es, Ee, Gs
+, Gm
+, Gs
d×, Gs
e×, Gm
×, V, class, →
,⇢, domV, grd)from our Example 2 (i.e., the patient transport scenario) is mapped to the
DAI Net #=(P, pin, Po, Pfi, T, TS, TI, V, class′,→′,⇢′, domV, grd′)as follows (cf. Fig. 4):
P={p(es,i1), p(i1,i2), p(i2,i3), p(i3,gs1
d×), p(gs1
d×,i4), p(gs1
d×,gm
×), p(i4,i5), p(i5,gs2
d×), p(gs2
d×,e1
e), p(gs2
d×,gm
×), p(gm
×,i6,), p(i6,i7), p(i7,i8), p(i8,e2
e)}
pin =p(es,i1)Pfi ={p(gs2
d×,e1
e), p(i8,e2
e)}Po=P−({pin}∪Pfi)
Ts
×={ts
(gs1
d×,i4), ts
(gs1
d×,gm
×), ts
(gs2
d×,e1
e), ts
(gs2
d×,gm
×)}Tm
×={tm
(gs1
d×,gm
×), tm
(gs2
d×,gm
×)}T+=∅TS=T+∪Ts
×∪Tm
×TI={ti1, ti2,...,ti8}
V={Status,Order}⇢′={(ti1,Status),(ti5,Order)}
→′={(p(es,i1), ti1),(p(i1,i2), ti2),(p(i2,i3), ti3),(p(gs1
d×,i4), ti4),(p(i4,i5), ti5),(p(gm
×,i6,), ti6),(p(i6,i7), ti7),(p(i7,i8), ti8),(ti1, p(i1,i2)),
(ti2, p(i2,i3)),(ti3, p(i3,gs1
d×)),(ti4, p(i4,i5)),(ti5, p(i5,gs2
d×)),(ti6, p(i6,i7)),(ti7, p(i7,i8)),(ti8, p(i8,e2
e)),(p(gs1
d×,gm
×), tm
(gs1
d×,gm
×)),
(p(gs2
d×,gm
×), tm
(gs2
d×,gm
×)),(tm
(gs1
d×,gm
×), p(gm
×,i6,)),(tm
(gs2
d×,gm
×), p(gm
×,i6,)),(p(i3,gs1
d×), ts
(gs1
d×,i4)),(p(i3,gs1
d×), ts
(gs1
d×,gm
×)),(p(i5,gs2
d×), ts
(gs2
d×,e1
e)),
(p(i5,gs2
d×), ts
(gs2
d×,gm
×)),(ts
(gs1
d×,i4), p(gs1
d×,i4)),(ts
(gs1
d×,gm
×), p(gs1
d×,gm
×)),(ts
(gs2
d×,e1
e), p(gs2
d×,e1
e)),(ts
(gs2
d×,gm
×), p(gs2
d×,gm
×))}
class′(ti1)=Request PET class′(ti2)=Confirmation class′(ti3)=Request Trans. class′(ti4)=Request Exam.
class′(ti5)=Result class′(ti6)=Arrival class′(ti7)=Retransport class′(ti8)=Return
domV(Status)=DStatus grd (ts
(gs1
d×,i4))=Status =critical grd (ts
(gs1
d×,gm
×))=Status =uncritical
domV(Order)=DOrder grd (ts
(gs2
d×,e1
e))=Order =abort grd (ts
(gs2
d×,gm
×))=Order =continue
●the initial marking min
#∶=(⊙in, valin)∈M#, whereby
⊙in(p)∶={1, if p =pin
0, else ∧ ∀v∈V∶valin(v)∶=
●the set of all final markings F#, whereby
F#∶={(⊙, val)∈M#∣∀p∈P∶⊙(p)≠0⇔p∈Pfi}
Further, ↝⊆M#×Tis the transition activation relation. m↝
tdenotes that marking m∈M#activates transition t∈T, iff
the following conditions hold:
1) ∀p∈P→t∶⊙(p)≥1,
2) ∀v∈
∼grd(t)∶val(v)≠,
3) grd(t)is satisfied for marking m
If a transition is activated, it may fire and lead from the
current marking to a subsequent one. More precisely, one
token is taken from each preceding place and one is added
to each succeeding place. Silent transitions fire immediately
when becoming activated. Activated interaction transitions fire,
iff a message of the corresponding message class is sent. In
this case, the value of the message is assigned to virtual data
objects as expressed by the data assignment relation. Note that
a message can only be sent if an interaction transition of the
related message class is activated and no silent transition is
activated (cf. Def. 9).
Definition 9 (Options + Subsequent Markings of DAI
Nets).Let #=(P, pin, Po, Pfi, T, TS, TI, V, class, →,⇢
, domV, grd)be a DAI Net, an m=(⊙, val), m′=(⊙′, val′)∈
M#be two markings of #. Then:
●O#∶=TS∪Σ#is the set of all options on #.
●opt#∶M#→2O#∶m↦{o∈O#∣∃m′∧mo
→m′}
maps each marking mto the options available under m.
●mo
→m′expresses that mleads to m′by applying option
o∈opt#(m)with:
Case 1: o=ts∈TSis a silent transition. Then: mts
→m′holds,
iff each of the following conditions is met:
1) m↝ts,
2) ∀p∈P→ts∶ ⊙′(p)=⊙(p)−1,
3) ∀p∈P←ts∶ ⊙′(p)=⊙(p)+1,
4) ∀p∈P↮ts∶ ⊙′(p)=⊙(p),
Transp. Provider
Hospital
Request Exam.
{abort, continue}
Hospital
Transp. Provider
Result
PET Provider
Transp. Provider
Retransport
Transp. Provider
PET Provider
Arrival
Status
{uncritical, critical}
{uncritical, critical}
Hospital
PET Provider
Request PET
Date
PET Provider
Transp. Provider
Request Trans.
Order
{abort, continue}
Date
Hospital
PET Provider
Confirmation
Date
Hospital
PET Provider
Confirmation
Date
Hospital,
Transp. Provider
PET Provider
Confirmation+
Alternative 1
Status=critical
Status=uncritical Order=continue Order=abort
Return
Transp. Provider
Hospital
Status=uncritical
Status=critical
Transp. Provider
PET Provider
Cancel PET
Alternative 2
Fig. 4. DAI Net derived for the patient transportation scenario
5) ∀v∈V∶val′(v)=val(v).
Case 2: o=µ=(c, v)∈Σ#is a message. Then: mµ
→m′holds,
iff each of the following conditions is met:
1) ∀ts∈TS∶mts, and
2) ∃ti∈TI∶m↝ti∧µ∈Σclass(ti),
3) ∀p∈P→ti∶,⊙′(p)=⊙(p)−1,
4) ∀p∈P←ti∶ ⊙′(p)=⊙(p)+1,
5) ∀p∈P↮ti∶ ⊙′(p)=⊙(p),
6) ∀v∈Vwith ti⇢v∶val′(v)=x,
7) ∀v∈Vwith tiv∶val′(v)=val(v).
Based on Def. 9, the following two theorems can be derived
(cf. [15]).
Theorem 2. Separation of Options Let #be a DAI Net. Then:
For each marking, the set of options solely contains either
silent transitions or messages or it is empty, i.e., ∀m∈M#∶
opt#(m)≠∅⇒opt#(m)⊆TS⊕opt#(m)⊆Σ#
Theorem 3. Termination of final markings Let #be a DAI
Net. Then: For each final marking, the set of options is empty,
i.e., ∀m∈F#∶opt#(m)=∅.
Based on Def. 9, we further define traces on DAI Nets as
sequences of options. To be more precise, a trace corresponds
to a related sequence of markings that starts with the initial
marking. If this related sequence of markings ends with a final
marking, we denote the trace as completed trace.
Definition 10 (Traces, and Prefixes, and Extensions).
(A) Let #=(P, pin, Po, Pfi, T, TS, TI, V, class, →,⇢
, domV, grd)be a DAI Net and τ=(τk)k∈[1..n]∈O⋆
#be a
finite sequence of options (i.e. silent transitions and messages)
of length ∣τ∣=∶n∈N. Let further m=(mk)k∈[1..n+1]∈M⋆
#
be a finite sequence of markings of length n+1. Then:
●τ∼mdenotes that τand mare related sequences, iff
∀l∈[1..n]∶ml
τl
→ml+1and m1=min
#.
●last ∶M⋆
#→M#with (mk)k∈[1..n]↦mnis a function
mapping a sequence of markings to its last marking.
●τ∈O⋆
#is a trace, iff ∃m∈M⋆
#and τ∼m. If last(m)∈
F#, we denote τa completed trace.
●T#denotes the set of all traces on #.
●Tc
#denotes the set of all completed traces on #.
(B) Let a=(ak)k∈[1..n], b =(bk)k∈[1..l], c =(cm)m∈[1..m]∈
L⊆M⋆be three elements of set Lbeing a set of sequences
over the elements of set M. Then:
●a⊴b(a◁b) denotes aa prefix (real prefix) of band b
an extension (real extension) of a, iff n≤l(n<l) and
∀i∈[1..n]∶ai=bi,
●a+c=bdenotes that ais extended by cto b, iff m+n=l,
and ais prefix of b, and ∀i∈[1..m]∶ci=bn+i,
●L⊴b∶={a∈L∣a⊴b}(resp. L◁b∶={a∈L∣a◁b})
denotes the subset of Lthat contains all prefixes (resp.
real prefixes) of b∈L, and
●L⊵b∶={a∈L∣b⊴a}(resp. L▷b∶={a∈L∣b◁a}) denotes
the subset of Lthat contains all extensions (resp. real
extensions) of b∈L.
After describing the behavior of a DAI Net by means of its
traces, we can use traces to characterize the desired behavioral
properties of DAI Nets. The first one is determinism. It
expresses that a trace is unique in terms of its related markings,
i.e., replaying a trace will always lead to the same marking.
The second fundamental property is soundness in terms of
boundedness as well as the absence of deadlocks and lifelocks
(cf. [16]).
Definition 11 (Determinism and Soundness).
(A) We call a DAI Net #deterministic, iff for each trace τon
#there exists exactly one related sequence of markings, i.e.,
∀τ∈T#∶∣{m∈M⋆
#∣m∼τ}∣=1.
Let #be a deterministic DAI Net. Then: Function mark#
maps each trace on #to its current marking, i.e. the last
marking of the related sequence of markings:
mark#∶T#→M#∶τ↦mark#(τ)∶=last(m), whereby
mis defined by τ∼∶m∈M⋆
#; Since #is deterministic, the
definition of mis unique. Thus, mark#is well-defined.
(B) We call a deterministic DAI Net #sound, iff all following
conditions hold:
●there exist completed traces on #, i.e., Tc
#≠∅,
●each trace on #is a prefix of a completed trace, i.e.,
∀υ∈T#∃τ∈Tc
#∶υ⊴τ.
●the set of reachable markings is finite, i.e.,
∣{m∈M#∣∃τ∈T#∶last(τ)=m}∣∈N
Note that the observable behavior of any DAI Net is
solely explained through the messages exchanged. Hence, we
must abstract from the silent elements of traces (i.e. silent
transitions) and define the observable behavior as conversation
being the projection of a trace to its messages (i.e., the part
of the trace defining its semantic). In the following, we first
introduce projections of sequences.
Definition 12 (Projections and Conversations).
Let A, B be two sets with B⊆A, and #=
(P, pin, Po, Pfi, T, TS, TI, V, class, →,⇢, domV, grd)be
a DAI Net, and τ∈T#be a trace on #. Then:
●ΠB∶A⋆→B⋆∶a↦ΠB(a)is the projection function
that restricts a sequence a∈A⋆to its elements of B,
●η∈Σ⋆
#denotes a conversation on #, iff it is the
projection of a trace on #to its messages, i.e., ∃(τ)∈
T#∶ΠΣ#(τ)=η.ηdenotes a completed conversation on
#, iff it is the projection of a completed trace on #,
●C#(Cc
#) denotes the set of all conversations on #,
●Cc
#denotes the set of all completed conversations on #,
●con#∶T#→C#∶τ↦con#(τ)∶=ΠΣ#(τ)maps each
trace to the related conversation.
As aforementioned, the behavior of silent transitions is not
observable. Hence, to ensure compatible behavior of partici-
pating roles, silent transitions must behave deterministically.
In other words, it must be possible to determine the behavior
of a DAI Net solely based on the messages exchanged,
i.e., message-determinism. First, this requires, that firing of
silent transitions always terminates (i.e., it is impossible to
solely execute silent transitions infinitely). Second, when silent
Example 4 (Traces and Conversations).Consider the DAI Net #from Example 3. Its set of completed traces of Tc
#consists
of traces τ1,τ2, and τ3. Projecting them to their messages leads to the conversations η1,η2, and η3, which build Cc
#:
τ1=<(Request PET, uncritical),(Confirmation,_2),(Request Trans.,_2), ts
(gs1
d×,gm
×), tm
(gs1
d×,gm
×),(Arrival, ),(Retransport, ),(Return, )>
τ2=<(Request PET, critical),(Confirmation,_2),(Request Trans.,_2), ts
(gs1
d×,i4),(Request Exam., ),(Result, abort), ts
(gs2
d×,e1
e)>
τ3=<(Request PET, critical),(Confirmation,_2),(Request Trans.,_2), ts
(gs1
d×,i4),(Request Exam., ),(Result, continue), ts
(gs2
d×,gm
×), tm
(gs2
d×,gm
×),
(Arrival, ),(Retransport, ),(Return, )>
η1=con#(τ1)∶=ΠΣ#(τ1)=<(Request PET, uncritical),(Confirmation,_2),(Request Trans.,_2),(Arrival, ),(Retransport, ),(Return, )>
η2=con#(τ2)∶=ΠΣ#(τ2)=<(Request PET, critical),(Confirmation,_2),(Request Trans.,_2),(Request Exam., ),(Result, abort)>
η3=con#(τ3)∶=ΠΣ#(τ3)=<(Request PET, critical),(Confirmation,_2),(Request Trans.,_2),(Request Exam., ),(Result, continue),
(Arrival, ),(Retransport, ),(Return, )>
transitions terminate, the set of activated options must only
depend on the messages exchanged before (i.e., it must be
independent from the order, in which the silent transitions were
fired). 1
Theorem 4. Termination of silent subtraces On a well-formed
DAI Net #, any trace cannot infinitely be continued by silent
transitions, i.e. ∀τ∈T#holds ∃N∈N∶ ∀υ∈T⊵τ
#with
∣τ∣+N<∣υ∣⇒con#(τ)≠con#(υ).
According to Theorem 4 from [15], a DAI Net is message-
deterministic, if the set of activated messages solely depends
on the messages exchanged before (cf. Def. 13).
Definition 13 (Message-Determinism).We call a deterministic
and sound DAI Net #message-deterministic, iff the same
sequence of messages always activates the same messages, i.e.,
the set of activated messages solely depends on the messages
exchanged before, i.e.,
∀τ, υ ∈T#∶
(opt#(mark#(τ)), opt#(mark#(υ))⊆Σ#∧ΠΣ#(τ)=ΠΣ#(υ)) ⇒
opt#(mark#(τ))=opt#(mark#(υ))
Let #be a deterministic, sound and message-deterministic
DAI Net. Then: Function mark#maps each conversation to
the set of messages it activates:
mo#∶C#→2Σ#∶η↦mo#(η)∶=opt#(mark#(τ)),τ∈
O⋆
#is defined by η=con#(τ)and opt#(mark#(τ))⊆Σ#.
Since #is message-deterministic, the definition is unique.
Thus, mo#is well-defined.
Until now, we solely considered DAI Nets and conversations
from a global perspective. However, a role solely knows
messages of a conversation it sends or receives itself. Thus, in
Def. 14 the view of a role on messages of a conversation is
introduced. Further, for each role the set of activated options
is defined.
Definition 14 (Views on Conversations and Options).
Let I=(R,D, C, domC, sC, rC, )be an interaction domain
and let the tuple #=(P, pin, Po, Pfi, T, TS, TI, V, class, →
,⇢, domV, grd)be a sound, deterministic, and message-
deterministic DAI Net and let R∈Rbe a role. Then we can
define the following views
1For reasons of simplification, we abstract from irrelevant message content
in Example 4
●vcR
#∶C⋆
#→Σ⋆
R∶(ηk)k∈[1..n]↦vcR
#(η)∶=ΠΣR(η)maps
each conversation on #to the view of Ron it, wherby
the view is the projection to the messages sent or received
by R,
●vcR→
#∶C⋆
#→Σ⋆
R∶(ηk)k∈[1..n]↦vcR→
#(η)∶=ΠΣR→(η)
maps each conversation on #to the messages sent by R,
●voR
#∶2Σ#→2ΣR∶M↦voR
#(M)∶=M∩ΣRmaps each
set of messages to its messages sent or received by R,
●voR→
#∶2Σ#→2ΣR→∶M↦voR→
#(M)∶=M∩ΣR→maps
each set of messages to its messages sent by Rand,
Based on Def. 14, we can define realizability. It denotes
DAI Nets to be deterministic from the viewpoint of a role.
Further, clear termination is defined, which indicates that a
role can determine when it sent or received its last message.
Definition 15 (Realizability, Clear Termination).Let #be
a deterministic, sound, and message-deterministic DAI Net.
Then, for a role R∈R:
●#is realizable, iff the messages role Rmay send solely
depend on the messages, Rhas sent and received before,
i.e., ∀R∈R∶ ∀η, κ ∈C#∶vcR
#(η)=vcR
#(κ)⇒
voR→
#(mo#(η)) =voR→
#(mo#(κ))
●#clearly terminates, iff it solely depends on the messages
Rhas sent and received before, whether or not further
interaction with Rwill occur, i.e.,
∀R∈R∶∀η∈Cc
#∄κ∈C#∶vcR
#(η)◁vcR
#(κ)
An important issue concerns decidability of the introduced
properties of DAI Nets and DAChors; i.e., determinism, sound-
ness (cf. Def. 11), message-determinism (cf. Def. 13), and
realizability and clear termination (cf. Def. 15). Basically,
these properties are decidable. Due to lack of space, we omit
a discussion in this paper.
IV. RELATED WORK
In the context of workflows, correctness has been discussed
for a long time [16]. The approaches presented [2], [17]
consider data as well. The two paradigms for modeling
choreographies (i.e. interconnection and interaction models)
are compared in [18]. Examples of interconnection models
are BPMN 2.0 Collaborations [5] and BPEL4Chor [6]. There
are several approaches that discuss the verification classic
soundness criteria (i.e. boundedness, absence of deadlocks, ab-
sence and lifelocks) of distributed and collaborative workflows
and service orchestrations [7], [13], [14], [19]–[22]. Some
approaches use data dependencies to interconnect processes
and to define process interaction [23], [24]. Examples of in-
teraction models (i.e., the paradigm we apply) include Service
Interaction Pattern [9], WSCDL [10], iBPMN Choreographies
[1], and BPMN 2.0 Choreographies [5]. Our approach has
been mainly inspired by [1], which defines the behavior of
iBPMN Choreographies through their transformation to Inter-
action Petri Nets, and further discusses correctness and real-
izability. Also, realizability of interaction models is discussed
in [11], [25]. Furthermore, [12] provides a tool for checking
realizability of BPMN 2.0 Choreographies. However, all these
approaches do not explicitly consider the data exchanged by
messages and used for routing decisions.
In [26], [27], state-based conversation protocols are intro-
duced that are aware of the content of messages. The messages
(and data) exchanged trigger state transitions. Thus, different
data may trigger different transitions. However, conversation
protocols do not support the modeling of parallelism because
they are state-based. Furthermore, realizability of conversation
protocols requires that at every state each partner is either
able to send or receive a message or to terminate (autonomy
condition). This condition strongly restricts parallelism. For
example, consider a choreography solely consisting of two
parallel branches: In the upper branch partner Asends a
message m1to partner Band partner Bsends message m2to
Ain the bottom branch. Obviously, the autonomy condition is
violated although the choreography is realizable (cf. Def. 15).
Hence, conversation protocols do not constitute interaction
models in our point of view. Thus, to our best knowledge
the framework presented within this paper is the first one
that considers realizability and clear termination of data-aware
interaction models.
V. SUMMARY AND OUTLOOK
Our vision is to provide sophisticated support for distributed
and collaborative workflows. To foster this vision, we base our
work on the analysis of scenarios from different domains. In
essence, we learned that data support is practically relevant
for interaction models from a varity of domains.
Further, this paper introduced a formal framework for data-
aware interaction models and described how correctness can be
ensured. The main parts of our framework include DAChors
and DAI Nets as well as the transformation of DAChors to
DAI Nets. Further, the bahavior of DAI Nets is definde. Other
fundamental contributions are the definitions of correctness
criteria for data-aware interaction models. The latter include
message-determinism, realizability, and clear termination. In
future work, we will extend our framework to support asyn-
chronous message exchange and related correctness properties.
Finally, we will develop algorithms for efficiently checking
correctness of data-aware interaction models. In this context,
we plan to apply abstraction strategies to large data domains
similar to [28].
ACKNOWLEDGMENT
This work was done within the research project C3Pro
funded by the German Research Foundation (DFG), Project
number: RE 1402/2-1.
REFERENCES
[1] G. Decker and M. Weske, “Interaction-centric modeling of process
choreographies,” Information Systems, vol. 36, no. 2, pp. 292–312, 2011.
[2] N. Trˇ
cka, W. M. P. van der Aalst, and N. Sidorova, “Data-flow anti-
patterns: Discovering data-flow errors in workflows,” Proc. CAiSE’09,
pp. 425–439, 2009.
[3] M. Reichert and B. Weber, Enabling Flexibility in Process-Aware
Information Systems. Springer, 2012.
[4] M. Reichert, T. Bauer, and P. Dadam, “Enterprise-wide and cross-
enterprise workflow management: Challenges and research issues for
adaptive workflows,” in Proc. Enterprise-wide and cross-enterprise
workflow management, 1999, pp. 55–64.
[5] OMG/BPMI, “Bpmn version 2.0,” 2011.
[6] G. Decker and et al., “Bpel4chor: Extending bpel for modeling chore-
ographies,” ICWS 2007, pp. 296–303, 2007.
[7] W. M. P. van der Aalst and et al., “Multiparty contracts: Agreeing
and implementing interorganizational processes,” The Computer Journal,
vol. 53, no. 1, pp. 90–106, 2010.
[8] G. Decker and A. P. Barros, “Interaction modeling using bpmn,” in
Business Process Management Workshops, 2007, pp. 208–219.
[9] A. Barros, M. Dumas, and A. Ter Hofstede, “Service interaction pat-
terns,” Business Process Management, pp. 302–318, 2005.
[10] W3C, “Web services choreography description language v1.0,” 2005.
[11] N. Lohmann and K. Wolf, “Realizability is controllability,” Web Services
and Formal Methods, pp. 110–127, 2010.
[12] P. Poizat and G. Salaün, “Checking the realizability of BPMN 2.0
choreographies,” in Proc. SAC’11, 2011.
[13] D. Yellin and R. Strom, “Protocol specifications and component adap-
tors,” ACM TOPLAS, vol. 19, no. 2, pp. 292–333, 1997.
[14] S. Rinderle, A. Wombacher, and M. Reichert, “Evolution of process
choreographies in DYCHOR,” in Proc. CoopIS’06, 2006, pp. 273–290.
[15] D. Knuplesch and M. Reichert, “A formal framework for data-aware
process interaction models,” Ulm University, Tech. Rep. 2012-06, 2012.
[16] W. M. P. van der Aalst, “Verification of workflow nets,” Application and
Theory of Petri Nets, pp. 407–426, 1997.
[17] M. Reichert and P. Dadam, “ADEPTflex – supporting dynamic changes
of workflows without losing control,” Journal of Intelligent Information
Systems, vol. 10, no. 2, pp. 93–129, 1998.
[18] O. Kopp and F. Leymann, “Do we need internal behavior in choreogra-
phy models,” in Proc. ZEUS’09, 2009, pp. 2–3.
[19] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “An integrated work-
bench for model-based engineering of service compositions,” Services
Computing Transactions on, vol. 3, no. 2, pp. 131–144, 2010.
[20] S. Rinderle, A. Wombacher, and M. Reichert, “On the controlled
evolution of process choreographies,” in Proc. ICDE’06, 2006, p. 124.
[21] M. Reichert, T. Bauer, and P. Dadam, “Flexibility for distributed
workflows,” in Handbook of Research on Complex Dynamic Process
Management. BSR, IGI Global, 2009, pp. 137–171.
[22] M. Reichert and T. Bauer, “Supporting ad-hoc changes in distributed
workflow management systems.” in Proc. CoopIS’07, 2007, pp. 150–
168.
[23] V. Künzle and M. Reichert, “Philharmonicflows: towards a framework
for object-aware process management,” Software Maintenance and Evo-
lution: Research and Practice, vol. 23, no. 4, pp. 205–244, 2011.
[24] D. Müller, M. Reichert, and J. Herbst, “Data-driven modeling and
coordination of large process structures,” in Proc. CoopIS’07, 2007, pp.
131–149.
[25] G. Decker, “Realizability of interaction models,” in Proc. ZEUS’09,
2009, pp. 55–60.
[26] X. Fu, T. Bultan, and J. Su, “Conversation protocols: A formalism for
specification and verification of reactive electronic services,” in Proc.
CIAA’04, 2004, pp. 188–200.
[27] ——, “Realizability of conversation protocols with message contents,”
Web Services Research, vol. 2, no. 4, pp. 68–93, 2005.
[28] D. Knuplesch, L. Ly, S. Rinderle-Ma, H. Pfeifer, and P. Dadam, “On
enabling data-aware compliance checking of business processmodels,”
in Proc. ER’10, 2010, pp. 332–346.
