< p a r t n e r L i n k n a m e = " c l i e n t " . . . / > < p a r t n e r L i n k n a m e = " h o t e l " . . . / >
Beijing, China
< o p a q u e A c t i v i t y n a m e = " p r e p a r e h o t e l o r d e r " / > < o p a q u e A c t i v i t y n a m e = " p r e p a r e a i r l i n e o r d e r " / > < i n v o k e p a r t n e r L i n k = " h o t e l " oper ati on= "h otel _re que st " inpu tVa ria bl e="# #op aqu e" /> < i n v o k e p a r t n e r L i n k = " a i r l i n e " oper ati on= "f ligh t_r equ es t" inpu tVa ria bl e="# #op aqu e" /> < o p a q u e A c t i v i t y n a m e = " m e r g e o f f e r s " / > < i n v o k e p a r t n e r L i n k = " c l i e n t " oper ati on= "t rave l_o ffe r" inpu tVa ria bl e="# #op aqu e" />
Figure 2: Abstract pro cess describing the observable b ehavior of a travel agency service. do not need to be implemented in two distinct activities. Instead, a single activity (maybe embedded into a loop) should be allowed in a compatible executable completion. · The order in which the reservation requests are sent to the hotel and the airline should be more relaxed. The hotel and the airline do not communicate with each other and therefore cannot realize whether the hotel reservation request is sent before or after the airline reservation request. Thus, any reordering or even a concurrent execution of the invoke activities sending the requests should be allowed if an asynchronous message binding is assumed. · Likewise, a reordering or concurrent execution of the receive activities should be allowed, again assuming an asynchronous message binding. For this and other variations, we will present transformation rules that ensure equivalence of the observable behavior. In Sect. 5, we present their application to the travel agency service.
2.2
Example
As an example, consider the abstract BPEL process of Fig. 2. It describes the abstract process of a travel agency that communicates with three parties: a client service, a hotel service, and an airline service. After receiving a travel request of the client, the travel agency prepares two orders for the hotel and the airline reservation system. As these preparations are highly datadependent and do not affect the observable behavior of the travel agency, these activities are specified opaquely. Then, the respective orders are forwarded to the hotel and the airline partner which return their respective offer. Finally these offers are merged and sent to the client. The APPOB specifies a set of derivable executable completions of this abstract process. Being compatible to the abstract process (i. e., the public view) of the travel agency, they have the same observable behavior in common. The goal of this paper is to introduce a novel abstract profile that extends the APPOB. This profile should extend the set of compatible executable completions and thus make the implementation of the abstract process more flexible. Considering the travel agency service, the following variations should be allowed: · The opaque activities describing the preparations of the orders for the hotel service and the airline service
3. FORMALIZING SERVICE CONFORMANCE
In [2], we proposed an approach for a contract-based composition of services which is based on formal models of services. A formal service model can be generated from a real (BPEL) specification using, for instance, the featurecomplete Petri net semantics [17] for BPEL which is available as an implemented translation from BPEL to Petri nets using the tool BPEL2oWFN [19]. On the level of service models, a strategy of a given finite state service S is another finite state service S with compatible interface such that the composition of S with S forms
787
WWW 2008 / Refereed Track: Web Engineering - Web Service Composition
a deadlock free finite state system. In [20], we show that we can compute a finite representation for the set Strat (S ) of all strategies of a given service S . We call this representation an operating guideline for S as it describes all correct interaction scenarios with S . The computation of an operating guideline is implemented in our tool Fiona [19].1 In the approach of [2], a contract is a set of service models (one for each party involved in the contract) such that their composition is deadlock free. Each of these services is called a public view of one party's contribution to the overall process. The verification of deadlock freedom is indeed feasible as all public views are available to each participating party. In contrast to a public view, a private view is the actual implementation of a party's contribution to the overall system. That is, the composition of the private views forms the implementation of the contract. In order to ensure deadlock freedom of the implementation, we proposed a criterion that relates public and private views of a single party. A private view Pr conforms to a public view Pu (of the same party) if and only if Strat (Pu ) Strat (Pr ). Intuitively, this means that every strategy of the public view must be a strategy of the private view. If all private views conform to their respective public views, we can show that the implementation of a contract inherits deadlock freedom from the contract itself. The actual value of this approach is that conformance between public and private view can be checked local ly by each party (using the concept of operating guidelines mentioned above), thus being able not to disclose trade secrets which might be present in a private view. In our formal model, we assume asynchronous communication (i. e., messages can overtake each other) between the involved parties. Some preliminary considerations on synchronous communication, however, suggest that similar results can be obtained for synchronous, or even a mixture of synchronous and asynchronous communication as well. In [1], we extended this approach with a set of (syntactic) rules for transforming services such that the conformance relation is established between the input of a transformation and the resulting service. This way, a conforming private view can be systematically derived from a public view.
Beijing, China
Observable Behavior (APPGOB). The only difference to the existing profile is that we do not allow adding new partner links as part of the executable completion. Therefore, in a sense, we thereby restrict the set of executable completions. Furthermore, in the BPEL specification, the common base is too restrictive in only allowing replacements of opaque entities and insertions of additional executable entities. There exist a number of cases where the reordering of activities as well as the deletion of activities can be tolerated if these transformations do not affect the main intention of the profile. The APPOB (as well as the more restrictive APPGOB) concentrate on interactions across partner links. Other activities like simple assignments do not need to be handled in such a restrictive fashion. For example, several assignment operations may be independent in the sense that reordering them has no effect on the externally observable behavior of the process. Therefore, we introduce a new relation we call "behavioral equivalence". The purpose of this relation is to extend the set of executable completions to a set of executable processes exposing the same observable behavior. We define our behavioral equivalence relation as follows: Definition 1. Let ep 1 and ep 2 be executable processes. Then ep 1 is behavioral equivalent to ep 2 if and only if ep 1 can be created out of ep 2 by applying zero or more of the following eight transformation rules: 1. 2. 3. 4. 5. 6. 7. I8. Looping Existing Activity Activity Removal from Sequence Activity Removal from Flow Activity Reordering Invoke-Flow Serialization Receive-Flow Serialization Invoke and Receive Communicating If-branches
4. A NOVEL ABSTRACT PROFILE FOR BPEL
Using the formal model introduced above, we are able to formally reason about the behavior of a process. In particular, we are able to define rules that restrict the set of permitted executable completions that are motivated by the semantics of a process instead of its syntax. These rules are less restrictive than the rules of the APPOB and thereby are suitable to extend BPEL's compatibility relation.
n the following, we introduce the above mentioned rules. We distinguish between the first four rules on the one hand as they consider only non-communicating activities and the remaining rules for communicating activities on the other hand. For each rule we present a textual description and an illustrating example by help of a code snippet. On the left hand side of each example the part of the existing BPEL process is shown while on the right hand side the respective part after applying the transformation is illustrated.
4.1.1
Rules for Non-Communicating Activities
We have identified the following four rules for non-communicating activities: Rule 1: Lo oping Existing Activity. Given a sequence of activities, we can embed a present non-communicating activity into a finite (while/repeatUntil/forEach) loop. Example for Rule 1:
4.1
Equivalence Notion for BPEL Processes
The APPOB in BPEL allows adding new partner links and communicating activities using these new partner links. We introduce a variation of the APPOB that preserves the externally observable behavior globally; that is, the set of al l partner links and interactions across these partner links remain invariant. In order to do so, we take the existing APPOB and introduce a new profile, the Abstract Process Profile for Global ly BPEL2oWFN and Fiona are available under http://www.informatik.hu- berlin.de/top/tools4bpel.
1
Although the common base already allows for inserting activities, it does not consider that a present non-communicating activity can be embedded into a loop.
788
operation="a"/> Beijing, China
Rule 2: Activity Removal from Sequence. A noncommunicating basic or structured activity can be deleted from a sequence of activities. Example for Rule 2:
T
a rec n v o eow o f "bceiv Rule 6: Receive-Flow Serializ e activities can be transformed into a se iv e oce. Example for Rule 6:
he common base allows for inserting an activity. That means, we can apply the transformation illustrated in the above example in the other direction as well. However, also removing an activity from a sequence does not change the observable behavior. Rule 3: Activity Removal from Flow. A noncommunicating basic or structured activity can be deleted from a flow. Example for Rule 3:
Rule 6 is the analogous of Rule 5; that is, n receive activities being concurrently executed in a flow can be executed in any sequential order without changing the observable behavior. Rulow>7: Invoke and Receive. eqAnce> uence of first a and then a be way in pe k t on ti a ity rec k o e ctiv ty c / < trimedperatioa=flb"w.> a frece ve o into n " o / sfor Example for Rule 7:
Like for the last rule, the common base only considers activity insertion but not the removal of an non-communicating activity from a flow. Rule 4: Activity Reordering. A sequence of solely non-communicating basic or structured activities can be arbitrarily reordered. Example for Rule 4:
Applying Rule 7 allows to increase the amount of concurrency in the BPEL process without affecting the observable behavior. In case of synchronous binding, a partner has to be the mirrored process, meaning it consists of a sequence of first a receive activity and then a one-way invoke activity. Thus, it will not be affected by the transformation. Otherwise, in case of asynchronous binding, a partner can also consist of a flow embedding a receive activity and a one-way invoke activity which is also not affected by the rule. Rule 8: Communicating If-branches If there is a BPEL process P with an if activity, where each branch starts with an invoke activity and P 's partner process has a pick activity in which each branch corresponds to one of the invoke activities in the if activity, then a branch can be removed from the if activity. Example for Rule 8 (the rule is illustrated on top, below the expected partner is shown):
... ... ...
Since we are allowed to remove and to insert non-communicating activities, we can consequently also reorder noncommunicating activities that are sequentially ordered. It is important to mention that applying these rules must not violate data-dependencies between activities.
Neint owe oipntroiou="e "four < x v ke erat d n c a /> er o c op mu i i n atin / ordactivities. Rule 5: Invoke-Flow Serializationv. kAoflerationo"ae-way invoke activities can be transformeseqiuetoea sequence.
4.1.2
Rules for Communicating Activities
addition
Example for Rule 5:
... ...
7
If n one-way invoke activities are concurrently executed in a flow, then these activities can be executed in any sequential order without changing the observable behavior. Rule 5 reflects the fact that every permutation of the one-way invoke activities is a possible execution sequence due to the concurrency in the flow activity. Informally spoken, applying Rule 5 fixes one of these sequences and hence restricts the behavior of the process.
89
WWW 2008 / Refereed Track: Web Engineering - Web Service Composition
Rule 8 is a little bit more restricted, since it can only be applied if knowledge about the structure of the partner is available. The idea is that since a partner has to be able to receive all sending messages of the corresponding if activity in P , it is still a partner if the number of branches (and therefore the number of invoke activities) in P will be restricted by removing a branch.
Beijing, China
Definition 3. Let ep 1 and ep 2 be executable processes. Then ep 1 is relaxed behavioral equivalent to ep 2 if and only if ep 1 is behavioral equivalent to ep 2 , or ep 1 can be created out of ep 2 by applying zero or more of the following three additional transformation rules: 9. Invoke-Sequence Reordering 10. Receive-Sequence Reordering R1. Invoke and Receive 1 ule 9: Invoke-Sequence Reordering. A sequence of one-way invoke activities can be arbitrarily reordered or it can be transformed into a flow. Example for Rule 9:
4.1.3
A Conformance Notion for WS-BPEL
Considering executable processes that are behavioral equivalent to an executable process belonging to the set of all executable completions for a given abstract process, we can construct the transitive relationship between all equivalent executable processes and the abstract process. Definition 2. Let ap be an abstract process and let ep1 be an executable process, let further EC GOB denote the set of executable completions of ap allowed by the APPGOB. Then ep1 conforms to ap if and only if there exists an executable process ep2 EC GOB such that ep1 and ep2 are beEavioral equivalent. h ach executable process in the set E CGOB of executable completions (cf. Fig. 1) that conforms to an abstract process exposes the same externally observable behavior. Figure 3 illustrates the relationship between an abstract process ap, an executable process ep1 that conforms to ap and an executable process ep2 that is behavioral equivalent to ep1 as it is defined in Def. 2. Therefore, our proposed conformance notion extends the notion of compatibility presented in the BPEL specification, because it allows to relate executable processes ep1 with an abstract process ap if ep1 and ep2 are behavioral equivalent. That way much more executable processes can be related to an abstract process which can be derived by applying the rules we have presented.
abstract process executable process
In case of asynchronous binding it is possible that if a process sends first a message a and then a message b, then its partner process may receive b before a. This is caused by the fact that messages can overtake each other on a message channel. Since a sequence of n send messages can reach the partner in any order, we can arbitrarily reorder a sequence of one-way invoke activities or even embed these activities into a flow. Rule 10: Receive-Sequence Reordering. A sequence of receive activities can be arbitrarily reordered or it can be transformed into a flow. Example for Rule 10:
compatible
For the same arguments as presented for Rule 9, we can arbitrarily reorder a sequence of receive activities or even embed these activities into a flow by applying Rule 10. Rule 11: Invoke and Receive. A flow that contains a one-way invoke activity and a receive activity can be transformed into a sequence of firstly the invoke and then the receive activity. Example for Rule 11:
ap
ep2
behavior equivalent
executable process
conformant
semantic relation syntactic relation
ep1
Figure 3: The relationships b etween compatibility, b ehavioral equivalence, and conformance.
4.2
Relaxed Equivalence Relation for Asynchronous Bindings
The BPEL specification makes no assumptions about protocols, bindings, and quality of service attributes of interactions. So far, all presented transformation rules are valid for both synchronous and asynchronous binding. However, if we would assume asynchronous bindings, we can relax the behavioral equivalence relationship even further by introducing three additional transformation rules. We therefore generalize the relation of behavior-equivalence to relaxed behavioral equivalence.
Ruqee1ce> escribes in fact the op It is the lefdve ope rotion=e b" /ama ence>opss simil b r to ro t he n (
a)
Beijing, China
operation="a"/> e> p equence> onMessage> > de
2. A sequence
crrent execution is disalo i cu
of first then a one way invoke activityNOT be transse US c fo e vers rmrececveo a fl t w, "r ic ed ie> ao < Exa: m v l k or rat ti-ru e 2 ow>
(c)
Figure 4: Counterexamples justifying the ness of Anti-rules 1 and 2.
correct-
Finally, the addition and usage of new partner links is not permitted. This anti-rule differs from the original APPOB where this addition is explicitly allowed. Anti-rule 3. New partner links or communicating activities MUST NOT be added. We discuss the motivation and the validity of the Antirules in the next subsection.
4.4
Discussion
So far, we just listed a set of rules and left the task of verification of their correctness to the reader's intuition. Correctness can, however, as well be formally verified. To this end, it is possible to map the given rules into the formalism of Petri nets using, for instance, the semantics of [17]. It turns out that the resulting Petri net transformation rules correspond to those that have been proven formally correct in [1]. To justify the Anti-rules we show that applying these rules to a process P would exclude a partner of P in the resulting transformed process P . Consider again Anti-rule 1. The process depicted in Fig. 4(a) is a partner for the left pattern in the example of Anti-rule 1, but not for the right pattern. Furthermore, Fig. 4(b) depicts a partner for the right pattern which is no valid partner for the left pattern. Similar for Anti-rule 2, Fig. 4(c) is a partner of the left hand side of the example in Anti-rule 2 but not for the right hand side. In contrast, Fig. 4(d) depicts a valid partner for the right hand side but not for the left hand side of Anti-rule 2. Anti-rule 3 excludes the addition of new partner links and new communicating activities. While this is permitted in the original APPOB and does not affect the observable behavior from one partner's point of view, it would change the global observable behavior by introducing "unintended" behavior. As an example, consider the process depicted in Fig. 5. The original APPOB would allow the addition of a partner link and the two receive activities (the bold lines of Fig. 5). Though this addition would not affect the partner communicating via partner link a, the addition would introduce unintended behavior: A partner communicating via partner link b would have to guess how the condition of the if activity was evaluated to decide whether to send a message
...
Figure 5: Counterexample justifying the correctness of Anti-rule 3.
using operation b1 or b2. Therefore, the process could either deadlock (in case the wrong operation was used) or would complete with a redundant pending message (in case both operations were used). Both cases are certainly not desirable, though not excluded by the APPOB. Summing up, the presented (syntactic) rules are correct, meaning, their application preserves conformance. Correctness has been proven on the level of our formal service model. The presented rules are, however, not complete. In other words, there exist conforming processes that cannot be derived by applying the presented transformation rules. Developing a complete set of conformance-preserving transformation rules seems to be rather laborious, whereas the practical relevance of such a complete set of rules is questionable. There are additional rules not presented in this paper which are rather complicate in the sense that many assumptions have to hold and whose practical applicability is not given. Furthermore, as an alternative to the presented transformation rules, we can check (relaxed) behavioral equivalence between two BPEL processes a-posteriori with our tools BPEL2oWFN/Fiona. Finally, all presented rules are conceptually independent; that is, none of these rules can be derived from other rules.
791
WWW 2008 / Refereed Track: Web Engineering - Web Service Composition
Beijing, China
5.
EXAMPLE REVISITED
The novel abstract profile, APPGOB, now allows the modifications motivated in Sect. 2.2. In particular, the reordering of the communicating activities can now be achieved by applying transformation rules that guarantee observable behavioral equivalence. Figure 6 illustrates the applied transformation rules and their effects. We assume an asynchronous binding for the travel agency service. Firstly, the opaque activities that organize the message sent from or to the agency are replaced by assign activities. Then, those activities that prepare the orders for the hotel and airline reservation system are removed (Rule 2). Instead, a new opaque activity is added and embedded into a while loop (Rule 1). This loop allows more flexibility and an easy integration of additional parties such as, for example, a car rental agency. Then, the invoke activities sending the requests to the hotel and the airline are embedded into a flow activity (Rule 9). Similarly, the responses of the hotel and the airline services are received concurrently (Rule 10). By Definition 3, the derived executable service (cf. Fig. 6(b)) is relaxed behavioral equivalent to the executable process in which only the opaque activities are replaced by assign activities. Furthermore, the executable process derived by applying the transformation rules conforms to the abstract process of the travel agency in Fig. 6(a). Still, this process would not be considered compatible by the original APPOB.
6.
RELATED WORK
There are many other papers dealing with conformance notions. Basten and van der Aalst present in [5] the notion of pro jection inheritance for Petri nets. Two Petri nets are related under pro jection inheritance if they have the same observable behavior. In [1] we have proven that our notion of conformance is a generalization of pro jection inheritance, meaning pro jection inheritance implies conformance. Rules 14 for non-communicating activities presented in Sect. 4.1.1 preserve pro jection inheritance. All other rules influence the communicating behavior and therefore do not preserve pro jection inheritance. Several authors propose conformance notions using process calculi. Castagna et al. [14] formalize the absence of deadlocks and livelocks in finite-state systems. This notion is called strong compliance. In contrast to our conformance notion, strong compliance demands the termination of the environment, but not the termination of the service itself. Bravetti and Zavattaro [10] propose a conformance notion that guarantees the absence of deadlocks, livelocks, and infinite runs in cyclic systems. In [11], their correctness criterion is enhanced by ensuring whenever a message can be sent, the other service is ready to receive this message. Systems that behave this way are called strong compliant. Strong compliance as in [11] seems to be an adequate correctness criterion for BPEL choreographies in case synchronous bindings are used. As a main difference to our conformance notion, [10] and [14] define their notions for synchronous communication and they do not explicitly show how asynchronous message passing can be translated into their calculi although it seems to be possible in general. A more expressive calculi which also supports name passing is used by Carbone at al. [13].
Fournet et al. [16] present stuck-free conformance, a refinement relation between two CCS processes of asynchronous message passing software components. Stuck-freedom formalizes like our notion of deadlock freedom the absence of deadlocks in the system. It can be shown that our conformance notion is more general than stuck-free conformance, because Fournet et al. compare the behavior of two processes N and N whereas we compare the set of strategies for N and N . Busi et al. [12] propose branching bisimulation as a notion of conformance between a choreography language based on WS-CDL and an orchestration language based on abstract BPEL. Conformance can be used to check if the implementation (i. e., the orchestrated system) behaves accordingly the conversation rules of the choreography. Bonchi et al. [8] model the behavior of services using a special kind of Petri nets, Consume-Produce-Read Nets. For their model they present saturated bisimulation as conformance relation. Both branching bisimulation and saturated bisimulation are too restrictive to allow reordering of messages. The concept of contract conformance is also related to deciding when a service can be substituted by another service. Most of this work, however, is restricted to synchronous communication [9, 7, 6] whereas our service model considers asynchronous message passing. Benatallah et al. [6] present four notions of substitutability. In this paper, we cover two of them: equivalence and subsumption. Equivalence in our notion means that both services have the same set of strategies and subsumption means the inclusion of the set of strategies (conformance). Lohmann et al. translate in [18] choreographies specified in the choreography language BPEL4Chor [15] into a Petri net model. This model is then checked for deadlocks using the model checker LoLA [22]. To summarize, most of the work uses a synchronous communication model whereas our model is based on asynchronous message passing thus allowing to identify rules as shown in Sect. 4.3. Furthermore, except the work on pro jection inheritance [5] there are to the best of our knowledge no papers about rules to derive from a service S a service S that conforms to S .
7. CONCLUSION
In this paper, we have presented a more liberal approach to decide compatibility between an abstract and an executable BPEL process. Therefore, we defined a novel profile for BPEL. This profile is not a WS-BPEL language extension. It should be taken as a new profile something that is already allowed by the standard today. This novel profile enhances the existing Abstract Process Profile for Observable Behavior (APPOB) by introducing a notion for behavioral equivalence on the one hand, and restricting it by defining explicit anti-rules on the other hand. We have shown that with our novel profile more executable processes can be considered conformant to an abstract process without the loss of general applicability. Based on our notion of behavioral equivalence we have identified and proven a set of transformation rules. Given an abstract process ap and an executable process ep that is compatible to ap with respect to the APPOB, these rules can be applied to derive an executable process ep that conforms to ap from ep . The set of presented rules is twofold. We have presented transformation rules being applicable
792
WWW 2008 / Refereed Track: Web Engineering - Web Service Composition