Sonia Ben Mokhtar

Jinshan Liu

Nikolaos Georgantas

Val Érie Issarny
email: valerie.issarny@inria.fr

Nikolaos Liu

Georgantas

QoS-aware Dynamic Service Composition in Ambient Intelligence Environments *

Keywords: D.2.12 [Software Engineering]: Interoperability Algorithms, Experimentation Semantic Web services, OWL-S, Web services composition, QoS-awareness, Automata theory

Due to the large success of wireless networks and handheld devices, the ambient intelligence (AmI) paradigm is becoming a reality. One of the most challenging objectives to achieve in AmI environments is to enable a user to perform a task by composing on the fly networked services available at a specific time and place. Towards this goal, we propose a solution based on semantic Web services, and we show how service capabilities described as conversations can be integrated to perform a user task that is also described as a conversation, further meeting the QoS requirements of the user task. Experimental results show that the runtime overhead of our algorithm is reasonable, and further, that QoS-awareness improves its performance.

INTRODUCTION

Ambient Intelligence (AmI) envisions human-centric retrieval and consumption of information, in contrast to the conventional computer-centric approach. Systemically, this is realized as a synergistic combination of intelligent humanmachine interfaces and ubiquitous computing and networking. One of the most challenging issues in AmI environments is to compose user applications by integrating on the fly networked software components that are available at a specific time and place, without any previous knowledge of these components. This would allow a mobile user carrying a handheld device with limited resources, to execute * This research is supported by the European IST AMIGO (investigating AmI systems, to realize the full potential of home networking to improve people's lives) project (IST-004182). potentially complex applications in different AmI environments, benefiting from the richness of each such environment. Building upon semantic Web services (OWL-S), we introduce an approach to the QoS-aware dynamic composition of user tasks from networked services in AmI environments, which are user applications described in the form of a workflow (conversation) realizing a user's goal. This workflow description resides on the user's handheld device and is abstract, that is, it does not refer to any specific service to be integrated. Furthermore, the task description specifies the QoS required by the user. Accordingly, networked services have a description specifying their supported conversation and QoS. We propose a composition algorithm that integrates the networked services' conversations into a task's workflow, further considering QoS. Moreover, our solution introduces an abstraction of OWL-S conversations as finite state automata, and a QoS model.

The remainder of this paper is structured as follows. First, we present our approach of modeling and measuring QoS (Section 2). We then introduce our approach of modeling abstract user tasks and networked services (Section 3) and to the dynamic composition of tasks (Section 4). Further, we describe our prototype implementation and evaluation (Section 5). Finally, we conclude with a summary of our contribution and future work (Section 6).

MODELING AND MEASURING QOS

We introduce a base QoS specification of services that is suitable to AmI environments. Usually, a small number of parameters is sufficient to capture the dominant QoS properties of a system [START_REF] Dijk | ARC: a bottom-up approach to negotiated QoS[END_REF]. Along with the factor of limited resources on mobile devices, we only take into account the most dominant and descriptive dimensions in our base QoS specification, instead of trying to incorporate every possible applicable dimension. However, it can be easily extended with more dimensions, if required by specific services, by supporting the new dimensions in a way similar to the one discussed in this section. Below is the table of dimensions we introduce for specifying non-functional properties of services in AmI environments.

The values of quantitative QoS dimensions can be provided by QoS measurements using available software utilities (e.g., pathchar1 for bandwidth measurement). However, providing values of metrics in service advertisements requires QoS prediction. QoS prediction prior to actual service execution can be carried out based on histories [START_REF] Flinn | Balancing performance, energy, and quality in pervasive computing[END_REF], which has been proved to be accurate and efficient [START_REF] Gurun | NWSLite: a light-weight prediction utility for mobile devices[END_REF].

SEMANTIC WEB SERVICE AND TASK DESCRIPTIONS

Service and Tasks Descriptions

OWL-S is a Web service ontology based on the Ontology Web Language (OWL), used to describe Web services properties and capabilities. This language describes Web services capabilities using three parts : the service profile, the process model and the service grounding. The service profile gives a high level description of a service and its provider, the process model describes the service's behavior as a process and the service grounding specifies the information necessary for service invocation. In our approach, each networked service is described as an OWL-S process model with QoS attributes on each involved atomic process (operation). These attributes are obtained from dynamic QoS measurement as described in section 2. On the other hand, the user task description is given in the form of an abstract OWL-S process with QoS requirements. The main difference between the user task's description and the services' descriptions is that contrary to the atomic processes involved in the services' processes, those involved in the user task process are not bound to any service, since services to be invoked are dynamically discovered. Finally, the non-functional requirements of the user task are expressed in the form of arithmetical constraints (e.g., Availability > 50%) and have to be taken into account during the service composition. Our objective is to allow a user to perform a task on the fly, without any previous knowledge about the networking environment and to guarantee that the task will meet the requested QoS. Existing composition approaches based on OWL-S, use service profiles for matching services' advertised capabilities against users required capabilities, while the process model is used only for dynamic service invocation. However, we argue that the process model contains more information about the service capabilities than the service profile and may lead to a more precise matching. Therefore, in contrast to the approach implied by OWL-S, our matching between the task and the integrated services is based on the process model. Our composition approach is divided in two steps. First, semantic discovery of atomic processes delivers a set of services that provide atomic processes which are semantically equivalent with those of the user task. Second, QoS-aware process integration composes the selected services processes to produce the user task's process.

Modeling OWL-S Processes as finite state automata

Towards dynamic composition of services, we use formal modeling of OWL-S processes as finite state automata as described in [START_REF] Ben Mokhtar | Ad hoc composition of user tasks in pervasive computing environments[END_REF]. This model defines mapping rules for translating an OWL-S process model to a finite state automaton. In this model, automata symbols correspond to the OWL-S atomic processes (the services operations) involved in the OWL-S process and a transition between two states is performed when an atomic process is executed. Each process involved in the OWL-S process model, is mapped to an automaton and linked together with the other automata in order to build the OWL-S process automaton. Both user tasks and networked services are modeled as finite state automata. However, the user task's automaton is complemented with additional information in some of its transitions, i.e., the probability for one transition to be selected. More precisely, a probability value is introduced in the case of a Repeat-While, Repeat-Until and Choice constructs. For the first two constructs (loops), the information added is the probability for the corresponding process to be executed once again. In the case of the Choice control construct, a probability is attached to each possible choice. This information is necessary to estimate the QoS of a composition on the basis of the user's histories. For example, if a composition involves a loop, the QoS of this composition depends on how many times the user will execute this loop. All these probabilities are evaluated based on histories and are updated each time the user task is executed.

In addition to the above probabilities that will be used to estimate the average QoS value of a service composition, some other information is needed to estimate the worst case value of QoS parameters. This information is attached to each loop construct in the task's process and gives the maximum number of times the loop can be carried out during the execution of a user task.

Evaluating the QoS of User Tasks

In our approach, as the task is abstract and does not refer to specific services, we need to extract the QoS formulae corresponding to each QoS metric. These formulae are extracted in advance and stored with the task's description. Then, during the composition, each time an abstract atomic process is replaced with a concrete one, these formulae are used to check the fulfillment of the task's QoS requirements. A number of research efforts propose reduction rules to compute the QoS of a workflow. We use the model in [START_REF] Cardoso | Quality of service for workflows and Web service processes[END_REF] to extract the formula of each QoS dimension, corresponding to the task's automaton structure. In this approach, a mathematical model is used to compute QoS for a given workflow process. More precisely, an algorithm repeatedly applies a set of reduction rules to a workflow until only one atomic node remains. This remaining node contains the QoS formula for each considered metric, corresponding to the workflow under analysis. We apply the reduction rules to OWL-S workflow constructs.

In our case, while evaluating the QoS of a service composition, we provide two estimations for each QoS dimension:

(1) a history-based, probabilistic estimation; and (2) a pessimistic estimation. The former corresponds to an average estimation, while the latter corresponds to a worst case estimation. They are used to satisfy different user requirements, i.e., deterministic or probabilistic. For example, if the user demands a deterministic QoS, our approach compares the requested QoS with the pessimistic estimation of the composite service. If the user requires an average QoS, the latter is compared against the probabilistic estimation.

QOS-AWARE, DYNAMIC TASKS COM-POSITION

The first step towards dynamic composition of user tasks is the semantic service discovery, which aims at selecting a set of services providing atomic processes that are semantically equivalent to the processes requested by the user task. This algorithm compares semantically the atomic processes of the user task with those of the networked services. Our semantic service discovery is based on the matching algorithm proposed by Paolucci et al. in [START_REF] Srinivasan | An efficient algorithm for owl-s based semantic search in UDDI[END_REF]. This algorithm is used to match a requested service with a set of advertised ones. In our case we use this algorithm to match services' operations rather than services' capabilities.

QoS-Aware Process Integration

In this section, we present our QoS-aware process integration algorithm, which integrates the processes of the selected services to reconstruct the process of the target user task. To perform such an integration, we employ the finite state automata model that we have defined earlier. Thus, we consider the automaton representing the user task's process and the automata representing the selected services' processes. In a first stage, we connect the services' automata together to form a global automaton. The next stage is to parse each state of the task's automaton starting with the start state and following the automaton transitions. Simultaneously, a parsing of the global automaton is carried out in order to find for each state of the task's automaton an equivalent state of the global automaton. An equivalence is detected between a task's automaton state and a global automaton state when for each incoming operation of the former there is at least one semantically equivalent incoming operation of the latter. In addition to checking for each state the equivalence between incoming operations, a verification of the conformance to the QoS constraints of the user task is performed. This is done by using the QoS formulae that have been extracted from the task's automaton structure as described in Section 3.3. Thus, we start with the QoS formula for each QoS dimension, in which the QoS values of all operations are initialized with the best value (e.g., latency = 0, availability = 1). Then, each time we examine a service operation, we replace the corresponding best value in the formula of the considered dimension, with the real QoS value of the operation. This allows evaluating the values of all QoS dimensions if the current operation is selected. These values are then compared to the corresponding values required by the user task, and if the constraints are not met, the path in the global automaton that includes this operation is rejected. Figure 1 gives an example of how we evaluate the aggregate QoS during the integration process. In this example, the abstract task automaton (left higher corner), which involves the operations op 1 , op 2 , op 3 , op 4 and op 5 , is going to be matched against the global automaton (right higher corner), which connects together the automata of services S1, S2, S3 and S 4 . These services have been selected after the semantic discovery stage, as their respective processes contain oper-ations that are semantically equivalent with those of the abstract user task. Note that in this figure, for readability purposes, semantically equivalent operations are represented with the same names. The abstract user task has a single QoS requirement, which is Latency < 6. The QoS formula for average latency corresponding to the task's structure is given by: Latency = σ 1 (L 1 +(σ 2 * L 2 +σ 3 * L 3 ))+σ 4 (L 4 +L 5 ), where each Li is the latency corresponding to the abstract operations opi, and σi is the probability for opi to be executed. Initially, the value of each L i is assumed to be equal to 0. While browsing simultaneously the two automata, we can notice that when matching the operation op1 of the user task against the equivalent operations S1.op1 and S2.op1 provided by the services S1 and S2, the latency in these two cases is respectively equal to: 0.8 * (2 + (0.3 * 0 + 0.7 * 0)) + 0.2 * (0 + 0) = 1.6 if S 1 .op 1 is selected, and 0.8 * (3 + (0.3 * 0 + 0.7 * 0)) + 0.2 * (0 + 0) = 2.4 if S 2 .op 1 is selected. In both cases the constraint Latency < 6 is met. Later, when matching the operations op 2 and op 3 of the user task, two paths are possible using the service S 1 alone, or using a composition of S 2 .op 1 and S 4 . However, the first choice gives a latency equal to: 0.8 * (0.3 * 3+0.7 * 7)+0.2 * (0+0) = 6.64 > 6. Thus, this path is rejected, as it does not meet the QoS required by the user task. On the contrary, the second solution is kept. The complete resulting composition, which is a concrete realization of the abstract user task with available services, is shown in the left lower corner of the figure.

The proposed process integration algorithm gives a set of sub-automata from the global automaton that behave like the task's automaton and meet the QoS requirements of the user task. Once the set of possible compositions is given, the last stage is to choose the best among resulting compositions, on the basis of provided QoS. We evaluate every resulting service composition sc with the benefit function as proposed in [START_REF] Liu | Qos-aware service location in mobile ad-hoc networks[END_REF]: Overall Benefit = P n i=1 (d i * w i ), where d i is the value of dimension d for the service composition sc, and wi is the relative importance of the considered dimension. Note that different dimensions are in different units and are therefore normalized as in [START_REF] Liu | Qos-aware service location in mobile ad-hoc networks[END_REF] to be comparable.

After selecting a composition scheme, an executable description of the user task that includes references to existing networked services is generated, and entered into an execution engine that executes this description by invoking the appropriate service operations.

PROTOTYPE IMPLEMENTATION AND EVALUATION

We have developed a prototype for evaluating the performance of our process integration algorithm. Whereas, our semantic service discovery is based on a semantic matching algorithm that have already been implemented and evaluated [START_REF] Srinivasan | An efficient algorithm for owl-s based semantic search in UDDI[END_REF]. We have implemented our prototype in Java, on a Linux platform running on an Intel Pentium 4, 2.80 GHz CPU with 512 MB of memory. The performance of our process integration algorithm depends largely on the complexity of the task and the services candidate to the integration in terms of the number of involved operations. More specifically, the run time overhead of the algorithm is proportional to the number of possible (intermediate) composition paths assessed during the whole execution of the algorithm. We have carried out an experiment for evaluating the impact of the number of operations involved in the task's and the services' processes on the performance of our algorithm. Furthermore, we have evaluated the impact of introducing QoS-awareness. Figure 2 shows the preliminary results of these experiments. In this figure the number of operations of the networked services is fixed to the extreme case equal to 100 semantically equivalent operations, while the task's number of operations is increasing from 1 to 10. Two results are reported in this figure: the performance of our algorithm with and without considering QoS. This figure shows an extreme scenario for our algorithm, as each operation of the user task is matched against 100 operations, and the resulting number of possible compositions is equal to: 100 nb in each case, where nb is the task's number of operations. We can see that even in the extreme case of 100 10 possible compositions our algorithm takes less time than the XML parsing time of services' and task's descriptions. This figure shows also another important result, which is the impact of introducing QoS in our integration algorithm. This impact amounts to a small increase in the XML parsing time, which is due to the addition of XML tags for describing QoS, while at the same time to a considerable decrease of the execution time of our algorithm. This is attributed to the rejection of a number of paths that do not fulfill the QoS requirements of the user task during the integration.

CONCLUSION

The AmI vision foresees that the environment around us is populated with networked, both computing and input/output devices, that provide services. Our objective is to allow a user entering into an AmI environment to perform tasks, abstractly described on his/her device, by integrating on the fly available networked services. Our solution building on semantic Web services offers much more flexibility by enabling semantic matching of interfaces and dynamic integration of services' processes to perform the target user task. Furthermore, the computed service composition provides an estimated QoS that fulfills the initial QoS requirements of a user task. The distinctive feature of our solution is the ability to compose Web services that expose complex behaviors to realize a user task that itself has Algorithm with and without QoS a complex behavior. Existing approaches in process-level matching generally consider that either the services or the task have a simple behavior, thus leading to simple integration solutions. In our case, we assume complex behaviors for both services and task described as OWL-S processes, and we propose a matching algorithm that attempts to integrate the services' processes to realize the user task. In order to deal with such level of complexity, our solution introduces an abstraction of OWL-S processes as finite state automata. A preliminary version of our matching algorithm was presented in [START_REF] Ben Mokhtar | Ad hoc composition of user tasks in pervasive computing environments[END_REF]. The current version of the algorithm, which we have presented in this paper, introduces QoS-awareness, and a prototype implementation and evaluation. We have evaluated the performance of our matching algorithm with and without QoS-awareness. The results show that the proposed algorithm has a reasonable runtime overhead, and that the introduction of QoS constraints improves its performance. Our ongoing research effort includes the integration of the semantic discovery of operations into a scalable service discovery protocol, which is appropriate to AmI environments, optimizing at the same time the semantic matching performed during the discovery.

Figure 1 :

 1 Figure 1: Example of the QoS-aware process integration

Figure 2 :

 2 Figure 2: Performance of the Process Integration Algorithm with and without QoS

Table 1 :

 1 QoS dimensions in our base specification

	Category	Dimension	Definition
	Reliability	Availability	Probability=[0..1]
	Performance	Latency	Service Time (in ms)
		CPU Load	Percentage = [0..1]
	Cost	Memory Bandwidth	Percentage = [0..1] Percentage = [0..1]
		Battery	Percentage = [0..1]
		Confidentiality	Boolean
	Security	Integrity	Boolean
		Non-repudiation	Boolean
		Atomicity	Boolean
	Transaction	Consistency Isolation	Boolean Boolean
		Durability	boolean

http://www.caida.org/tools/utilities/others/pathchar


Ferda Tartanoglu
email: galip-ferda.tartanoglu@inria.fr

Valérie Issarny
email: valerie.issarny@inria.fr

Specifying Web Service Recovery Support with Conversations

Web services offer a number of valuable features towards supporting the development of open distributed systems, built out of the composition of autonomous services.

Nonetheless, the resulting systems must offer a number of non-functional properties and in particular dependabilityrelated ones, for acceptance by users, including effective exploitation in the e-business domain. However, dependability of composite services can only be achieved according to the recovery property of composed Web services. This calls for the rigorous specification of the standard and exceptional behavior of Web services. This paper introduces the WS-RESC conversation language that addresses this issue. In a way similar to existing conversation languages, WS-RESC includes constructs for defining ordering and choices. However, WS-RESC further includes constructs for specifying concurrency since it is an inherent feature of distributed systems, and for specifying timing constraints and recovery properties of conversation since these are key behavioral properties in the context of dependability.

Introduction

Although the modularity and interoperability of the Web services architecture enable complex distributed systems to be easily built by assembling several component services into one composite service, there clearly is a number of research challenges in supporting the thorough development of distributed systems based on Web services. One such challenge relates to the effective usage of Web services in developing business processes, which requires support for composing Web services in a way that guarantees dependability of the resulting composite services. The development of dependable composite services lies in specifying the services' standard and exceptional behavior, as enabled by most composition languages through support for exception handling and possible integration of distributed transaction management [START_REF] Tartanoglu | Dependability in the Web services architecture[END_REF]. The exceptional specification of the composite service is further closely related to the ones of the Web services that are composed since the latter must ultimately perform some recovery actions (e.g., compensation) in the presence of faults.

The exceptional specification of a Web service is in part given by its WSDL interface [START_REF]Web services description language (WSDL), version 1.1[END_REF], which states the exceptions that may be signaled in the form of fault messages. However, the behavior of a Web service is more precisely defined if its specification comes along with the ordering requirements over the service's operations as well as on timing constraints. For example, a Web service may require that a client first authenticate itself using a Login operation, and then, that it calls subsequent operations with at most 15 minutes intervals. It is now well recognized that providing machine-readable specifications of such descriptions, called conversations, is beneficial for at least three reasons. First, it helps in the discovery process where the service requester may search providers that support a given conversation. Second, the specification may be used to check correctness of the implementation, i.e., that the client side implementation is correct with respect to the serverside specification. Finally, such a specification may be used to automate Web service programming, e.g., by providing tools for the automated generation of correct code skeletons [START_REF] Meredith | Contracts and types[END_REF][START_REF] Benatallah | Web service conversation modeling[END_REF]. Moreover, these and further analyses are possible using formal methods provided that an encoding of the conversation to a corresponding formal model is given [START_REF] Meredith | Contracts and types[END_REF][START_REF] Pahl | Ontology support for Web service processes[END_REF]. A typical use of such a formal model may be to verify refinement relationships over conversations through model checking. For example, one can verify that the required conversation at the client-side matches the provided conversation at the server-side, in a way similar to architectural connector matching [START_REF] Allen | A formal basis for architectural connection[END_REF]. Although several propositions for describing Web service conversations exist (e.g., [START_REF] Benatallah | Web service conversation modeling[END_REF][START_REF] Curbero | Business Process Execution Language for Web Services[END_REF][START_REF] Hanson | Conversation-enabled web services for agents and e-business[END_REF][START_REF]Web services choreography description language version 1.0[END_REF][START_REF]Web Service Choreography Interface (WSCI) 1.0, W3C Note[END_REF][START_REF]Web services conversation language (WSCL), version 1.0[END_REF][START_REF] Yi | Process composition of Web services with complex conversation protocols: a colored Petri nets based approach[END_REF]), they provide no or limited support for describing recovery behavior of Web services.

This paper introduces the WS-RESC conversation language that allows the thorough specification of both the standard and exceptional behavior of autonomous, composable Web services, further assisting the development of de-0-7695-2268-8/05/$20.00 (C) 2005 IEEE Proceedings of the 38th Hawaii International Conference on System Sciences -2005 pendable composite services. The language in particular enables the definition of equivalence relationships over conversations with respect to their recovery behavior, which may be exploited for the design of fault-tolerant composite actions. WS-RESC is an XML-based language to be directly used by Web service developers to describe recoveryrelated properties of Web services. In addition, we provide a formal specification of the language through translation into the π-calculus [START_REF] Milner | Communicating and Mobile Systems: The π-Calculus[END_REF] that makes available a large number of tools for reasoning about Web service properties. In particular, it allows the automated analysis of the correct composition of Web services with respect to the services' behavior.

Notions that are introduced are illustrated throughout this paper using some base recovery-related properties, i.e., redundancy, retry-ability, compensability and atomicity. The next section presents our approach to the specification of the recovery behavior of Web services, characterizing in particular the above properties, and introduces the notion of equivalence relationships using transition diagrams to specify them at the conversation level. Section 3 then introduces our conversation language, together with its formal semantics using the π-calculus. Section 4 further exemplifies the use of our language, addressing the specification of the aforementioned recovery properties associated with conversations, and its exploitation for developing dependable composite services. Related work is described in Section 5. Finally, Section 6 summarizes our contribution and sketches perspectives for our research.

Specifying recovery behavior of Web services

Specifying recovery behavior of Web services is central to the development of dependable composite Web services. Recovery properties of the composite service ultimately depend upon the ones offered by the composed services. For example, a composite service may require all the operations of the composed services to be atomic for the duration of all its interactions with them. Alternatively, it may require that a specific operation be retry-able. Such requirements may then be matched against the properties of the individual services, so as to allow, e.g., checking the correctness of the composition with respect to dependability properties, or dynamically retrieving instances of Web services that may actually be composed.

Several approaches exist that specify error recovery properties for individual operations, using meta-data. These approaches enforce participant Web services to describe their supported transactional behavior. Then, a client (the service composer), or a middleware service acting on behalf of a client, may exploit those descriptions for specifying and executing a (open-nested) transaction over a set of Web services whose termination is dictated by the outcomes of the transactional operations invoked on the individual services. Such a concern is particularly addressed in the WSTx [START_REF] Mikalsen | Transactional attitudes: Reliable composition of autonomous Web services[END_REF] and WebTransact [START_REF] Pires | Web, Web-Services, and Database Systems 2002, chapter Building Reliable Web Services Compositions[END_REF] frameworks. However, these approaches are not sufficient for comprehensively expressing the recovery behavior of a service. The error recovery mechanism that is implemented by the client-side (i.e., the composite service) often involves more than one operation to be invoked on the server-side, and specific orders and conditions under which they should be invoked may be required for delivering the target recovery property. In this section, we address how conversations, in addition to specifying how to use the service in terms of dependencies between operations and time constraints, may be used to specify the recovery properties of Web services. In a first step, we present how recovery properties may be expressed using the notion of state equivalence ( § 2.1). Then, we discuss how state equivalence that is based on the knowledge of the systems' internal states may be used in the modeling of systems that exhibit only their potential behavior, leading us to introduce a specific equivalence relation over conversations ( § 2.2).

Recovery-related properties

Achieving fault tolerance of composite Web services through some recovery mechanism (e.g., open-nested transaction, replication) implies support of some base properties (e.g., atomicity, compensability) from individual operations or conversations of the composed services. Most of these properties may be characterized in terms of relationships over values of the individual services' states, an in particular state equivalence (also referred to as final state equivalence).

Redundancy, which is a key fault tolerance technique used in both hardware and software systems, implies having multiple systems that behave similarly. Hence, the redundancy property applies to two system activities (e.g., conversation, operation) if the system's state after the execution of either activity is equivalent to the one after the execution of the other, when both are executed with initial system states that are equivalent.

Retry-ability often involves using idempotent activities, i.e., activities that, when executed several times, give the same result. In other words, an activity is retry-able if the states reached after one or more sequential executions of the activity are equivalent.

Atomicity, is another base recovery property, stating that an activity either successfully executes until completion, or aborts by exceptionally terminating in the same state as the one that held before its execution. The atomicity property is then formally expressed in terms of state equivalences over the activity's pre-and post-states [START_REF] Zarras | A framework for systematic synthesis of transactional middleware[END_REF]. Transactions for long running activities are realized based on the compensation of operations that already committed (i.e., externalized), instead of implementing the atomicity property. We can describe compensation-based transactions using the notion of state equivalence, specifying that the successful compensation of an operation, or of a set of operations, brings the system to a state that is equivalent to either the initial one or another consistent state. Indeed, some committed operations may have effects on parts of the system that cannot be recovered, leading to bring the system to a state that is not equivalent to the one that could be restored under the atomicity property. In this case, the state that is reached should still be a consistent state. Applying compensation operations when several operations are already performed on a Web service may be tricky, if there are dependencies between operations, which implies verifying a number of properties for deciding whether the compensation can be applied. For instance, in [START_REF] Korth | A formal approach to recovery by compensating transactions[END_REF], the authors give a formal definition of compensating transactions based on the equality of histories. The definition makes use of the notion of the commutativity of sequence of operations. Then, different types of compensations are defined based on this notion. Commutativity of operations, or sequence of operations, can be expressed with state equivalence relations.

Recovery properties of conversations

We use labeled transition systems to model conversations, similarly to the UML activity diagram used in WSCL [START_REF]Web services conversation language (WSCL), version 1.0[END_REF]. This approach, contrary to the state-machine modeling as that of [START_REF] Benatallah | Web service conversation modeling[END_REF], has the advantage of relying only on operation names and messages, as they are defined in the service's WSDL document, for the definition of states (or nodes) and labeled transitions. A state then models an operation of the Web service that may potentially be called, and a transitions models the actual call of the operation and gives the next available operations. Transitions are labeled optionally by either the output or fault return messages of the previously called operation. Starting states are defined using a Start state and the end of a conversation is given with an End state. In addition, the Empty state refers to an operation without messages associated with it and that does nothing. The Start, End and Empty states are the only states that do not refer to any Web service operation. Thus, the transition originating from the Start and Empty states may not be labeled, and End is final.

As an illustration, Figure 1 models a conversation specifying that all the interactions with the specific Web service begin with the Login operation. For example, assuming that the Login operation is of type request/response, the conversation starts when the client sends the input message of the Login operation. Then, if the Login operation returns the LoginOut output message, the client is allowed to call the Search operation, as many times as necessary, followed by a Buy operation. The conversation terminates either if the Buy operation returns a Confirmation output message or if the Login operation returns a LoginError fault message. Consider now the conversation depicted in Figure 2. It may be useful for the service's client to know that the internal state of the Web service (which is hidden) is exactly the same after each invocation of the operation modeled by state A, i.e., that the operation is retry-able. The client (or composite Web service) may use this information either to verify if a particular Web service supports retry-ability in case of a failure, or to implement an application-specific forward error recovery handler based on the retry technique.

A B α α *

Figure 2. Retry-ability

Consider further the conversation depicted in Figure 3, which specifies that there are two execution paths for reach-

ing the state D: A α -→ B β -→ D, and A α -→ C γ -→ D.
We can deduce that the operations modeled by B and C are alternative executions, if the system's internal state at node D is the same following either execution path, i.e., if the redundancy property holds over the two activities:

A α -→ B β -→ End, and A α -→ C γ -→ End.
Such a property may then be exploited for implementing, e.g., fault tolerance using recovery blocks.

According to [START_REF] Gaudel | DSoS Conceptual Model[END_REF], there are two different approaches to defining the internal state of a system: (i) the forwardlooking style with which the internal state of a system at a given instant is a notional attribute of the system that is sufficient to determine the system's potential behavior; and (ii) the backward-looking style with which the internal state of a system is the total information explicitly stored (in state variables) by the system up to the given instant. The state equivalence relation used for specifying recoveryrelated properties relies on the equivalence of internal states of systems, as given in the second definition. However, what is typically described in conversation-like languages follows the former definition, i.e., the potential behavior of systems. The system is specifically viewed as a process and represented, in general, with labeled transition systems. Conversation languages are further often tightly coupled with formal methods, such as process calculi like CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] or π-calculus [START_REF] Milner | Communicating and Mobile Systems: The π-Calculus[END_REF]. Using these modeling approaches, the notion of equivalence (referred to as observational equivalence) is expressed in terms of the system's external behavior and verified using bisimulations of processes (e.g., see [START_REF] Sangiorgi | The pi-calculus: A Theory of Mobile Processes[END_REF] for an exhaustive list of different bisimulations for the π-calculus).

Following the above, we introduce an equivalence relationship over conversations, to express the equivalence of system's internal states after the execution of the specified conversations, without making explicit their values, in a way similar to the work of [START_REF] Black | An equational theory for transactions[END_REF]. Our equivalence relation is a binary relation, noted ∼, between two conversations. For two conversations A and B of a Web service W , if A ∼B holds, then the internal state of W after the execution of A is equivalent to that reached after the execution of B, if the initial internal states for both executions are equivalent. Note that the equivalence relation specifies only equivalence over internal states, not behavior. Thus, processes are neither structurally congruent nor observationally equivalent. Our equivalence relation satisfies the following properties:

• Reflexivity: A ∼A • Commutativity: (A ∼B) ⇒ (B ∼A) • Transitivity: ((A ∼B) ∧ (B ∼C)) ⇒ (A ∼C)
The specification of Web services conversations together with the equivalence relationships holding over them support the thorough development of dependable composite Web services, defining the standard and exceptional behavior of the Web services to be composed.

The WS-RESC language for dependability

Following the specification of Web services conversations discussed in the previous section, we introduce the WS-RESC (Web Service REcovery Support Conversation) XML-based language for specifying conversations and related recovery behavior. Conversations are in particular specified in terms of the Web service's offered operations, which are defined in the related WSDL document. Conversations then set the rules of how to use the specific Web service. In a way similar to existing conversation languages, WS-RESC includes constructs for defining ordering (dependency) with conditions on exchanged messages and choices. However, WS-RESC further includes constructs for specifying concurrency since it is an inherent feature of distributed systems, and for specifying timing constraints and conversation equivalences since these are key behavioral properties in the context of dependability. Finally, WS-RESC supports the composition of conversations.

The definition of WS-RESC comes along with its formal specification through translation in the π-calculus, thus allowing for automated reasoning about behavioral matching of Web services using π-calculus tools. Such a support is crucial in assisting the development of dependable composite Web services, since it enables enforcing the correct usage of Web services in the composition process. We use the following notation to denote π-processes, with Exp denoting boolean expressions:

P, Q ::= Processes P |Q Parallel P + Q Choice !P Replication if Exp then P else Q Conditional v(x) Input message v(x) Output message (νx)P Restriction (x is a new name in P) ∅ Null process
We recall that the input process v(x).P is ready to input from channel v, then to run P with the formal parameter x replaced by the actual message, while the output process v(y).P is ready to output message y on channel v, then to run P . The reduction relation, noted →, is further defined over processes, with P → P 1 expressing that P can evolve to process P 1 as a result of an action within P . For instance, we have:

((v(x).P + P )|(v(y).Q + Q )) → P |Q{ x / y },
with Q{ x / y } meaning that x replaces y in Q. In the following, we also use a shorthand notation for input and output messages, denoting the channel and parameter with message names. We further use the following XML notations within examples: the default namespace is the one of the conver-0-7695-2268-8/05/$20.00 (C) 2005 IEEE Proceedings of the 38th Hawaii International Conference on System Sciences -2005 sation specification language, namespace this refers to the document being specified, and ws refers to the WSDL document of the Web service.

States and transitions

A state of a conversation is declared with the state XML element, which has two attributes: (i) name names the state and (ii) operation relates the state to an operation of the Web service. Note that the Web service operation as well as its associated message exchange pattern, i.e., whether it is of type request-response, one-way or solicit-request, etc. is declared in the related WSDL document. Naming states allows their reuse, and dually introducing several states referring to the same operation, with different transition rules, in different parts of the conversation. As an illustration, the example below introduces two states, Login and Search, of the conversation depicted in Figure 1: <state name=''Login'' operation=''ws:Login''/> <state name=''Search'' operation=''ws:Search''/> Transition from a state occurs when the operation that is associated with the state is executed. Destination states then specify the operations that can be subsequently called. Additionally, we may have conditions on transitions, represented as labels on the transitions. Conditions refer to the names of the output and fault messages of the source operation. The transition is only valid if the condition is satisfied, i.e., if the operation returns the given messages. The condition is expressed as an XPath [START_REF]XML Path Language (XPath)[END_REF] expression and may thus be a boolean expression composed of several messages. A transition is specified using the transition XML element, which embeds: the source element that gives the source state (or activity), and the destination element that gives the target state (or activity). The optional condition attribute of the source element is defined for transitions that depend on some output or fault messages. In addition, we use the attributes minOccurs and maxOccurs for the transition element to specify how many times the sequence should be repeated. The special keyword all for a source state is introduced as a shorthand notation for declaring as many transitions as states. As an illustration, the following defines two transitions of the conversation depicted in Figure 1.

Choice

Using XML, non-deterministic exclusive choices are defined by declaring two or more transitions from the same state and with the same condition. This further directly translates into π processes combined with the choice (+) operator, as above. The following example, taken from the conversation of Figure 1, specifies that after the execution of the Search operation, the client is allowed to call either the Search or Buy operation: <transition name=''t1''> <source state=''this:search'' condition=''ws:Item'' /> <destination state=''this:search''/> </transition> <transition name=''t2''> <source state=''this:search'' condition=''ws:Item'' /> <destination state=''this:buy''/> </transition>

Correlation for session management

Since there is not a standard way to manage sessions in Web services, keeping track of Web service instances is usually managed by the application. For example, a Web service implementation may use cookies stored at the client side for handling sessions, or may require a session identifier to be associated with interactions. Such information may be used to identify the client, in the case where some operations should be invoked by the same client, as well as to identify a specific Web service instance on the serverside.

We abstractly represent session information using correlations, which serve as identifiers for states. Therefore, when a state has the same correlation value as another, this means that both states are part of the same session. We define correlations with the element correlation. Then, states sharing the same correlation values are identified through the attribute correlate referencing this correlation element, as exemplified below. Correlations are defined in corresponding π processes using parameters. Specifically, (νi)A π (i) is the process A π with the newly defined correlation value i. The correlation value can then be shared with processes within the same session by passing the value in a way similar to input messages.

Activities and nesting

An activity is a connected graph that defines the conversation supported by a Web service. Activities

Figure 4. Activities and composition

As an illustration, Figure 4 depicts an activity with a nested activity Y . Activities are declared using the activity element and nesting is specified through transition with a destination element of type activity, leading to an implicit transition on the Start state of the nested activity. The nested activity may then continue until an End state is reached. Only then, the containing activity may resume, from a transition that has the nested activity as a source destination. Conditions on this transition may be on the output or fault messages of the state preceding the End state in the nested activity. We get the following XML definition for the activity of Figure 4. SearchHotel and SearchFlight. Concurrency is specified using the ∧ symbol on the state-transition diagram. The corresponding XML declaration is given using the concurrent construct and by declaring multiple destination states and/or activities. In addition, the minOccurs and maxOccurs attributes may be specified for the concurrent element, to specify that the destination operations may be called several times in parallel: <transition name=''concurrency''> <source state=''this:Start''/> <concurrent> <destination state=''this:SearchHotel''/> <destination state=''this:SearchFlight''/> </concurrent> </transition> Synchronization of concurrent activities is further specified using a join condition, which is expressed as a boolean expression on basic communication events that specifies under which conditions the execution is allowed to continue. In the activity depicted in Figure 5, the concurrent activities are both required to terminate before invoking the Payment operation. Various conditions can be specified, ranging from the synchronization of all the parallel activities, termination of a subset of the concurrent activities, and no condition at all. In general, the join condition is specified as a boolean expression on the output messages of the last operation of each activity that is joined. Formally, this translates into a conditional π process that is sequentially composed with the concurrent activity, and whose condition is a boolean expression over related output events. The XML representation of the activity depicted in Figure 5 is given below. The corresponding transition specifies the states of all the concurrent activities that are to be joined as source states, and the join condition as an Xpath [START_REF]XML Path Language (XPath)[END_REF]

Figure 6. An activity with timers

Web services may have timing constraints on some of their interactions. For example, a Web service that requires authentication before starting subsequent interactions may impose a delay of at most 15 minutes between successive operations, and enforce re-login upon timeout, as illustrated in Figure 6. A timeout is associated with a transition using the timeout construct. The embedded onInput attribute is set to true if the timeout is computed from upon receipt of an input message by the source operation, or set to false (default) if the timeout is computed from upon emission of the output message. The state attribute further specifies the destination state of the process upon timeout occurrence. <transition> <source state=''this:Login'' condition=''ws:LoginOut''/> <timeout duration=''300'' onInput=false state=''this:Login''/> <destination state=''this:Search''/> </transition> Since there is not a standard way to model timers in the π-calculus, we can abstract from time by using a specific process that is run when the timer timeouts and that can be prefixed by an output event relating to a timeout fault message, if any. A timer sets on a Login operation that returns a TimeOut fault message may then be specified as: Login.(OK.Search π + T imeOut.Login π ). An alternative would be to model the time directly in the calculus, as presented in [START_REF] Berger | The two-phase commitment protocol in an extended pi-calculus[END_REF]. In this paper, the authors extend the πcalculus with a timer denoted by timer t (x(v).P, Q), with t being a positive integer representing time steps, Q the process that is run when the timer timeouts and x(v).P is the continuation process. The latter modeling has the advantage of making time explicit and thus allows reasoning about timing properties of processes. However, there does not yet exist any tool assisting such reasoning. We thus undertake the former approach for modeling timeout in the π-calculus, allowing to benefit from existing tools for the analysis of WS-RESC conversations.

Equivalence

Finally, we introduce the equivalence element to specify equivalence between activities, according to our definition introduced in Section 2.2. We get the following XML notation: <equivalence> <activity name=''this:activityA''/> <activity name=''this:activityB''/> </equivalence>

We recall that the equivalence relationship serves specifying equivalence of internal states and not of behavior. Thus, our definition does not map to any of the equivalence relationships define over π processes. However, two processes can be substituted if they are equivalent according to our definition, when analyzing the behavior of processes from the standpoint of dependability.

Given the process algebra definition of the proposed conversation language, behavioral compatibility of Web service clients (e.g., composite service) with Web services (e.g., composed Web services) may be verified using observational equivalences such as simulation tests between processes. Specifically, the server process must simulate the client process, as discussed in the context of Web services in [START_REF] Pahl | Ontology support for Web service processes[END_REF]. In the general case of composite services, i.e., when a client accesses several Web services, additional verifications may be done for checking safety and liveness properties on the composition process. Furthermore, identifying the appropriate Web service that can take part in a composition that requires a specific recovery protocol to be implemented (e.g., WS-Transaction [START_REF]Web Services Transaction (WS-Transaction)[END_REF]), may be done by: (i) verifying that the Web service may implement the required protocol, i.e., the process defining the protocol simulates the Web service's conversation process, and (ii) checking that required recovery properties hold. Note that the π-calculus formalization of Web services protocols are given in [START_REF] Bhargavan | A semantics for web services authentication[END_REF] for Web services authentication protocols and in [START_REF] Bocchi | A calculus for longrunning transactions[END_REF] for longrunning transactions, which may be conveniently combined with our work.

Specification of error recovery properties

Retry-ability

A retry-able process is defined as a process that behaves similarly when sequentially executed several times, i.e., the process delivers the same results in terms of output or fault message returned to the caller, and the internal states of the Web service after any number of executions are equivalent, at least as can be perceived by the client. It is quite direct to specify this property in terms of activity equivalence. For instance, consider the example we introduced in Section 2 (Figure 2). The corresponding π process is specified as A π ::= msg.(ᾱ.A π + ᾱ.B π ), with msg denoting the call message of the operation associated with A, and ᾱ the output message of the operation associated with A. Consider another conversation that is also supported by the Web service, with the operation associated with A being executed only once (Figure 7), i.e., A π ::= msg.ᾱ.B π . If A π ∼A π , then this implies that a single execution of the operation has the same effect as several executions and thus that the operation is retry-able.

A B α

Compensation

Consider now the activity depicted in Figure 8 and specified as C π ::= msg Buy .ᾱ.Cancel π and Cancel π ::= msg Cancel . β.End π . The equivalence relationship: C π ∼∅, states that the operation Cancel cancels the effects (on the server side) of the operation Buy, provided that the operation Cancel returns an output message, given by the transition β that confirms the correct execution.

Atomicity

Figure 9 illustrates an atomic activity which terminates either successfully by committing performed operations or without completing its task by aborting and rolling back its state. The activity starts with the invocation of the Begin operation and then allows calling several times operations A or B in any order. If any of these operations returns a fault message, the whole activity is aborted on the server side, and the client can no longer continue and may only call the Abort operation to confirm the abortion. Otherwise, the client may call, anytime, either the Commit operation to validate results and finish or the Abort operation to cancel the effects of previous operations. Note that in the first situation, the client calls Abort to confirm (i.e., acknowledge) the abortion that is automatically done at the server-side, and that in the second situation the choice of either aborting or validating is left to the user.

Related works

Various conversation languages have been introduced in the literature, which may be coupled or not with the specification of Web services composition. The former approach is in particular addressed by choreography languages such as WS-CDL [START_REF]Web services choreography description language version 1.0[END_REF]. The latter approach is the most general, as it enables defining reusable autonomous services and does not impose any concrete link to other services nor specific composition processes. Hence, it is more appropriate for defining loosely coupled, reusable services. Relevant conversation languages then include DML [START_REF] Tolksdorf | A dependency markup language for web services[END_REF], WSCL [START_REF]Web services conversation language (WSCL), version 1.0[END_REF][START_REF] Frolund | cl: A language for formally defining web services interactions[END_REF], the framework introduced in [2], the service model description of OWL-S [START_REF]The OWL Services Coalition at the World Wide Web Consortium. Owl-s: Semantic markup for web service[END_REF], Abstract BPEL [START_REF] Curbero | Business Process Execution Language for Web Services[END_REF], WSCI [START_REF]Web Service Choreography Interface (WSCI) 1.0, W3C Note[END_REF] and the conversation specification presented in [START_REF] Yi | Process composition of Web services with complex conversation protocols: a colored Petri nets based approach[END_REF]. However, most conversation languages lack constructs for specifying recovery properties associated with conversations. They only allow exceptional behavior to be described using transitions on fault messages. Hence, except the framework introduced in [START_REF] Benatallah | Web service conversation modeling[END_REF], specification of recovery properties such as transactional behavior of conversations is not addressed. The language introduced in [2] allows specifying transactional behavior of conversations. However, it uses a list of pre-defined transactional properties in a way similar to approaches that annotates individual operations with transactional properties [START_REF] Mikalsen | Transactional attitudes: Reliable composition of autonomous Web services[END_REF][START_REF] Pires | Web, Web-Services, and Database Systems 2002, chapter Building Reliable Web Services Compositions[END_REF], hence reducing the language's expressiveness. Furthermore, existing conversation languages do not address timing issues, except for CS-WS [START_REF] Hanson | Conversation-enabled web services for agents and e-business[END_REF] that introduces an additional timeout attribute associated to operations. Also, it should be possible to specify concurrent activities within conversations, as concurrency allows specifying complex distributed systems involving several participants competing and/or collaborating. However, only workflow-based BPEL [START_REF] Curbero | Business Process Execution Language for Web Services[END_REF] and WSCI [START_REF]Web Service Choreography Interface (WSCI) 1.0, W3C Note[END_REF] address the specification of concurrent abstract processes.

Conclusion

The Web services architecture offers many attractive features for supporting the development of open distributed systems, spanning various application domains such as ebusiness processes but also mobile applications [START_REF] Issarny | Developing ambient intelligence systems: A solution based on web services[END_REF]. However, the development of distributed systems using Web services still raises numerous challenges, in particular related to the enforcement of non-functional properties. Dependability of Web services is in particular a crucial issue since it greatly conditions acceptance of the Web services technology by both service clients and providers. Such an issue has led to tremendous research effort over the last couple of years, as witnessed by, e.g., the introduction of choreography languages integrating support for the specification of recovery actions in the composition process, and of advanced transaction protocols for distributed composite Web services. However, the recovery behavior of composite services ultimately depend upon the recovery properties of the composed services, which require adequate specification of the individual Web services. Such an issue is partly addressed in the definition of the services' WSDL interfaces through fault messages. However, this does not specify complex recovery properties such as compensation of operations, as exploited by advanced transaction models for Web services. Other attempts define the recovery behavior of Web services operations, using meta-data. However, these approaches are not sufficient for comprehensively expressing the recovery behavior of a service. The error recovery mechanism that is implemented by the client-side (i.e., the composite service) often involves more than one operation to be invoked on the server-side, and specific orders and conditions under which they should be invoked may be required for delivering the target recovery property. This then suggests to specify the recovery properties of Web services at the level of conversation. However, existing conversation languages, do not address such a needs, as they primarily focus on the specification of the services' standard behavior.

This paper has introduced the WS-RESC conversation language, which allows the comprehensive specification of Web services standard and exceptional behavior, further assisting the development of dependable composite services. The language in particular enables the definition of equivalence relationships over conversations with respect to their recovery behavior, which may be exploited for the design of fault-tolerant composite actions. Formal specification of the language through translation into the π-calculus additionally allows the automated analysis of the correct composition of Web services with respect to the services' behavior. In order to make such an automated analysis, formal specification of the composition behaviour should also be provided. In future work, we plan to use such a formally described composition language on a real-life application and show how WS-RESC may be used to correctly integrate component Web services.

The conversation and related recovery properties specified in WS-RESC is to be provided as part of the Web service's interface, extending the WSDL description. However, unlike the WSDL document that gives all provided operations, the WS-RESC description may only expose conversations and related properties considered relevant by the Web service designer. Then, conversations and properties related to the actual composition as it is implemented by a client may be obtained by applying composition rules given by the formal definition on conversations specified by the Web service.

0

  -7695-2268-8/05/$20.00 (C) 2005 IEEE Proceedings of the 38th Hawaii International Conference on System Sciences -2005

Figure 1 .

 1 Figure 1. An e-business service conversation

0

  Figure 3. Alternatives

Figure 5 .

 5 Figure 5. An activity with a join conditionConcurrency refers to activities or processes that are allowed to execute concurrently, which directly translates in the π-calculus using the parallel (|) operator. Figure5depicts a conversation where the concurrent transition from the Login state leads to two concurrent sub-activities: SearchHotel and SearchFlight. Concurrency is specified using the ∧ symbol on the state-transition diagram. The corresponding XML declaration is given using the concurrent construct and by declaring multiple destination states and/or activities. In addition, the minOccurs and maxOccurs attributes may be specified for the concurrent element, to specify that the destination operations may be called several times in parallel:

  The WS-RESC language allows precisely characterizing the recovery behavior of Web services, further easing 0-7695-2268-8/05/$20.00 (C) 2005 IEEE Proceedings of the 38th Hawaii International Conference on System Sciences -2005 the development of dependable composite services. This section illustrates usage of our language through examples of common recovery-related properties, i.e., retry-ability ( § 4.1), compensability( § 4.2), and atomicity ( § 4.3).

Figure 7 .

 7 Figure 7. Expressing retry-ability

Figure 8 .

 8 Figure 8. Compensating operations

Figure 9 .

 9 Figure 9. AtomicityLet C be the the activity illustrated in Figure9and C' the sub-activity that always terminate with an Abort and that can be simulated by C. C' may be expressed with the following process:C ::= msg Begin .( b.A + b.B) A ::= msg A .(ᾱ.A + ᾱ.B + ᾱ.Abort + F ault A .Abort) B ::= msg B .(ᾱ.B + ᾱ.A + ᾱ.Abort + F ault B .Abort) Abort ::= msg Abort .ā.EndThe equivalence relation C ∼(msg Begin . b.End) states that the internal state of any activity that starts at the Begin state and ends (after an undetermined number of transitions) at the Abort state, is equivalent to the internal state of the starting state Begin. That means that all of the executed actions are undone.

0

  -7695-2268-8/05/$20.00 (C) 2005 IEEE Proceedings of the 38th Hawaii International Conference on System Sciences -2005

  with in being the input message for the operation associated with A, n the number of output transitions, out i .B i π modeling the transition labeled with message abstracted by out i , and B i π denoting the process associated with the destination state.

	<transition name=''t0''/>
	<source state=''this:start'' />
	<destination state=''this:login''/>
	</transition>
	<transition name=''t2'' >
	<source state=''this:login''
	condition=''ws:LoginOut''/>
	<destination state=''this:search''/>
	</transition>
	A state A and related output transitions directly translate
	into a π process A

π ::= in.((out 1 .B 1 π ) + ... + (out n .B n π ),

  are named and contains at least one Start state and an optional End state. Besides the Start and End states that have no behavior, a state in the graph may define a Web service operation or another activity, which has its own Start and End states.A nested activity has to terminate on an End state to allow the continuation of the main activity. A nested activity is viewed as an isolated execution, thus considered as a single state. Isolation is further enforced by disallowing states to be shared between activities. Activities thus directly translate into π processes, according to rules associated with embedded constructs.

	Start	A	α	Activity Y	β	B	γ	End