In scenarios where a set of independent business partners engage in complex conversations, interaction models are a means to specify the allowed interaction behavior from a global perspective. Atomic interactions serve as basic building blocks and behavioral dependencies are de ned between them. The notion of realizability centers around the question whether there exist a set of roles that collectively realize the speci ed behavior. This notion has been studied in the literature in different avors. This paper aims at providing an overarching framework for realizability.
Conversation models, as presented in [
s1 (A,τ,A) (C,y,D) (b)
(C,z,D) of roles and M the set of message types. The 3-tuple (s; m; r) then describes the sender, the type and the receiver of a message.
Figure 1 illustrates a number of sample interaction models. States are depicted by circles and the transitions by arrows. The initial state is targeted by an arrow without source state and the nal state is denoted by a double-circle.
Figure 1(a) shows the example described in the introduction. It is not possible to nd interacting roles that exactly show the speci ed behavior. Nevertheless, it would be possible to nd interacting roles that show a subset of the speci ed behavior: Imagine two roles A and B that interact and roles C and D simply do nothing. In this case, however, a conversation would not terminate properly, as the nal state cannot be reached.
Figure 1(b) shows a choice between two interactions. Similarly to the previous example, A and B cannot know whether C and D have already interacted and vice versa. In contrast to the previous example, we can nd roles that collectively realize a subset of the speci ed behavior with proper termination. Imagine again that only roles A and B interact while C and D do nothing. However, we are not able to nd a set of roles that realize a subset of the behavior where all interactions from the conversation model are reachable.
Similarly to the rst example, the enablement dependency between the AB interaction and the CD interaction is the problem in Figure 1(c). As a solution, C could wait for the message from B before interacting with D. That way, the resulting behavior would be a properly terminating subset of the initially speci ed behavior.
Figure 1(d) shows an example containing a non-deterministic choice. This conversation model represents that A should internally be able to decide whether B will interact with C later on. However, B cannot observe this decision as in any case it will get a message x from A. As A does not have any control over the BC interaction, the decision whether this interaction takes place or not will be independent form A's initial choice. When only considering the possible traces of the conversation model we can easily create roles that collectively produce exactly the same traces. The main di erence is that B or C can decide whether the nal interaction takes place or not in the realization. We see that considering the branching structure is crucial whenever the ownership of (and the moment of) choices is of importance. It might be argued that local choices are irrelevant in choreographies. This might be true if choreographies are considered to be a collection of mere interaction sequences. However, from a business perspective it makes a major di erence who makes a branching decision. Therefore, this should be re ected in the formal model as well.
Figure 1(e) shows a cyclic example containing a choice between an AB interaction and a CD interaction, similarly to the second example. The di erence here is that by expanding the cycle to a sequence, we can at least nd roles that realize a subset of the behavior.
Finally, Figure 1(f) shows an example that is perfectly realizable in a synchronous world, where C can block B until it has interacted with A. However, when considering an asynchronous world, where message sending and receiving do not happen in one step, the order of the send activities would not conform to the order of interactions in the conversation model. 3
The examples from the previous section show that we need to distinguish di erent dimensions of realizability. The following three dimensions apply. Complete behavior vs. subset of behavior. Choreographies de ne constraints and obligations of the roles involved. Constraints apply as the choreography enumerates all allowed interactions in every conversation state, obligations apply as a nal state must be reached which is only possible through the execution of the given interactions.
In this context, we can either demand that it must be possible to carry out the complete behavior speci ed in the choreography. Or, a subset of the behavior might already be su cient. Here, the follow-up question is what a valid subset would be. For instance, proper termination of conversations might be a basic criterion. Furthermore, reachability of all interactions from the original choreography might also be demanded.
Communication model. Synchronous communication could be assumed, where sending and receiving of messages must happen at the same time. Two avors are possible in this context: it might be allowed that a sender blocks until the receiver is ready to receive the message. Alternatively, the conversation fails if a role can only send in a given state without any other role being able to receive the message.
In asynchronous settings, message send and receive do not happen in one step. Here, message bu ers are introduced for storing the incoming messages. We might assume that there is only one queue, e.g. with FIFO message delivery, or that there is a bu er where any incoming message can be received from.
The order of interactions is of central importance. However, especially in the case of asynchronous communication, there are di erent options of what ordering relationships to consider. For instance, only the ordering of send transitions might be considered, or the ordering of receive transitions or the ordering of communication transitions within the individual roles might be of importance. Equivalence notion. Having agreed on what ordering relationships to consider, it is important to choose an equivalence notion for comparing the original choreography and the collective behavior of the roles. Here, trace-based techniques can be applied. This is su cient when dealing with deterministic behavior in the choreography and the roles. Branching structures are of relevance in the presence of non-determinism. Here, bisimulation-like techniques can be used.
In order to formally capture the di erent notions of realizability we need to introduce the following concepts. C denotes the set of all choreographies (also with silent transitions). R denotes the set of all role behavior models.
: }(R) ! C is a function that composes a choreography out of a set of role behavior models. C C is a binary relation on choreographies.
Please note that heavily depends on the communication model chosen and, in the case of asynchronous communication, the ordering relationships to be considered. In the special case of considering the order of communication transitions within a role, depends on the role under investigation. depends on whether the complete or only a subset of the behavior is demanded and it also depends on the equivalence notion chosen.
De nition 1 (Realizability). A choreography c 2 C is realizable, i there exists a set of roles r1; : : : ; rn 2 R such that (r1; : : : ; rn) c. 4
Realizability checking for conversation models was presented in [
The notion of local enforceability was rst introduced in [
The notion of desynchronizability investigates whether a choreography that
is realizable under the assumption of synchronous communication properly
terminates under the assumption of asynchronous communication (with one bu er
per message type) [
Similarly to the approaches in [
As we want to preserve the branching structure we carefully need to consider
the observability of choices within each role. We construct the role behavior for
a role r in a similar way like in the operating guidelines approach [
The nodes and their connections are the resulting role projection cr for r. The initial node n becomes the initial state of cr and all nodes containing nal states become nal states of cr. Figures 2(a) and 2(b) illustrate this for roles B and C and the conversation model from Figure 1(d).
An exception to rule (c) applies to all those cases where several transitions with the same label originate in the same state. In this case, di erent nodes must be identi ed / created. If multiple states belonging to the same node have several transitions with the same label (s; m; r), nodes must be identi ed / created for the di erent combinations. 6
This paper motivated di erent dimensions for realizability and investigated role projection for those realizability notions that are based on bisimulation. Here, the branching structures must be considered carefully in order to cater for the moment of observability of choices. Composition of role projections for di erent communication models was outside of the scope of this paper due to the space restrictions. Also the binary relation for comparing the composition and the original conversation model was not covered.
The work presented in this paper is based on conversation models.
Interaction Petri nets [