We outline a fundamental approach to behavioral aspects of services. In the center of this approach, we see behavioral models of services, interactions, and nite representations of sets thereof. Several operations and relations can be de ned and their implementation on our representations can be studied. Finally, a number of interesting problems can be traced back to our models and operations. On the boundary of our theory, we place interfaces to other aspects of services.
Services are made for being loosely coupled to larger artifacts. A reasonable coupling (i.e. interaction via message transfer) must take care of various aspects of compatibility, including: { Semantical compatibility: what does the content of exchanged messages mean? { non-functional compatibility: how is the exchange of a message organized? { behavioral compatibility: in which order are messages exchanged? We target the behavioral aspect of compatibility. The remaining aspects are taken care of by a well-de ned interface which enables us to integrate any techniques, approaches, and results regarding semantics or non-functional aspects of service composition. There seem to be two complementary approaches to the speci cation of service behavior. In the rst approach, we specify the control ow of a single service (end point, peer, participant). This control ow implicitly constrains the order of messages that are transmitted via the middleware. In the second approach, we specify sequences of message transmissions which we want to see in the middleware (a choreography). A theory of service behavior should support both points of view.
For the speci cation of single services, we propose to use service automata.
They o er concepts of state and transition for modeling control ow. Transitions
can be labeled with primitives like sending or receiving a message thus
modeling the interaction behavior of a service. Service automata may be compactly
represented as Petri nets or expressions in a process algebra thus inheriting
several results from existing theories. Service automata are well linked to relevant
languages like WS-BPEL or BPMN as there exist back-and-forth translations
between these languages to Petri nets [
For the speci cation of a choreography, we have not yet identi ed a canonical formalism. On one hand, a set of traces of interaction primitives (like sending or receiving a single message) seems to be a more reasonable starting point than process description formalisms like the pi-calculus. The reason is that the middleware that connects services is not an actor which deliberately takes decisions. It is rather a medium that records the e ect of decisions taken elsewhere. On the other hand, some authors insist that it might be essential for a choreography description to record who is in charge for selecting a particular sequence from the space of opportunities given by a set of traces. We conclude that the selection of an appropriate formalism for a theoretical study of choreographies is still a future work task.
In addition to the speci cation of a single behavior, we consider speci cations of sets of behaviors. A meaningful example in the case of single services is an operating guideline, i.e. a nite representation of the set of all compatible partner services to a given service. We believe that many interesting problems can be traced back to simple questions concerning single behaviors or sets of behaviors. 3
Among the important operations on behavior, there are of course a few trivial ones. These include, for example, the composition of services to larger ones or ecxtracting the set of traces in the middleware that can be realized by a given composition of services.
A next class of operations concerns the synthesis of missing components to
an incomplete speci cation. We already have algorithms for the synthesis of
compatible partners to a given services [
In a third class of algorithms, we investigate standard operations on our core objects. As a starting point, we look for realizations of standard set operations (intersection, union, complement, projections) to representations of sets of service behaviors. The actual challenge is that we start with, and want to arrive at, nite representations of in nite sets (where each element is as complex as the control ow of a service). We have some indication, that we will succeed with a minor extension of the structures used for operating guidelines (characterization of the set of all compatible partners of a given service). Further down in this article, we sketch some useful applications.
In a fourth class of operations, we would transform given service behaviors.
Potential applications include the repair of malfunctioning compositions [
Service behaviors need to be compared with each other. A core concept in this regard is the one of equivalence. Several equivalence notions for services have already been proposed. Not all of these notions are very well motivated. For instance, substituting a service with a trace equivalent one may not preserve compatibility with other services. On the other hand, requiring bisimulation equivalence is often too strong a requirement that prevents harmless substitutions.
We believe that reasonable equivalence notions need to be derived from application scenarios. As an example, study a scenario where a service is substituted by another one such that all compatible partners of the old service remain compatible with the new one. The corresponding equivalence holds between all services with the same set of compatibvle partners. It turns out that this equivalence is strongly tied to the process algebraic notion of a should testing equivalence which is a non-trivial entry in the huge zoo of equivalences proposed in process algebra. In future work, we want to identify other application scenarios which may call for di erent notions of equivalence. 4
Of course, the objective of our theory is to provide useful solutions to interesting problems. In this section, we demonstrate that the outlined theory of service behavior yields approaches to a number of interesting problems.
Through the synthesis of a compatible partner [
Due to an already existing link from service automata via Petri nets to abstract
WS-BPEL, we may support the automatic generation of services for various
purposes. These services are compatible by construction. Our theory enables a
exible selection of services to be generated [
Composition may be supported for instance by synthesizing missing components
(adapters) [
Using the right equivalence notions, replacement of services can be done without harming compatibility. Our existing substitutability notion can be traced back to basic set operations as follows. Let OGX be the set of compatible partners of service X. Then P can be exchanged with R i OGP OGR which is equivalent to OGP \ OGR = ;. The remaining emptyness check should be easy. Moreover, a nonempty OGP \ OGR canonically provides examples which prove non-substitutability. Such an example may help in providing diagnostic information and is not available in existing approaches to checking substitutability.
There exist notions of realizability of a choreography. We believe that it is possible to translate the realizability problem into a partner synthesis problem. In the future, we may see more interesting problems concerning choreographies. 5
Most problems and solutions can be formulated in several settings. So far, we have identi ed the following parameters which more or less in uence all approaches stated so far.
There are several reasonable notions of compatibility. The one occurring most frequently is deadlock freedom in the composed system. One may also require that it should always be possible to reach a designated terminal state, or to have a composed system that is sound (as de ned for work ow models). Instead of possible termination one can also require eventual termination. The latter notion requires that the model contains information about fairness of decisions in the control ow. Additional user de nable constraints may parametrize compatibility.
In a canonical setting, message passing is thought of being asynchronous. Existing approaches do or do not allow overtaking of messages. In the literature, synchronous communication is frequently studied, too. Further, we may or may not consider constraints that are implied by the semantics of messages. For instance, semantics may identify message type a as \empty form" and b as \ lled form" which implies that it would not make sense to send b before having received a. Further down, semantical constraints are discussed in more detail.
Many services have interfaces to more than one partner. For synthesizing partners,
we may or may not assume the capability of those partners to be coordinated
during run-time or during build-time. This leads to di erent results concerning
well-formedness [
For being applicable, our solutions must be in line with the remaining aspects of service compatibility. As an example, we sketch an interface to semantics which we already found useful in the context of adapter synthesis.
We already mentioned that the semantics of messages may imply constraints
on the behavior of a synthesized service. Examples of such constraints include
{ Do not send a lled form before having received an empty one (while the
order of unrelated messages does not matter)
{ Do not send a message containing somebody else's password without having
received it in another message (wihle you may send your own password
without having received any message)
We claim that most relevant semantical constraints can be expressed in terms
of transformation rules such as empty form ! lled form, ! own password,
meter ! feet, or street + zipcode + name ! address. The rules specify the
semantically implied e ect of message contents on the behavior, without implying
any particular approach to represent or discover semantics as such. In fact, the
rules may be speci ed manually, synthesized from semantic web approaches, etc.
We already showed that it is possible to trace back synthesis problems in presence
of semantical constraints to plain synthesis problems [
There is already a family of tools which provide some of the discussed functionality: { LoLA for the exploration of state spaces and thus for the investigation of complete compositions; { Fiona for the synthesis of compatible partners and partner sets as well as for the synthesis of adapters, checking compatibility and a few other applications; { BPEL2oWFN and oWFN2BPEL for the translation between WS-BPEL and
Petrio nets; { Rachel for a repair of a malfunctioning choreographies { and certainly a number of tools developed in other groups.
They prove that, to the degree innplemented, operations can indeed be applied to realistic service speci cations. 8
We propose a reasonable set of objects and operations to constitute a theory of service behavior. We have already identi ed a number of interesting problems which all can be traced back to a small number of operations on recurring kinds of objects like sets of service behaviors (also known as operating guidelines). We believe that a further consolidation of the theory would yield additional insights into the nature of services and their composition. Moreover, tracing back many interesting problems to a few operations helps us to strengthen the tool support for a large variety of problem settings.