This paper discusses Web services synchronization at the composition level. Synchronization aims at assisting independent parties coordinate their actions and thus, avoid conflicts. Our previous work on synchronization primarily focused on the component level and shed the light on two types of behaviors related to specifying Web services. The control behavior defines the business logic that underpins the functioning of a Web service, and the operational behavior regulates the execution progress of this control behavior by stating the actions to carry out and the constraints to put on this progress. Control and operational behaviors continue to be used to specify composite Web services with respect to the orchestration schemas that these composite Web services have to comply with whether centralized or peer-to-peer. As a result, various types of messages to achieve synchronization are developed per type of orchestration schema. Experiments showing the use of these messages are reported in this paper as well.
In [
As the literature review points out [3], it is known that the “beauty” of Web services resides in their capacity to be composed into high-level business processes known as composite Web services. Composition is suitable for users’ requests that cannot be satisfied by any single, available Web service, whereas a composite Web service obtained by combining available Web services might be used. Composition design and development are bound to a specification that describes, at design time, multiple elements such as execution order of component Web services, data dependencies between component Web services, and corrective strategies in case component Web services raise exceptions. At run time, the composition specification is triggered, which means identifying and invoking component Web services, overseeing their execution, coordinating their actions, and initiating corrective strategies if needed. Different specifications related to Web services composition currently exist such as BPEL (de facto standard) and WSCI.
In term of execution, Web services composition can be
structured along two types of orchestration [
This paper extends the synchronization initiative we
report in [
Section 2 discusses the commonalities and differences between the component and composite levels and provides a running scenario. Section 3 reports on the synchronization work that was done at the component level. Section 4 discusses synchronization at the composite level with focus on the P2P schema. Prior to concluding in Section 6, some experimental details are given in Section 5. 2 2.1
In a composition scenario, we classify interactions that involve composite and component Web services into vertical (from composite Web service to component Web service) and horizontal (from component Web service to another component Web service). By establishing an interaction session, the initiator of a message aims at making the recipient of this message behave and take actions according to the content of this message. In the following, we identify the acceptable actions that a message initiator can execute over a potential recipient during vertical and horizontal interactions. The objective of identifying these actions is to facilitate the definition of the relevant synchronization messages that would be suitable per type of interaction.
In vertical interactions, a centralized orchestration of Web services composition is implemented. Here, a composite Web service through the centralized module has the authority to carry out the following actions over a component Web service:
“Invite” action makes the composite Web service request the participation of the component Web service in its composition scenario1;
“Ping” action makes the composite Web service check
the liveness of the component Web service that accepted
1Component Web services invitation is discussed in [
“Trigger” action makes the composite Web service initiate the execution of the component Web service; “Audit” action makes the composite Web service monitor the performance of the component Web service for assessment purposes; service level agreements motivate the audit exercise;
And, “retract&invite” action makes the composite Web service withdraw the component Web service from its composition due to poor performance for example. This yields into searching for another replacement Web service that will be added to this composition.
In horizontal interactions, a P2P orchestration of Web services is implemented. Here, a component Web service has the authority to carry out the following actions over a peer:
“Invite” action makes the component Web service request the participation of the peer in the current composition scenario;
“Ping” action makes the component Web service check the liveness of the peer that accepted its invitation of participation; there is no guarantee that the peer is still part of a composition scenario at time of invocation;
And, “trigger” action makes the component Web service initiate the execution of the peer.
Compared to the vertical interactions in the centralized orchestration, “audit” and “retract” actions are excluded from the horizontal interactions in the P2P orchestration. Essentially, this is due to the challenges that are posed when tracking the performance of Web services and replacing them if needed. Not all providers would like to have their Web services audited by the Web services of other providers for reasons that could be related to security, privacy, competitiveness, etc. In a centralized orchestration, providers do not mutually interact with each other and might not even know that they are parts of the same composition scenario. The absence of “audit” and “retract” actions in a P2P orchestration sheds the light on the necessity of developing appropriate mechanisms that should take into account concerns like privacy and competitiveness. However, these mechanisms do not fall into the scope of this paper. 2.2
Our running scenario concerns a university student who is in the process of organizing a cookout party to celebrate his recent graduation. We identify hereafter the Web services along with their activities that will implement this party’s logistics.
CateringWS: searches for and contacts catering companies according to some criteria like allocated budget, number of expected guests, type of cuisine, etc.
GuestWS: sends invitees invitations, keeps track of confirmed invitations, reminds late invitees for confirmation, etc.
PlaceBookingWS: looks for a place to host the cookout party, books the place, completes the necessary paperwork like payment, etc.
WeatherWS: checks weather forecast for the day of the cookout party. In case of bad weather, the party takes place at the student’s place.
In our initial synchronization project [
The operational behavior guides the execution progress
of the business logic of a Web service. To this end,
this behavior relies on a specific number of states, which
are activated, not-activated, done, aborted,
suspended, and compensated. These states are
reported in the field of transactional Web services [
As mentioned in Section 1, the control and operational behaviors of a Web service are modeled using state charts. This exercise of modeling is hereafter interleaved with some formal definitions and illustrative examples.
Definition 1 (Web Service Behavior). The behavior of a Web service is a 5-tuple B = hS; L; T ; s0; F i where: S is a finite set of state names; s0 2 S is the initial state; F µ S is a set of final states; L is a set of labels; and T µ S £ L £ S is the transition relation. Each transition t = (ssrc; l; stgt) consists of a source state ssrc 2 S, a target state stgt 2 S, and a transition label l 2 L. From now on, we qualify transitions in the behavior of a Web service as intra-behavior. ¤
The control and operational behaviors of a Web service are defined as instances of the behavior of this Web service (Definition 1). These two behaviors are denoted by Bco = hSco; Lco; Tco; sc0o; Fcoi and Bop = hSop; Lop; Top; so0p; Fopi, respectively.
Example 1: Fig. 2 (a) is a state chart of the control behavior of WeatherWS. Several states like city-located (initial state), report-delivered (final state), and search-canceled, and several transitions like (city-located, unavailable, search-canceled) are included in this state chart. In this transition example, city-located and search-canceled are the source and target states, respectively, and unavailable is the transition’s label. Example 2: Fig. 2 (b) is another state chart that illustrates this time the operational behavior of WeatherWS. Similar to the control behavior, several states like not-activated and suspended, and transitions like (compensated, rolling-back, not-activated) and (activated, failure, aborted) are identified in this state chart.
In Fig. 2, the control and operational behaviors of a Web service include different finite sequences that connect states and transitions together. We refer to these sequences as paths and define them as follows: Definition 2 (Path in Web Service Behavior). A path pi!j in the behavior B of a Web service is a finite sequence of states and transitions starting from state si and ending at state sj and is denoted as follows: pi!j = si ¡l!i si+1 ¡li!+1 si+2 : : : sj¡1 ¡lj!¡1 sj such that 8k 2 fi; j ¡ 1g : (sk; lk; sk+1) 2 T (exponents in state names are here given for notational purposes only). ¤ Example 3: Let l1 (resp. l2) = start (resp. l1 commitment) in Fig. 2 (b). not-activated ¡! l2 activated ¡! done is a path in the operational behavior of WeatherWS. 3.2
We pointed out that the operational behavior guides the performance of the control behavior of a Web service. This guidance requires bringing both behaviors together. For instance, done state that a Web service takes on in the operational behavior will in return make this Available City located Access
Unavailable Refinement
Access failed Search canceled Weather Submission collected Web service take on other appropriate counterpart states like weather-collected and report-delivered in the control behavior.
The process of connecting operational and control behaviors together results in establishing conversation sessions between the respective states of these two behaviors (Fig. 3). To complete this connection process, a mapping function is defined as follows: Definition 3 (Mapping Function). Let Pco be the set of all paths in the control behavior of a Web service starting from any state in this behavior. Connecting the operational behavior to the control behavior and vice-versa occurs using the following mapping function: M ap : Sop ! 2Pco , where 2Pco is the power set of Pco. ¤
What the he mapping function M ap does is to associate each state in the operational behavior with a set (possibly empty) of possible paths in the control behavior. Example 4: Fig. 3 is an example of the use of the mapping function in WeatherWS where activated state in the operational behavior is associated with multiple paths in the control behavior. One of these paths is: city-located ¡l!1 weather-collected ¡l!2 report-delivered where l1 = available and l2 = submission. A second path for activated state is given in Fig. 4 (b) as well.
On top of the mapping function Map, interactions between control and operational behaviors require a specification operation that indicates which state in the operational behavior is associated with which set of possible paths in the control behavior along with the “new” transitions that will implement these interactions. The next state to take on in the operational behavior is determined by the executed path in the control behavior and whether this execution was a success or failure. In other words, the specification operation lets the control behavior indicate to the operational behavior what needs to be done next. We define the specification operation as follows: Definition 4 (Specification Operation). Let LS be the set of labels associated with the “new” transitions between operational and control behaviors. The specification operation uses the following two functions: Spec : Sop ! 2LS£Pco£LS and N ext : Sop £ Pco ! Lop £ Sop: ¤
The specification function Spec associates each state sop in the operational behavior with a (possibly empty) set of triples. A triple contains (i) the label of the transition from sop to the first state in the control behavior of a mapped path, (ii) the mapped path itself pi!j , and (iii) the label of the transition from the last state in the control behavior of the mapped path back to sop in the operational behavior. We qualify the “new” transitions that connect states in independent state charts as inter-behavior (note that intrabehavior transition was used in Definition 1). The partial function N ext associates both a given state in the operational behavior and the mapped path in the control behavior with both the next state to take on in the operational behavior and the associated transition label.
Example 5: Fig. 4 shows the synchronization of WeatherWS’s operational and control behaviors where two types of transitions exist: intra-behavior from Tco [ Top (plain lines) and inter-behavior (dashed lines, Labels1;2;3). Fig. 4 contains Spec(activated)=f(label1, path1, label2),(label1, path2, label3)g, N ext(activated,path1)=(commitment,done), weather-collected ¡l!2 report-delivered and N ext(activated,path2)=(failure,aborted) l3 where path2= city-located ¡! access-failed l4 ¡! connection-closed.
In Fig. 4, the initiation of WeatherWS is shown in the operational behavior with activated state. WeatherWS takes on this state following receipt of a user’s request. Because of (activated, label1, city-located) interbehavior transitions, the execution of WeatherWS begins by using a dedicated database to search for the requested city. This makes WeatherWS take on city-located state in the control behavior. Afterwards, two cases are identified.
Case a. Everything goes fine and a 5-day weatherforecast report is delivered back to the user. Because of (report-delivered, label2, activated) interbehavior transition, this makes WeatherWS complete its operation with success by transiting from activated to done states in the operational behavior, i.e., (activated, commitment, done) intra-behavior transition.
Case b. The access to the database fails (not like in case a) as the control behavior of WeatherWS indicates with access-failed and connection-closed states. Because of (connection-closed, label3, activated) inter-behavior transition, this makes WeatherWS terminate its operation with failure by transiting from activated to aborted states in the operational behavior, i.e., (activated, failure, aborted) intrabehavior transition.
To wrap-up this section, the formal definitions of interbehavior and conversation session are provided. Needless to propose a formal definition for intra-behavior transition, which is a regular transition in a state chart (Definition 1). Definition 5 (Inter-Behavior Transition). The set of all inter-behavior transitions that connect the operational and control behaviors of a Web service is denoted by IT where IT = IT op!co [ IT co!op such that: IT op!co µ SIT (op) £ Lop!co £ SIT (co) is the inter-behavior transition relation starting from the operational behavior and ending at the control behavior; IT co!op µ SIT (co) £ Lco!op £
SIT (op) is the inter-behavior transition relation starting from the control behavior and ending at the operational behavior; SIT (op) µ Sop is a finite set of state names in the operational behavior that take part in inter-behavior transitions; SIT (co) µ Sco is a finite set of state names in the control behavior that take part in inter-behavior transitions; and Lop!co is a set of inter-transitions’ labels from the operational to the control behaviors, and Lco!op is a set of inter-transitions’ labels from the control to the operational behaviors (Lco!op [ Lop!co = LS (Definition 4)). ¤
Before we define Web service conversation session, we introduce another function known as Lab. This function returns the label of an inter-behavior transition: Lab : IT ! LS : Definition 6 (Web Service Conversation Session). A conversation session between the operational and control behaviors of a Web service is a 4tuple hsop; itop!co; pco; itco!opi such that: sop 2 Sop; itop!co 2 IT op!co; itco!op 2 IT co!op; pco 2 Pco; and (Lab(itop!co); pco; Lab(itco!op)) 2 Spec(sop). ¤ 4
Synchronization is a mechanism by which independent entities coordinate their next actions by agreeing on how, where, and when to carry out these actions. In the rest of this paper, entities correspond to Web services that could be either component or composite. We look into synchronization from two perspectives: Intra, which means how the operational and control behaviors in a component/composite Web service are coordinated (Section 4.1), and Inter, which means how the operational and control behaviors in separate component Web services are coordinated within the context of the same composite Web service (Section 4.2). Because composition could have either a centralized or a P2P orchestration schema, inter Web-services synchronization is examined from these two types. 4.1
of component Web services was the main object of our
research project in [
of composite Web services is differently handled from the synchronization of component Web services. This is due to the characteristics of composite Web services that need now to be highlighted through their operational and Operational behavior
Control behavior
Control behavior Operational behavior
City located DB
label1 label2
Message name sync success
Description Originates from an operational state and targets a control state. The purpose is to trigger the execution of the control states (including the targeted control state) in a conversation session. sync is a blocking message, which makes the operational state wait for a notification back from the last control state to execute in this conversation session.
Originates from a control state and targets the operational state that submitted sync. The purpose is to inform this operational state of the successful execution of the control states in a conversation session and to return the execution thread back to this operational state as well. success is coupled with sync. control behaviors. These characteristics are as follows.
Firstly, the control behavior represents the business logic of a composition scenario and no longer the business logic of a certain component Web service. Secondly, the current definition of the operational behavior (Definition 1) does not tell much about the execution outcome of a composition scenario and if this execution either succeeded or failed.
This current definition through states like activated and suspended is geared towards the needs of the component level, only (Fig. 2 (b)).
Definition 7 (Composite Web Service Control Behavior).
The control behavior of a composite Web service is a 5
cws = hWSco; Lco; Tco; WSc0o; Fcoi where WSco is tuple Bco a finite set of states that correspond to Web services’ names;
0 WSco ½ WSco is the set of initial states that correspond to initial Web services; Fco µ WSco is the set of final states that correspond to final Web services; Lco is a set of labels; and Tco µ WSco £ Lco £ WSco is the transition relation. Each transition t = (wssrc; l; wstgt) consists of a source Web service wssrc 2 WSco, a target Web service wstgt 2 WSco, and a transition label l 2 Lco. ¤ Example 6: Fig. 1 is a state chart of the control behavior of the CookoutParty composite Web service.
Several states like WeatherWS (initial state) and CateringWS (final state) and several transitions like (WeatherWS, NiceWeather, PlaceBookingWS) are included. In this transition example, WeatherWS and PlaceBookingWS are the source and target states, respectively, and NiceWeather is the transition’s label.
Definition 8 (Composite Web Service Operational Behavior). The operational behavior of a composite Web service is defined as an instance of the behavior of a
cws = Web service (Definition 1) and is denoted by Bop hSop; Lop; Top; so0p; Fopi. ¤
The purpose of the operational behavior of a composite Web service is (i) to initiate the execution of its specification, which is in fact the control behavior of this composite Web service and (ii) to report on the success or failure of the execution of this specification. As a result, the operational behavior of a composite Web service is a subset of the operational behavior of a component Web service.
Example 7: Fig. 5 is another state chart that illustrates this time the operational behavior of the CookoutParty composite Web service. In this state chart, the number of states is limited to four, namely not-activated, activated, done, and aborted, and the number of transitions is limited to three, namely start, commitment, and failure.
Compared to the six states in the operational behavior of a component Web service (Fig. 2 (b)), the four states in the
Aborted operational behavior of a composite Web service (Fig. 5) puts some restrictions on the authorized synchronization messages (like those suggested in Table 1) that can be considered between this operational behavior and its counterpart control behavior. These restrictions are hereafter listed: 1. There is one conversation session between the operational and control behaviors. This session includes the activated state in the operational behavior and all the states (i.e., WSco) in the control behavior. 2. Interaction message of type sync to come out of the activated state in the operational behavior has one recipient, which is the initial state(s) (i.e., Web service) in the control behavior (i.e., WSc0o). 3. Any state (i.e., component Web service) in the control behavior can only submit an interaction message of type fail back to the activated state in the operational behavior. This restriction is waived for the final state(s) in the control behavior (i.e., Fco) that can submit on top of fail message another message of type success back to the activated state in the operational behavior. 4. Interaction message of type syncreq is not allowed
from the control to the operational behaviors. 4.2
Centralized orchestration is well “embraced” in Web
services composition projects. But, a few projects look into
the changes that need to be made in Web services
standards/specifications like BPEL to smooth the design and
development of P2P orchestration. Gowri Nanda et al. note
that because performance and throughput are major
concerns in enterprise applications, removing the
inefficiencies that a centralized control introduces, is required [
In this paper, we look at inter Web-services
synchronization from two perspectives: centralized and P2P (focus of
this paper). This synchronization aims at initiating the
development of composition scenarios and overseeing the
execution progress of this development at run-time. As a result,
this raises the necessity of enhancing Web services with
additional mechanisms based on the needs and requirements
of these composition scenarios. For instance, a Web
service has now to decide if it would or not take part in a
composition scenario subject to carrying out some sort of
self-assessment [
We identify the additional mechanisms that should
embody Web services along four cases, which we denote by
invitation, execution, verification, and replacement. These
four cases abstract the different types of actions that
component and composite Web services carry out during
vertical and horizontal interactions. For example, a Web service
should submit its performance details to a composite Web
service as part of the verification exercise that this
composite Web service carries out. In addition, a Web service
should not leave its ongoing operations pending in case a
composite Web service decides to substitute it as part of the
replacement exercise. These additional mechanisms need
to be woven into the business logic that underpins the
functionality of a Web service. In [
Case of P2P orchestration. The synchronization of inter Web-services in a P2P orchestration reinforces the existence of the component level, only. Each component Web service that takes part in a composition scenario is associated with an operational and a control behaviors (Fig. 6). The previously proposed definitions for these two behaviors continue to be used (Definition 1). However, new definitions are deemed appropriate for first, the inter-behavior transitions between component Web services and second, the conversation sessions that result out of setting-up these inter-behavior transitions. These new definitions have to be inline with the authorized actions to carry out in a P2P orchestration. These actions are “invite”, “trigger”, and “ping”.
In Fig. 6, the double-arrowed lines (plain and dashed) illustrate where the synchronization of inter Web-services should take place in a P2P orchestration. Numbers associated with these lines represent message chronology. In the P2P orchestration we hereafter adopt, sequential execution of the component Web services is assumed even though concurrent execution could be handled without any substanComponent Web servicei
Operational 1 behavior
3 Legend
Control 2 behavior
Component Web servicej tial changes in the new or existing definitions. Plain lines in Fig. 6 represent inter-behavior transitions within the same component Web service (Section 4.1). What is now needed, which is the focus of this part of the paper, is to define the inter-behavior transitions between component Web services. These inter-behavior transitions are represented with dashed lines (3, 6, 7, 8) in Fig. 6.
In a P2P orchestration, the absence of a centralized coordination that would “spread the word” to other component Web services about the execution outcomes of their peers requires some changes in the way these component Web services should behave. For instance, component Web services cannot announce their immediate successful execution until they receive positive feedbacks from their peers in a reverse order. In case of negative feedbacks, these component Web services have to cancel or compensate their execution outcomes and notify their predecessors about the cancelation or compensation actions they have taken, as well. Announcement delay and backward notification have to be reflected on the operational levels of the different component Web services. Like in a centralized orchestration we split done state into two states (Fig. 7): partial done and final done.
² Partial done in a component Web service allows to pass on the execution thread to the next peer(s) (Fig. 6, dashed lines 3 and 6). ² Final done in a component Web service permits to confirm its successful execution (final completion) following receipt of a positive notification from a successor peer (Fig. 6, dashed lines 7 and 8).
Definition 9 (Completion Status of Component Web Service in Peer-to-Peer Orchestration). Let assume a composition scenario of n component Web services. The completion status of a component Web service WSi in term of either success or failure is dependent on the notification message that WSi receives from its direct successor component Web service WSi+1. It is worth to mention that success and failure are conversational messages between component Web services. These messages are specified in Table 2.
Fig. 7 illustrates the different conversation sessions that need to be set-up in a P2P orchestration. The focus is on conversation session #2; conversation session #1 is already discussed in Section 4.1. The identification of the inter-behavior transitions that should be included in conversation scenario #2 takes advantage of the set of acceptable actions (e.g., “invite” and “ping”) that can be carried out between component Web services. These actions are now woven into the synchronization messages to occur between the respective operational behaviors of the component Web services. The following comments are made on the new operational behavior of a component Web service: (i) partial done and final done states are added and connected, (ii) partial done and aborted states are connected, and (iii) partial done and compensated states are connected as well.
Table 2 summarizes some messages that can be exchanged in a P2P orchestration during inter Web-services synchronization. This table is built upon the messages of Table 1. The description of each message type shows (i) the direction of the bidirectional flow between the operational behaviors of the component Web services, and (ii) the case that corresponds to the actions to perform during horizontal interactions. Interesting to discuss messages #9 and #10, i.e., confirm and cancel, respectively in Table 2. Both messages are used by component Web services to notify other component Web services that they could either confirm or cancel their execution.
Definition 10 (Inter-Behavior Transition in Peer-to-Peer Orchestration). The set of all inter-behavior transitions that connect the operational behaviors of component Web services together in a P2P-orchestration mode (conversation session #2 in Fig. 7) is denoted by IT (wsi;wsj) where IT (wsi;wsj) = IT (owp!si;owpsj) [ IT (owp!sjo;wp si) such that: lan ro io iv lteeevn )erSWtreapO eabh l ComFamiliutrmeent CancellatPioanrtial
done
Not activated
Start
Activated Commitment Menu items
Catering delivered IT (owp!si;owpsj) µ SIT (op) £ L(owp!si;owpsj) £ SIT (op) is the interbehavior transition relation starting from the operational behavior of a component Web service (W Si) and ending at the operational behavior of another component Web service (W Sj ). Same definition applies to IT (owp!sjo;wpsi) µ (wsj;wsi) SIT (op) £ Lop!op £ SIT (op); SIT (op) µ Sop is a finite set of state names in the operational behavior of a component Web service that take part in inter-behavior tran(wsi;wsj) is a set of inter-transitions’ labels sitions; and Lop!op from the operational behavior of a component Web service (W Si) to the operational behavior of another compo(wsj;wsi) is the opposite nent Web service (W Sj ), and Lop!op (L(owp!si;owpsj) [ L(owp!sjo;wpsi) = LS ). ¤
To test the viability of the proposed approach, a
prototype system was implemented in Java and integrated under
Eclipse 3.3 by extending the Web service development
platform we developed previously [
The ControlBehaviorModeler and the OperationalBehaviorModeler assist engineers specify the control and operational behaviors of a component or a composite Web service, respectively. In particular, we developed a visual interface for editing Web services’ behaviors using state charts. The ConversationModeler takes the behavior specifications of a Web service as an input to produce conversation specifications (i.e., inter-transitions and message sequences). It implements functions to support conversations between operational and control behaviors. Specifically, it provides methods for managing conversation instances and triggering transitions. When dealing with a peer to peer synchronization, the ConversationModeler manages first, the inter-behavior transitions between component Web services and second, the conversation sessions that result out of setting-up these inter-behavior transitions. Finally, the SimulationController tracks and analyzes (if necessary) the execution of a composite or a component Web service according to its conversation definition (e.g., whether the messages are received and sent in an appropriate order).
Fig. 8 shows the execution of a component Web service in the case of a peer to peer orchestration. Upon the reception of a user’s request, the operational level of the first component Web service (WeatherWS in this case) moves from not-activated state to activated state (red color is used to show the execution path). This latter state, submits a Sync message to Citylocated state in the control behavior to trigger its execution. In a success case, Reportdelivered state returns a Success message back to the activated state in the operational behavior. Based on this information, the operational behavior moves from activated state to partial done state. This latter state sends a trigger message to invoke the next component Web service (CateringWS). 6
We presented in this paper a framework for establishing synchronization between Web services engaged in composition scenarios. Synchronization assists independent parties coordinate their actions and thus, avoid conflicts. This framework extends the research work we carried out on iso# lated Web services (not engaged in any composition) and leverages two types of behaviors related to specifying such Web services. The control behavior defines the business logic that underpins the functioning of a Web service, and the operational behavior regulates the execution progress of this control behavior by stating the actions to carry out and the constraints to put on this progress. Synchronizing Web services through their respective behaviors has revealed that the orchestration schemas, whether centralized or P2P, affect the mechanisms to develop in response to the needs and requirements of the composition scenario that is under consideration. The use of some of these mechanisms per orchestration schema was demonstrated through a prototype. In term of future work, we plan to study the value-add of model checking to the early-detection of design inconsistencies and errors.