Without taking care of the semantics of messages, every message is an isolated entity that can be created and sent at will. This leads to anomalies like a synthesized service that sends a lled form before having received the empty form. In this paper we pick up ideas from adapter synthesis for taking care of semantical constraints and develop them into two directions. First, we show that the approach taken for adapter synthesis can be applied to synthesis of services in general. Second, we argue that the taken approach is in a certain sense complete.
tokens on interface places. We require further that nal markings do not enable any transition (although transition may become enabled by putting tokens on input places). The interface is divided into input and output places and we require that no transition takes tokens from an output place an no transitions puts tokens on an input place.
There exist translations from industrial languages like WS-BPEL into open nets [
Composition may lead to an open net with empty interface which we call closed net.
A closed net is deadlock-free i all markings without enabled transitions are nal. An open net P is controllable i there exists an open net R such that their composition P R is a deadlock-free closed net.
It is just one possibility to use deadlock freedom as the underlying property for controllability. Other requirements could include livelock freedom or any other desired property. Deadlock freedom is, however, the most prominent property discussed in the context of web services. 3
Controllability of an open net P is decidable [
In presence of the mentioned conditions, controllability can be decided by synthesizing (the
state space of) a canonical R as required by the de nition of controllability. The resulting state
space (a kind of automaton) can be transformed into a Petri net using standard approaches [15{
17] and further into languages like WS-BPEL [
The synthesized partner provides a communication skeleton for correct interaction with P and
is thus valuable beyond witnessing controllability. If one desires to invoke P , he can automatically
generate the corresponding code from the description of P . If one does not want to use P
arbitrarily, additional constraints may be applied using the techniques of [
A particular application of this approach is the automated synthesis of an adapter A between two services P and R. If the composition of P and R is not deadlock-free, an intermediate component may mediate the communication between the two and enforce deadlock freedom. Formally, A is a service such that P A R is deadlock-free and can thus be synthesized as a witness for controllability of P R. More precisely, we need to rename interfaces of P and R such that they become disjoint. This way, all communication between P and R will pass A. 4
As we synthesize behavior, we are not necessarily interested in the details of the semantics of exchanged messages as such. We are only interested in the impact of semantics on behavioral issues. Experience from adapter synthesis suggests that the main impact of semantical issues is to constrain the ability of a service to manipulate message contents. The semantics determines own password, simple acknowledgement address electronic message length in feet to length in meters address to name, city, street
Example con foreign password money transfer, transaction number real item (e.g., book) zipcode to length the other way round name, city, street to address
the other way round at reader's discretion whether or not the content of a message can be generated, copied, deleted, or computed from the content of other messages.
In [
Table 1 lists those semantical constraints which have been proposed in the context of adapter synthesis, together with examples where they make sense as well as examples where they don't make sense. The examples show that the applicability of a rule indeed depends on the semantics of the message contents and cannot be inferred from the service protocol. Consequently, we consider a scenario where the constraint speci cation is part of the input to the synthesis problem.
There are various ways to generate a speci cation of semantical constraints. First, they may be generated manually. Since the transformation rules are rather simple, this should not be a problem. Second, they may be inferred using semantic web technology like ontology reasoning. State of the art in this eld is beyond the scope of this note. Third, they may become part of the service construction process using some (may be intra-organizational) modeling standard. 5
Our approach (already exercised in [
In this agenda, the construction of S is obviously the crucial part as all other steps rely on existing technology. Consider some given service P and a set C of semantical constraints ranging on a set E of semantical entities. Let I and O be the sets of input and output places of P .
We assume that I \ O = ; and I [ O E. For simplicity of presentation, we assume that for each rule in S, both sides are sets; the general case follows analogously using Petri nets with arc multiplicities.
For de ning the service S, we use names from the space (E [ C) fe; n; c; r; sg, where e, n, c, r, s denote characters instead of variables; hence we assume that these names do not occur in the given service.
The interface of S consists of output places I, input places O (i.e., the interface of P in opposite orientation), and some input and output places speci ed below. For each entity e : e 2 E, we introduce in service S an internal place (e; c) (c for \copy"). In the initial and nal markings, the internal places are empty, although this can easily be generalized in future work.
Service S has three kinds of transitions. For every input place o : o 2 O, there is a transition (o; r) (r for \receive") to move arriving messages from interface place o to their internal place (o; c). For every transformation rule w : w 2 C, there is a transition (w; c) to perform the actual transformation in terms of the internal places. Finally, for every output place i : i 2 I, there is a transition (i; s) (s for \send") to move messages from their internal place (i; c) to interface place i.
Finally, we discuss the additional interface places for the controller. For every input place o : o 2 O, output place (o; n) (n for \notify") noti es an arrived message o. For every transformation rule w : w 2 C, input place (w; e) (e for enable) enables transformation rule w, and output place (w; n) noti es an execution of w. Finally, for every output place i : i 2 I, input place (i; e) enables the delivery of a message i (once available).
De nition 1 (Service S). Let I; O; E; C be as introduced before. The corresponding service S is de ned as an open net with the following constituents:
P = (E fcg) [ Pi [ Po Pi = O [ (C feg) [ (I feg) Po = I [ (C fng) [ (O fng) T = (O frg) [ (C fcg) [ (I s ) f g F = Fr [ Fc [ Fs Fr = SSo2O f [o; (o; r)]; [(o; r); (o; n)]; [(o; r); (o; c)] g Fc = w=X7!Y 2C ( f[(m; c); (w; c)] j m : m 2 Xg [
f[(w; e); (w; c)]; [(w; c); (w; n)]g [ f[(w; c); (m; c)] j m : m 2 Y g ) Fs = Si2I f [(i; c); (i; s)]; [(i; e); (i; s)]; [(i; s); i] g m0 = 0
= f0g
We use 0 to denote the marking that is zero in every place. By construction, all outputs to P have been obtained from the input of P using the transformation rules only. The actual scheduling of rule applications and message deliveries is left to a controller using the remaining interface.
The inner of S may be unbounded which would complicate further synthesis. For this reason, we pragmatically introduce some capacity on the places of S that, if chosen su ciently large, should not restrict our results unduely.
Having generated S, it remains to synthesize a partner R of P S which can be done using
the approach of [
A WS-BPEL process constructed from R S would contain an opaque activity for each transition, including those that represent the application of transformation rules. In several situations, it is possible to complement the speci cation of semantical constraints with code snippets that actually implement the speci ed transformation. In these cases, we may end up with an executable WS-BPEL process that implements the whole interaction with P and is correct by construction. 6
In the next section, we wish to establish a result of the following kind: Given a service P and a set C of semantical constraints, if there is any R such that R interacts correctly with P and R obeys the semantical constraints, then P S is controllable. A result of that kind is only valuable if the de nition of \to obey the semantical constraints" is as liberal as possible. In this section, we propose such a de nition. For simplicity, we consider only nets where all arc multiplicities are equal to one.
As a starting point, we assume that R has one place for each semantical entity occurring in C. This may be seen as a restriction. Since, however, typical semantical entities are exchanged messages for which there is anyway a representing place, this condition should not be too restrictive. Let PS be the set of places that represent semantical entities. Let FS be the set of edges that have their source or sink node in PS .
The idea of our de nition is to mark the application of transformation rules in the normal control ow of an open net. To this end, we use some in nite set U . Each element of U represents the application of a single rule in C. There may be several elements in U that represent the same rule. Elements of U are assigned to those edges which are connected with PS , i.e. we consider a mapping : FS ! U . This way, access to semantical entities is grouped. u represents a rule X 7! Y i the source places of arcs labeled with u match X, the sink places of arcs labeled u match Y , and each consumption activity causally precedes each production activity. Formally, the rst requirements amount to X = fp j [p; t] 2 FS , ([p; t]) = ug, Y = fp j [t; p] 2 FS , ([p; t]) = ug. Causal precedence is di cult to formalize as we do not want to rule out open nets with cycles. Therefore, we need to separate di erent instances of transitions which contribute to a rule. This leads to the second restriction. We require that, for each u, every run of the inner of R can be divided into sequentially arrangeable parts such that each part contains exactly one occurrence of each transition contributing to u (i.e. there is a p such that ([p; t]) = u or ([t; p]) = u). Within each part, we may now require that ([p; t]) = u and ([t; p]) = u implies that t causally precedes or is equal to t0 which formalizes the idea that consumption precedes production.
We say that R obeys C i a mapping with the discussed properties exists.
It is easy to see that R S as computed in the previous section obeys C. 7
With the de nition of the previous section we are now ready to claim completeness of our approach.
Theorem 1. Consider an open net P and a set C of semantical constraints. If P has a correctly interacting partner that obeys C then P S is controllable where S is the open net constructed from C as described earlier in this note.
For proving this theorem, let R be a correctly interacting partner of P that obeys C. We transform R into a correctly interacting partner of P S using the following ideas. { Rename input places p of R to (p; n) and output places to (p; e). This way, R talks to S instead of P . { For each used u 2 U , introduce new places pu and qu. These places control the invocation of rules.
{ For each [p; t] with ([p; t]) = u, an arc [t; pu]; for each [t; p] with ([t; p]) = u, an arc [qu; t]; { For each u (where c=X 7! Y is the rule represented by u), a transition that consumes jXj tokens from pu and puts one token on (c; e) as well as a transition that consumes one token from (c; n) and puts jY j tokens on qu.
By this construction, a rule is invoked in S after having consumed the corresponding semantical entities in R but before having produced any entity. By our requirements on causal dependencies, the construction does not in uence the behavior of R. Thus, the resulting partner interacts correctly with P S. 8
We have shown that the approach of [