Julien Ponge

Fabio Casati

Analysis and Applications of Timed Service Protocols

Web services are increasingly gaining acceptance as a framework for facilitating application-to-application interactions within and across enterprises. It is commonly accepted that a service description should include not only the interface, but also the business protocol supported by the service. The present work focuses on the formalization of an important category of protocols that include time-related constraints (called timed protocols), and the impact of time on compatibility and replaceability analysis. We formalized the following timing constraints: C-Invoke constraints define time windows within which a service operation can be invoked while M-Invoke constraints define expirations deadlines. We extended techniques for compatibility and replaceability analysis between timed protocols by using a semantic-preserving mapping between timed protocols and timed automata, leading to the identification of a novel class of timed automata, called protocol timed automata (PTA). Specifically, PTA exhibit a particular kind of silent transitions that strictly increase the expressiveness of the model, yet they are closed under complementation, making every type of compatibility or replaceability analysis decidable. Finally, we implemented our approach in the context of a larger project called ServiceMosaic, a model-driven framework for web service life-cycle management.

Introduction

Service descriptions are specifications of the syntactic or semantic properties of a service that are made available to potential clients for the purpose of (i) assisting developers in creating clients that can correctly use and interact with a service, and (ii) enabling the selection, either at design time or at runtime, of services that match the clients' needs. Today, service descriptions typically include the interface definition, the transport-level properties (both can be specified in WSDL), and may also include business protocol definitions, that is, the specification of the possible message exchange sequences (conversations) that are supported by the service [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF]. Protocols can be specified using BPEL [START_REF]Web Services Business Process Execution Language Version 2[END_REF]) or any of the many other languages developed for this purpose (e.g., [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF][START_REF] Berardi | Automatic composition services: models, techniques and tools[END_REF]).

Providing service descriptions is not in itself sufficient to facilitate development and binding. In addition to descriptions, we need methods and software tools for analyzing service descriptions to (i) identify if interaction between a client and a service is possible; (ii) if it is, identify which conversations can be carried out between two services, to help developers to check if these include all and only the desired ones; (iii) if it is not, understand mismatches between protocols and, if possible, create adapters to allow interactions to occur. We generally refer to this kind of analysis as compatibility/replaceability analysis [START_REF] Mecella | Compatibility of e -services in a cooperative multi-platform environment[END_REF][START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF].

The need for formal methods and software tools for such type of analysis is widely recognized, and many approaches have been developed to this end, including some by the authors. In [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF][START_REF] Benatallah | Analysis and Management of Web Services Protocols[END_REF][START_REF] Benatallah | Representing, analysing and managing web service protocols[END_REF], we presented an approach and a model for business protocols as well as a framework for compatibility analysis. This paper focuses on the important category of protocols that include time-related constraints (called timed protocols in the following). Time is a crucial abstraction that has been studied in several works in research fields such as workflow systems [START_REF] Laurentiu | E-timed workflow nets[END_REF][START_REF] De | An automaton-based approach to the verification of timed workflow schemas[END_REF][START_REF] Bettini | Temporal reasoning in workflow systems[END_REF] and even web services [START_REF] Berardi | Finite state automata as conceptual model for e-services[END_REF][START_REF] Raman Kazhamiakin | Timed modelling and analysis in web service compositions[END_REF][START_REF] Díaz | Automatic generation of correct web services choreographies and orchestrations with model checking techniques[END_REF]. There are countless examples of behaviors that involve timing issues in any kind of protocol [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF], from business protocol for web services (e.g., see the RosettaNet PIPs [START_REF]RosettaNet PIP Directory[END_REF]), to interactions between traditional web-based services and users (see E-Commerce web sites such as Travelocity or Amazon), to lower level protocols such as TCP. Time-related behaviors range from session timeouts to "logical" deadlines with different kinds of behaviors (e.g., seats reserved on a flight needs to be paid within n hours otherwise they are released). Existing approaches in the field of service-oriented computing mainly consider time for performing traditional model checking (e.g., detecting deadlocks).

Given the importance of considering time-related properties, we present concepts and techniques, supported by a tool, for performing compatibility and replaceability analysis between timed protocols. Furthermore, we show how the analysis and the tool can be leveraged to perform the same analysis between BPEL processes or between a BPEL process and a protocol. The availability of such concepts and tools is quite useful in that it allows to assess compatibility and replaceability in both top-down and bottom-up development approaches. In top-down scenarios a client is designed starting from its external interface and protocol, and we are faced with the problem of binding it with a (compatible) service. In bottom-up approaches the development starts from the composition of services (e.g., the BPEL process), and quite often no protocol description is made available as part of the documentation (and if it is made available, we have no guarantee that it correctly describes the message exchanges actually supported by the process). In this case, we are then faced with the problem of verifying if a selected partner service is compatible with our composition, either by looking at the partner's defined protocol, if available, or by looking at the partner's process (again, if available). If none of the above is available then compatibility analysis can only be based on the WSDL interface description and it is necessary limited). Compatibility analysis between processes (composite services) is very useful in integration scenarios within an enterprise where process (e.g., BPEL) specifications are often available. Solving the above problem and supporting these protocol-based analysis scenarios require tackling a number of challenges that we address in this paper. More precisely, the main contributions of this paper are:

• The first step consists in defining a protocol model. We did so in our previous work, and we briefly summarize the results in this paper to make it self-contained. In particular, an informal model for timed protocols has been presented in [START_REF] Benatallah | On temporal abstractions of web service protocols[END_REF], with a first approach being formalized in [START_REF] Benatallah | Compatibility and replaceability analysis for timed web service protocols[END_REF] as a subset of the model that we present in this paper. Here, we revisit and extend concepts and techniques defined earlier for basic protocols to make them applicable to timed protocols. As it is often the case in such tasks, when designing our extended model we were facing a trade-off between expressiveness and complexity / readability of the model. While in general new abstractions may provide benefits, they may also make the model too complex, thereby rendering it unusable for practitioners. To find a reasonable balance between expressiveness and complexity, we conducted an analysis of real world e-commerce portals to identify the service abstractions that are useful and commonly needed in many practical situations [START_REF] Benatallah | Conceptual modeling of web service conversations[END_REF].

• The next step addressed in this paper lies in the extension of the protocol operators (e.g., intersection, difference), needed to handle the compatibility and replaceability analysis, to the context of timed protocols and the investigation of their computational properties. Indeed, the introduction of time aspects adds significant complexity to the problem. Many formal models enabling explicit representation of time exist (e.g., timed automata, timed petri-nets), all showing extreme difficulties to handle algorithmic analysis of timed models [START_REF] Alur | Decision problems for timed automata: A survey[END_REF][START_REF] Girault | Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications[END_REF]. For example, timed automata, which are today one the most used modeling formalism to deal with timing constraints, suffer from undecidability of many problems such as language inclusion and complementation that are fundamental to system analysis and verification tasks. Such problems have been shown to be sensitive to several criteria (e.g., density of the time axis, type of constraints, presence of silent transitions, etc). In this paper we show that the set of protocol manipulation and comparison operators that are essential for realizing protocol analysis are decidable. We show this by establishing a reversible, semantic-preserving mapping to timed automata [START_REF] Alur | A theory of timed automata[END_REF] that, incidentally, identifies a new class that we called protocol timed automata. This class exhibits silent or ε-transitions with clock resets, making it strictly more expressive than general timed automata for which there is no closure under the complementation operator, and hence the language inclusion problem is not decidable. These properties turn out to be the key for realizing the protocol operators. Protocol timed automata are a novel class of timed automata which is closed under complementation and for which the language inclusion problem is decidable, despite the presence of ε-transitions with clock resets.

• We tackle the problem of examining compatibility between processes (and specifically BPEL processes with time-related constructs such as alerts and durations). This is very important as protocol definitions are not always available (even for the services we develop), while BPEL specifications are. Furthermore, BPEL is widely used also as a protocol language and therefore addressing BPEL significantly increases the practical applicability and impact of the research presented here. To this end, we build on top of the protocol analysis operators by devising a mechanism to extract timed protocol specifications from BPEL code and by then using the operators to analyze (in)compatibility between BPEL processes and the services they are supposed to interact with.

• All the features described here have been implemented in a tool as part of a larger project called ServiceMosaic [START_REF] Benatallah | Service mosaic: A model-driven framework for web services life-cycle management[END_REF] which aims at developing a model-driven framework for web service life-cycle management. In addition to process and protocol analysis as discussed here, ServiceMosaic also includes facilities for designing protocols and for discovering protocol models from service execution logs [START_REF] Hamid | Protocol discovery from imperfect service interaction logs[END_REF]. A demonstration featuring the ServiceMosaic tools has been presented in [START_REF] Hamid | Servicemosaic: Interactive analysis and manipulation of service conversations[END_REF]. Preliminary versions of this work that consider restricted forms of timed protocols have been already published in conference papers [START_REF] Benatallah | On temporal abstractions of web service protocols[END_REF][START_REF] Benatallah | Compatibility and replaceability analysis for timed web service protocols[END_REF][START_REF] Ponge | Fine-grained compatibility and replaceability analysis of timed web service protocols[END_REF]. More precisely, [START_REF] Benatallah | On temporal abstractions of web service protocols[END_REF][START_REF] Benatallah | Compatibility and replaceability analysis for timed web service protocols[END_REF] deals with a timed protocol model without C-Invoke constraints and which includes M-Invoke constraints that only refer to the last transition while [START_REF] Ponge | Fine-grained compatibility and replaceability analysis of timed web service protocols[END_REF] considers timed protocol model in which explicit transitions cannot be fired after the expiration of the implicit transitions. This paper extends our previous work in the following directions: (i) it considers a more general timed protocol model without restrictions on the usage of the C-Invoke and M-Invoke constraints. As a consequence, a more in-depth technical analysis is required in order to set up an adequate mapping to timed automata and to prove the closure properties of the operators, (ii) it extends the protocol analysis approach in order to be able to compare BPEL processes or a BPEL process and a protocol and illustrates on a typical usage scenario how the proposed approach works.

The remainder of this paper is organized as follows. Section 2 motivates the need for time-related constraints and introduces both informally and formally the timed protocol model used in this paper. Section 3 extends to the context of timed protocols the approach of protocol compatibility and replaceability analysis as well as the protocol manipulation and comparison operators introduced in [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF]. Sections 4 and 5 contain the main technical contribution of this work. Section 4 describes a semantic-preserving mapping between timed protocols and timed automata and leverages it to prove the main computational properties of the considered timed protocol operators for which we give algorithms in section 5. Section 6 presents our prototype platform and illustrates it on a typical usage scenario related to service development. In particular, this section describes how the presented protocol analysis approach can be applied on BPEL processes. Section 7 discusses some limitations of the proposed approach as well as related work. We conclude in Section 8.

Timed protocol modeling

This section starts by motivating the need of time-related constraints using three examples related to web services and business processes where timing constraints play a critical role: an application, an application integration standard and a web service composition language. Then, it describes the timed protocols model both formally and informally.

• E-Commerce portals. The sales condition notice of many E-Commerce portals provide temporal constraints. Let us consider a classic example of a plane ticket seller portal. A potential purchaser is usually allowed to put a seat on hold for a day or two before a confirmation and payment. In case the buyer does not confirm the purchase after the delay, or if it does not cancel the reservation, the seller will implicitly release the seat holding and cancel the purchase process. There are other examples in the field of E-Commerce. For example goods selling portals are usually entitled by law regulations to allow a buyer to return a purchase within a short delay such as one week after the delivery. Also, they are often constrained to respect delays when dealing with customers for operations such as the deliveries or the refunding of returned purchases.

• RosettaNet PIPs. RosettaNet [START_REF]RosettaNet PIP Directory[END_REF] is an industrial consortium which aims at facilitating the transactions among the supply chains of trading partners. It consists of many specifications called the Partner Interface Processes (PIPs) that represent the processes involved in those transactions. The PIPs have been applied to the production systems of companies such as Intel. The PIPs can be potentially implemented using service-oriented architectures. The PIPs exhibit time-dependent behaviors. For example the PIP 3A4 specifies how a seller and a buyer can process a purchase order. More specifically, it specifies the following timing constraints: (i) the PurchaseOrderRequestAction and the PurchaseOrderConfirmationAction must be acknowledged within 2 hours, and (ii) the reply to the PurchaseOrderRequestAction must be sent within 24 hours.

• BPEL processes. The Business Process Execution Language [START_REF]Web Services Business Process Execution Language Version 2[END_REF] is the major specification in the field of long-running web services orchestrations. BPEL provides several time-related constructions such as the wait activity which causes a given process to "sleep" for a given amount of time or until a date has been reached. The other activity is the use of pick containers for which timers can be defined, for example to trigger a timeout handler if a message has not been received after a given delay, or when a given date has been reached. We propose an extension of the business protocol model [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF][START_REF] Benatallah | Representing, analysing and managing web service protocols[END_REF] which is built upon the traditional state-machine formalism. Indeed, state-based models have been commonly used to model the behavior of systems, due to the fact that they are simple and intuitive. In the model, states represent the different phases that a service may go through during its interaction with a requester. A transition label is a message supported by the service. It has a polarity which is positive (+) if the message is incoming, or negative (-) if it is outgoing. Transitions are triggered when their associated messages are sent or received. Hence, a state identifies a set of outgoing transitions, and therefore a set of possible messages that can be either sent or received when the conversation with a requester is in this state. For example, the protocol depicted on Figure 1 (inspired by the Ford Credit web portal ) is initially in the Start state, and requesters begin a conversation by sending a login message, moving to the Logged state.

Overview of the model

In the figure, the initial state is indicated by an unlabeled entering arrow while final states are double-circled. A conversation is accepted when ending in such a final state. Hence, a sequence of messages login(+) • preApproval(+) • reject(-) is a conversation supported by the protocol, while selectV ehicle(+) • login(+) is not: no transition for a selectV ehicle message is available from the Start state, the two messages cannot be ordered this way, and the conversation does not end in a final state. Business protocols must be deterministic, as the requesters always needs to be able to determine in which state the service is, otherwise much of the purpose of the protocol specification would be lost. We consider the following two extensions to the base protocol model:

1. C-Invoke constraints specify time windows within which a transition can be fired. Outside of those time windows, the transition is disabled, and exchanging the associated message results in an error. 2. M-Invoke constraints specify when a transition is automatically fired.

The obtained model is called timed (business) protocol model. C-Invoke constraints can be attached to explicit transitions for which a message is exchanged between the service provider and its requesters. The absence of C-Invoke constraint on an explicit transition means that it can be fired from its source state at any time. By contrast, M-Invoke constraints are associated to implicit transitions. They model state changes in conversations once a delay has elapsed (a typical example being a timeout). Implicit transitions are analogous to the silent transitions in the automata theory [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF] and we associate the empty word ε as the label of those transitions. However, and unlike usual silent transitions, implicit transitions are mandatorily fired whenever their associated M-Invoke constraints are evaluated to true.

Continuing with the example protocol depicted on Figure 1, it is indicated that a full credit application is accepted only if it is received at most 24 hours after a payment estimation has been made. This behavior is specified by tagging the transition T 14 : fullCredit(+) with a time constraint C-Invoke(T 13 ≤ 24h), i.e., T 14 can only be fired within a time window [0h, 24h] after T 13 has been fired. T 10 has a constraint M-Invoke(T 8 = 30d), meaning that once a pre-approval application has been approved (T 8 ), a requester is given 30 days to select a vehicle (T 9 ). If it does not continue the conversation by sending a selectV ehicle message within the next 30 days, then the service provider will automatically fire T 10 and move to the CreditExpired state, ending the conversation. Finally, it should be noted that the presence of an implicit transition from a given state affects the time constraints of the explicit transitions outgoing from the same state. Indeed, T 10 implies that T 9 can only be fired within a time window matching the 30 days. Hence, a constraint C-Invoke(T 8 < 30d) is implicitly associated with T 9 because of the M-Invoke constraint of T 10 .

Formal model

Syntax

Before giving the definition of timed protocols, we need to formalize the C-Invoke and M-Invoke constraints. Let X be a set of variables referring to transition identifiers: if r is a transition then T r ∈ X is the variable referring to this transition. We consider the two kinds of time constraints defined over a set of variables X using the following grammars:

• C-Invoke(c) with c defined as follows:

c ::= x op k | x -x op k | c ∧ c | c ∨ c
with op ∈ {=, =, <, >, ≤, ≥}, x ∈ X , x ∈ X and k ∈ Q ∪ {⊥}, where Q denotes the set of positive rational numbers, • M-Invoke(c) with c defined as follows:

c ::= (x = k) ∧ c | c ∧ c | c ∨ c with x ∈ X , k ∈ Q ∪ {⊥}
and c being defined like in the grammar of C-Invoke constraints.

The following is the definition for timed business protocols, extending the business protocols model [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF][START_REF] Benatallah | Representing, analysing and managing web service protocols[END_REF]. Definition 2.1. A timed business protocol is a tuple P = (S, s 0 , F, M, X , C, R) where:

• S is a finite set of states, with s 0 ∈ S being the initial state.

• F ⊆ S is the set of final states. If F = ∅, then P is said to be an empty protocol.

• M = M e ∪ {ε} is a finite set of messages M e augmented with the empty message ε. For each message m ∈ M e , we define a function Polarity(P, m) which will be positive (+) if m is an input message in P, and negative (-) if m is an output message in P.

• We assume that each transition r ∈ R is identified by a unique identifier id(r). X = {T i | ∃r ∈ R, T i = id(r)} is a set of clock variables defined over the set of transitions R. • C is a set of time constraints defined over a set of variables X . The absence of a constraint is interpreted as a constraint which always evaluates to true.

• R ⊆ S 2 × M × C is a finite set of transitions. Each transition (s, s , m, c) identifies a source state s, a target state s , a message m and a constraint c. We say that the message m is enabled from a state s. When m = ε, c must be a M-Invoke constraint, otherwise c must be either a C-Invoke constraint or true.

In the sequel, we use the notation R(s, s , m, c) to denote the fact that (s, s , m, c) ∈ R.

To enforce determinism, we require that a protocol has only one initial state, and that for every state s and every two transitions (s, s 1 , m 1 , c 1 ) and (s, s 2 , m 2 , c 2 ) enabled from s, we have either m 1 = m 2 or c 1 ∧ c 2 ≡ false.

Semantics

Before defining the timed protocol semantics, we introduce first the notion of variable valuation.

Variable interpretation

We consider as a time domain the set of positive reals R ≥0 augmented with a special element ⊥ to denote the fact that a transition has never been taken yet. Let X be a set of variables valued in R ≥0 . A variable valuation V : X → R ≥0 ∪ {⊥} is a mapping that assigns to each variable x ∈ X a time value V(x).

We note by V t (x) the valuation of x at an instant t. In the beginning (i.e., at instant t 0 = 0) we assume that all of the variables are set to ⊥, i.e., V t 0 (T i ) =⊥, ∀T i ∈ X . Then, a variable valuation at a time t j is completely determined by a protocol execution. Consider for example an execution σ = s 0 • (m 0 , t 0 ) • s 1 . . . s n-1 .(m n-1 , t n-1 ) • s n of a protocol P. The valuation of a clock variable T i at time t j , with 0 < j ≤ n, is defined as follows:

V t j (T i ) = V t j-1 (T i ) + (t j -t j-1 ) 0 if T i = id(R(s j , s j+1 , m, c)) is fired from s j to s j+1
It should be noted that for any r ∈ R ≥0 , k ∈ Q and any comparison operator op ∈ {<, ≤ , =, =, >, ≥}:

           ⊥ + r = ⊥ ⊥ -r = ⊥ ⊥ op k = false ⊥ op ⊥ = true if op ∈ {=, ≤, ≥} ⊥ op ⊥ = false otherwise
Given a variable valuation V and a constraint C-Invoke(c) (respectively, M-Invoke(c)), we denote by c(V) the constraint obtained by substituting each variable x in c by its value V(x). A variable valuation V satisfies a constraint C-Invoke(c) (respectively, M-Invoke(c)) if and only if c(V) ≡ true. In this case, we write

V |= C-Invoke(c) (respectively, V |= M-Invoke(c))
Timed conversations Timed conversations are inspired from the notion of timed words in timed automata as defined in [START_REF] Alur | A theory of timed automata[END_REF].

Let P = (S, s 0 , F, M, X , C, R) be a timed protocol. A correct execution (or simply, an execution

) of P is a sequence σ = s 0 • (m 0 , t 0 ) • s 1 . . . s n-1 • (m n-1 , t n-1 ) • s n such that: 1. t 0 ≤ t 1 ≤ . . . ≤ t n (i.e.
, the occurrence of times increase monotonically). As usual, we also assume non-Zenoness [START_REF] Alur | A theory of timed automata[END_REF] of the sequences of time (i.e., we cannot have infinite sequences in finite time), 2. s 0 is the initial state and s n is a final state of P, and 3. ∀j ∈ [1, n], we have: R(s j-1 , s j , m j-1 , c j-1 ) and V j-1 |= c j-1 .

As an example, the sequence σ = Start • (login(+), 0) • Logged • (preApproval(+), 1)

• P reApprovalApplication • (approved(-), 3) • CreditApproved • (ε, 33)
• CreditExpired is a correct execution of the financing service protocol depicted on Figure 1.

If σ = s 0 • (m 0 , t 0 ) • s 1 . . . s n-1 • (m n-1 , t n-1 )
• s n is a correct execution of P, then the sequence tr(σ) = (m 0 , t 0 ) . . . (m n-1 , t n-1 ) forms a timed trace which is compliant with P. Continuing with the example, the execution σ of the above service protocol leads to the timed trace tr(σ ) = (login(+), 0) • (preApproval(+), 1) • (approved(-), 3) • (ε, [START_REF] Fu | Analysis of interacting bpel web services[END_REF].

During an execution σ of a protocol P, the externally observable behavior of P, hereafter called timed conversation of P and noted conv(σ), is obtained by removing from the corresponding timed trace tr(σ) all of the non observable events (i.e., all of the pairs (m i , t i ) with m i = ε). For example, during the previous execution σ , the observable behavior of the financing service is described by the timed conversation obs(σ ) = (login(+), 0) • (preApproval(+), 1) • (approved(-), 3).

In the following, given a protocol P, we denote by T races(P) the set of the timed traces which are compliant with P and with T r(P) the set of timed conversations of P.

Timed interactions Timed conversations describe the externally observable behavior of timed protocols and, as we will show below, are essential to analyze the ability of two services to interact correctly. Consider for example the protocol P depicted on Figure 1 and its reversed protocol P obtained by reversing the polarity of the messages (i.e., input messages become outputs and vice-versa).

We can observe that when P interacts with P by following a given timed conversation, P follows exactly a conversation with the reversed polarities of the messages. For example, if during such an interaction the timed conversation of P is (login(+), 0) • (selectV ehicle(+), 1) • (estimateP ayment(+), 10) • (fullCredit(+), 30) • (accept(-), 100), then the timed conversation of P is (login(-), 0) • (selectV ehicle(-), 1) • (estimate-P ayment(-), 10) • (fullCredit(-), 30) • (accept(+), 100).

In this case, we call the path (login, 0) • (selectV ehicle, 1) • (estimateP ayment, 10) • (fullCredit, 30) • (accept, 100) a timed interaction trace of P and P . The polarities of the messages that appear in interaction traces are not defined. Indeed, each input message m of one protocol matches an output message m of the other protocol.

More precisely, let P and P be two timed protocols and let τ = (a 0 , t 0 ) • (. . .) • (a n , t n ) be a sequence of events in which the polarities of the messages are undefined. Then τ is a timed interaction trace of P and P if and only if there exist two timed conversations σ 1 and σ 2 such that:

1. σ 1 ∈ T r(P) and σ 2 ∈ T r(P ), and 2. σ 1 is the reverse conversation of σ 2 (i.e., the conversation obtained from σ 2 by inverting the polarities of the messages), and 3. τ = Unp(σ 1 ) = Unp(σ 2 ) where Unp(σ) denotes the trace obtained from σ by removing the polarities of the messages.

Protocol analysis concepts

Our approach for protocol compatibility and replaceability analysis is based on a set of protocol manipulation and comparison operators that were introduced in [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF]. The proposed operators are build on existing relations and operators defined in the context of timed automata (e.g., language inclusion, intersection, complementation, etc). We briefly recall hereafter both the type of analysis that we target and the operators that we use to do it. We describe the implementation of our operators using already-known constructs on timed automata in Section 5.

Protocol analysis

Compatibility analysis is concerned with verifying whether two services can converse. It is necessary for both static and dynamic binding, and it also aids in managing evolution as it helps verify that a modified client can still interact with a certain service. More precisely, we identified two compatibility classes. Partial compatibility between two protocols P 1 and P 2 implies that at least one conversation can be carried out between two services implementing these protocols. A protocol P 1 is fully compatible with P 2 if P 2 can support all message exchanges that P 1 can generate (the inverse is not required to be true). Ideally, if we have developed a service S characterized by protocol P , at binding time we will want to look for services that have a protocol with which P is fully compatible, so that every message exchange that our service can generate is understood by our partner.

Replaceability analysis identifies whether a service can act as a substitute of another one, either in general or when interacting with certain requesters. Such an analysis involves finding the set of conversations that both services can support even if they are not equivalent. This is useful to determine whether a new version of a service (protocol) can support the same conversations as the previous one or whether a newly defined service can support the conversations that a given standard specification mandates. As in the case of compatibility, we identified several replaceability classes. Protocol equivalence occurs when two protocols support exactly the same conversations. Protocol subsumption occurs when a protocol supports at least all of the conversations of another one. Finally, Protocol replaceability w.r.t. a client protocol occurs when a protocol P 1 can replace a protocol P 2 when interacting with a client protocol P c if every valid conversation between P 2 and P c is also a valid conversation between P 1 and P c . This latter definition is helpful in managing evolution, as when we update our service we may want to check that it can still communicate with the same clients it was interacting before.

We now recall the operators that fully characterize the compatibility and replaceability classes mentioned above and give examples of their usage.

Protocol operators

Operands of the algebra are protocols and operators are special operations defined on protocols that enable, for example, to determine intersection and difference among protocols or to identify which conversations can and cannot be supported when a service is used in place of another one.

Operator name

Symbol Semantics Compatible Composition TC P = P1 TC P2 is a protocol P such that T ∈ T r(P) iff T is an interaction trace of P1 and P2

Intersection TI P = P1 TI P2 is a protocol P such that T r(P) = T r(P1) ∩ T r(P2) Difference TD P = P1 TD P2 is a protocol P that satisfies the following condition: T r(P) = T r(P1) \ T r(P2) Projection ˆTC ˜Let P = P1 TC P2. ˆP1 TC P2 ˜Pi , with i ∈ {1, 2}
, is the protocol obtained from P1 TC P2 by defining the polarity function of the messages as follows: P olarity( ˆP1 TC P2 ˜Pi , m) = P olarity(Pi, m), ∀m ∈ M Table 1: Protocol manipulation operators semantics.

We informally describe the protocol manipulation operators below, while their formal semantics are presented in Table 1.

• Parallel composition, denoted as TC , takes two input timed protocols and returns a timed interaction protocol that captures the possible interactions between them. A timed interaction protocol has simply no messages polarities. More precisely, the resulting timed interaction protocol describes the set of timed interaction traces of the input protocols. • Projection, used to project the polarity of one protocol on the parallel composition of two protocols, is denoted as

P 1 TC P 2 P 1 .
• Intersection, denoted as TI , takes two input timed protocols and returns one timed protocol that captures the timed conversations that they have in common. • Difference, denoted as TD , takes two input timed protocols and returns one that captures the timed conversations that are supported by the first input protocol but not by the second one.

We give examples of operators-based compatibility and replaceability analysis on Figure 2. P 1 and P 2 are only partially compatible, as P 1 TC P 2 P 2 ≡ P 2 . By using the difference operator to compute P 2 TD P 1 TC P 2 P 2 , we get the set of conversations that are supported by P 2 but not by P 1 which yield to a partial compatibility (P 1 does not support receiving a c message after 10 units of time). P 4 can be replaced by P 3 as it supports all of the conversations that P 4 supports, denoted as P 3 P 4 (every valid conversation of P 3 is also a valid conversation of P 4 ). The converse is however not true as illustrated by P 3 TD P 4 : P 3 cannot handle d messages. The formalization of the compatibility and replaceability classes that was introduced in [START_REF] Benatallah | Compatibility and replaceability analysis for timed web service protocols[END_REF] as well as the characterization of these classes using the aforementioned operators remain unchanged in the context of our extended protocol model (see Table 2). However, due to the expressiveness of the timed protocol model used in this paper, the decision problems underlying protocol analysis (e.g., closure properties of the operators, decidability of protocol subsumption) must be investigated in this new context. As described below, we conducted our investigation using a formal framework based on timed automata theory.

From timed protocols to protocol timed automata

The previous sections have introduced the model of timed business protocols which is suitable for describing and analyzing the external behavior of web services in presence of timing constraints. In turn, the model of timed automata [START_REF] Alur | A theory of timed automata[END_REF] has been extensively studied as an extension of classical automata [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF] with real-valued clocks and conditions on the transitions. Given the extensive research that has been made on timed automata, we chose to: (i) use timed protocols as a conceptual model, and (ii) use timed automata for implementing the behavior of timed protocols, and (iii) adapt and/or extend theoretical properties on timed protocols from existing work on timed automata. To achieve this task, we give a mapping from timed protocols to timed automata. However, defining such a mapping is not a trivial task. Indeed, as we will see later, M-Invoke constraints are not straightforward to implement using timed automata.

Note that we do not directly use timed automata for modeling service protocols at the conceptual level as we believe that this will be a difficult and error prone task. The difficulties in defining the semantic-preserving mapping that we will see hereafter as well as the complexity of the obtained timed automata are strong arguments in favor of timed protocols.

This section is structured as follows. We first introduce timed automata and then provide a formal definition of the model used in this paper. Then we illustrate the challenges of converting a timed protocol into a timed automaton that correctly implements its behavior. We describe the technique for performing such a mapping and finally, we give a characterization of the obtained class of timed automata. Timed automata were introduced in [START_REF] Alur | A theory of timed automata[END_REF] as an extension of classical automata [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF] to model real-time systems. We take as an example the timed automaton A depicted on Figure 3. At first sight, A is much like a "normal" automaton: it has locations (e.g., s 0 , s 1 and s 2 ) as well as switches with labels over the alphabet Σ = {a, b}. There is one initial location s 0 while s 2 is an accepting location. Timing constraints are added in A by making use of a clock x which is a continuous variable over the set of real-valued numbers R ≥0 . The automaton A recognizes the set of timed words a•b such that b is recognized at most 5 units of time after a. To do that, the clock x is reset to 0 when the automaton switches from the location s 0 to s 1 on the symbol a. Again, a switch can reset an arbitrary number of clocks. Initially, every clock is set to 0 and then, they grow synchronously as time evolves. Note that, time elapses in the locations, while the switches are instantaneous. Clocks can be used in constraints attached to the switches, called guards, and that can enable or disable a switch depending on how guards are evaluated. Here, the clock x is used in the guard of the b-labeled switch so that b cannot be recognized when (x ≥ 5) is true. More precisely, a timed word over an alphabet Σ is a finite sequence (a 0 , t 0 )

Quick overview on timed automata

• (a 1 , t 1 ) • • • (a n , t n ) of symbols a i ∈ Σ that are paired with nonnegative real numbers t i ∈ R ≥0 such that t 0 ≤ t 1 ≤ • • • ≤ t n . For example w = (a, 0) • (b, 1
) is a timed word where b has been recognized 1 unit of time after a. A timed language over an alphabet Σ is a set of timed word over Σ. Timed automata recognize timed languages. For example, the automaton A of Figure 3 recognizes the time language {(a, t) • (b, t ) | tt < 5}. In the sequel, we denote by L(A) the timed language recognized by a given automaton A.

Over the years, several classes of timed automata with different level of expressiveness have been studied leading to many results regarding the usual verification problems (e.g., reachability, language inclusion, etc) [START_REF] Alur | Decision problems for timed automata: A survey[END_REF]. We present below the timed automata model used in our context.

Target timed automata model

We consider a timed automata model that enables silent transitions, noted hereafter ε and called ε-labeled switches. As usual, a timed automaton is defined using a set of clocks X while the set of clocks constraints over X, noted C(X), is built using boolean combinations of atomic constraints of the form x # c with x ∈ X, # ∈ {=, =, <, ≤, >, ≥} and c ∈ Q. We also allow diagonal constraints of the form (x 1 -x 2 # k) with x 1 , x 2 ∈ X and k ∈ Q∪⊥. Diagonal constraints are known not to increase the expressiveness of the model but allow more representation conciseness [START_REF] Bouyer | Diagonal constraints in timed automata: Forward analysis of timed systems[END_REF].

Definition 4.1. A timed automaton A is a tuple A = (Σ, L, L 0 , L f , X, E) where:
• Σ is a finite alphabet, and denotes the empty word in Σ * , • L is a finite set of locations (or states), with L 0 ∈ L being the initial location,

• L f ⊆ L is the set of final locations (or accepting states), • X is a finite set of clocks, • E ⊆ L × C(X) × Σ ∪ {ε} × 2 X × L is a finite set of switches (or transitions) e =
(l, g, a, r, l ) ∈ E from l to l , where g is the guard, r is the set of clocks to be reset and a is the label.

A clock valuation v for a set X of clocks is a mapping from X to R ≥0 ∪{⊥} that assigns to each clock x ∈ X a value v(x) in R ≥0 ∪ {⊥}. A clocks valuation v satisfies an atomic constraint (x # c) if and only if (v(x) # c) is true. This allows to check whether a guard g can be satisfied by a clocks valuation v, denoted as

v |= g. Given d ∈ R ≥0 , v = v + d is the clocks valuation such that v (x) = v(x) + d for each x ∈ X. Also, for r ⊆ X, v = [r ← 0]v denotes a clock valuation such that v (x) = 0 if x ∈ r and v (x) = v(x) if x ∈ X \ {r}.
As usual, each clock of a timed automaton is a real valued variable that records the amount of time that has elapsed since the last time the clock was reset. However, unlike "standard" timed automata, and in the same spirit as [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF], we assume that the values of all clocks are initially equal to ⊥ (i.e., undefined ). Then, the first time any clock x is reset to 0, its valuation starts to grow synchronously w.r.t. other clocks as time evolves. Detailed semantics of timed automata and discussion of "classic" verification problems (e.g., location reachability, closure under complementation) can be found in [START_REF] Alur | A theory of timed automata[END_REF]. We use the timed protocol from Figure 4 as a running example throughout this section. It allows us to illustrate the challenges in creating a timed automaton that behaves like a timed protocol. At first sight, the translation may look straightforward. However as we will see, preserving the behavior of M-Invoke is not an easy task. The translation is performed in two steps.

Informal overview of the challenges

The first step consists in a straightforward procedure that converts a timed protocol P into a timed automaton A as follows. States of P are translated into locations in A (e.g., the state s 0 of P is mapped to a location l 0 ). The initial state is mapped into an initial location while final states are mapped to final locations. Each explicit (respectively, implicit) transition in P is translated into a switch in A with the message name as its label (respectively, a ε-labeled switches). For example, in P, T 1 : R(s 0 , s 1 , a, true) is translated into a switch e 1 = (l 0 , true, a, r, l 1 ) in A. The transition identifiers from P are used to generate clocks in A. Indeed, each identifier generates a unique clock which is solely reset on its corresponding switch. For example the transition T 2 generates a clock x T 2 in A which is only reset on the switch that was mapped from T 2 . This way, we can know when a switch was fired, just like in the timed protocol P. The conversion of a C-Invoke constraint from P is also direct. For example, a constraint C-Invoke(T 1 < 3) is mapped to a guard (x T 1 < 3). At this stage, the mapping of P to A yields the timed automaton of Figure 5.

Let us now have a closer look on the mapping of implicit transitions. As mentioned before, implicit transitions are automatically fired whenever their associated M-Invoke constraints are evaluated to true. This semantics is not enforced in the target timed automata by simply mapping implicit transitions into ε-labeled switches with a direct translation of M-Invoke constraints into guards. Continuing with our example, the guard g 1 and g 2 of the timed automata of Figure 5, may potentially become satisfied at the same time, and hence the c-labeled transition can be fired while the guard g 2 of the ε-labeled switches is evaluated to true. To capture correctly the semantics of M-Invoke constraints in the timed automata, ε-labeled must be preempted with respect to other transitions that can be fired from the same location. To achieve this goal, additional constraints must be added during the mapping phase in order to ensure that once a guard of a given ε-labeled switch becomes true, all the other switches starting from the same location must be deactivated.

To see how such constraints can be enforced, let us have a closer look at the various cases that may occur when entering a location that offers one ε-labeled switch. We illustrate that again on the location l 2 of of Figure 5 but by considering only the switch c and one ε-labeled switch, namely the one associated with the guard g 1 . The generalization to more than one ε-labeled is straightforward, and will be detailed later. Three cases are possible. The first one is that l 2 is entered before g 1 has been satisfied (i.e., while the constraint (x T 1 < 10) is true). In this case c can be fired as long as (x T 1 < 10) is true. The second case is that l 2 is entered when the valuation of x T 1 is such that (x T 1 > 10): c can be fired since g 1 will never be satisfied in the future. Finally, third one is that l 2 is entered while (x T 1 < 10) is satisfied and the automaton remains at location l 2 while time elapses until an instant t such that the clock valuation becomes such that (x T 1 ≥ 10) is true. In this case c can be fired only if, in the past (i.e., at an instant t < t), when (x T 1 = 10) was true, (x T 2 > 2) was false. Note that, in this later case to decide if a transition c can be fired safely at a given instant t it is necessary to conduct a reasoning about the 'past' (i.e., the values of the clocks at an instant t < t).

To sum up, a direct translation of the M-Invoke constraints to guards is not enough to properly capture the implicit transitions semantics in timed automata. Because of that, more elaborated constraints need to be added into the guards. More specifically:

1. the mapping needs to rewrite some guards to enforce the expected behavior of M-Invoke constraints, and 2. there is a need for knowing the exact clock valuations when a location is entered:

(a) to know the status of each equality clause in each ε-labeled switches (e.g., when l 2 is entered, do we have (x T 2 < 5), (x T 2 > 5) or (x T 2 = 5)?) (b) to know if the ε-labeled switches guards will be satisfiable or not (e.g., g 2 ) when their equality clause is satisfied. In particular, knowing the valuation of each clock when a location was entered is important for enabling/disabling some switches. For example when entering l 2 , if x T 2 was already greater than 5, then we know that the ε-labeled switch with guard g 1 will have no influence on the execution of the c-labeled switch nor on the other ε-labeled switch.

In timed automata, as clocks evolve synchronously, the difference between 2 clocks x 1 and x 2 is a constant until one of them is reset to zero. In the following, we use diagonal constraints of the form (x 1x 2 # k), with k ∈ Q ∪ ⊥, to capture the clock valuations when locations are entered. More precisely, for each location offering at least one ε-labeled switch, we add a clock that is attached to this location. Such a clock is reset on every incoming switch of the considered location. For example on Figure 5, we add a clock y l 2 which is reset on the b-labeled switch. Then, the difference between any clock x e and such a "location clock" y l is the exact value of x e when the location l was entered. Indeed, when the location is entered, the valuation of y l is 0 as the clock has just been reset. Given that the difference between the two clocks remains a constant while l remains the current location, (x ey l ) is the clock valuation of x e when l was entered.

Using this technique to capture clock valuations at a time a location is entered, the second step of the mapping can be done by rewriting the guards of every switch whose source location offers ε-labeled switches. The rewriting must take care of allowing normal (i.e., non ε-labeled switches) to recognize input symbols when there is no conflict with ε-labeled switches and deactivate them otherwise. To this purpose, we will introduce new clock constraints to capture when a given switch is allowed with respect to the guard of a ε-labeled switch. Going back to the example of Figure 5 with a new clock y l 2 having been added, observe that g 1 must enable the other switches in the following two cases: (x T 2 < 5), and (x T 2 > 5) ∧ (x T 2y l 2 > 5). While the first case is rather easy (i.e., l 2 is entered before the equality clause has been satisfied), the second case uses the valuation of x T 2 when l 2 was entered. (x T 2y l 2 > 5) is only true if l 2 was entered when (x T 2 > 5) was true.

In a similar manner, g 2 enables the other switches in the following cases:

(x T 1 < 10), (x T 1 > 10) ∧ (x T 1 -y l 2 > 10), (x T 1 > 10) ∧ (x T 1 -y l 2 ≤ 10) ∧ (x T 2 -x T 1 ≤ -8), and (x T 1 = 10) ∧ (x T 2 -x T 1 ≤ -8).
The first two cases are similar to the case of g 1 . The third case enables the other switches after the equality clause of g 2 has been verified if the clause

(x T 2 > 2) is false when (x T 1 = 10) is true. Indeed, (x T 2 -x T 1 ≤ -8) = (x T 2 -x T 1 ≤ 2 -10)
and when x T 1 = 10, this reduces to (x T 2 ≤ 2) which is the negation of (x T 2 > 2). Hence the clause (x T 2 -x T 1 ≤ -8) is able to check when g 2 cannot be satisfied. Finally the fourth case is similar as it enables the other switches when the equality clause is satisfied if the rest of g 2 cannot be completely satisfied.

The correct mapping of P to A is given on Figure 6, where the "permits" constraints are just the cases that we mentioned above. For example, permits(g 1 ) = (x T 2 < 5)

x

T 2 > 5) ∧ (x T 2 -y l 2 > 5).

Enforcing M-Invoke constraints in protocol timed automata

To enforce M-Invoke semantics, the following behavior needs to be captured (examples are taken from Figure 5).

1. When a ε-labeled switch guard becomes satisfied, all other switches must be immediately disabled so as to make it the only switch that can be taken. An example is when g 1 becomes satisfied in l 2 : the two other switches must be disabled. 2. When a location offering a ε-labeled switch is entered after the equality clause of its guard has been satisfied, the other switches must not be disabled. For example, if l 2 is entered while x T 2 > 5, the other switches must not be disabled. 3. When the guard of a ε-labeled switch cannot be satisfied when its equality clause is satisfied, the other switches must not be disabled. Let us consider g 2 while the current location is l 2 . In case (x

T 1 = 10) is satisfied but (x T 2 > 2)
is not, the two other switches must not be disabled. The enforcement is done by rewriting the constraints using two new ones. First, we define a constraint "inhib" over a ε-labeled transition guard of the form g = (x = k) ∧ g . The role of this constraint is to capture the cases where g is false, thus making the switch that has g as its guard inactive. As we will see, this constraint plays a critical role in enforcing the M-Invoke constraints in protocol timed automata. Then, we will provide another constraint, called "permits", also defined over a ε-labeled transition guard. It defines when it allows other switches from the same source location to become actionable. This constraint relies on the introduction of clocks that are attached to locations so as to capture the clocks valuation when locations are entered. It uses "inhib" that we introduce in the following definition. Definition 4.2 (inhib constraint). Let a guard g := (x = k) ∧ g of a ε-labeled switch defined over a ε-labeled switch l → l such as x is a clock over

T = R ≥0 ∪ {⊥}, k is a constant in Q ∪ {⊥} and g is any clocks constraint: g = (x 1 # 1 k 1 ) ∧ • • • ∧ (x j # j k j ) ∧ (x j+1 -x j+1 # j+1 k j+1 ) ∧ • • • ∧ (x m -x m # m k m ) (for any i ∈ {1, • • • , m}: x i , x i ∈ X ∪ Y , k i ∈ Q ∪ {⊥}, # i
is any comparison operator) and Y is the set of clocks that we add to record when a location is entered by resetting them on the switches that are incoming to a given location.

We define the constraint "inhib" such that:

inhib(g) = (x 1 -x not(# 1 ) k 1 -k) ∨ • • • ∨ (x j -x not(# j ) k j -k) ∨ (x j+1 -x j+1 not(# j+1 ) k j+1 ) ∨ • • • ∨ (x m -x m not(# m ) k m )
In the case where g is not defined (i.e., g = (x = k)), then inhib(g) = false.

Going back to the timed automaton of Figure 5: inhib(g 1 ) = false and inhib(g 2 ) = (x T 2x T 1 ≤ -8). Without loss of generality, we chose to reduce the ε-labeled switch guard g to a unique conjunction in the previous definition to simplify the notations. The case where g is a disjunction is easy: we consider it as multiple ε-labeled switches with each switch having a single conjunctive guard. We keep this assumption in the remainder.

With this "inhib" constraint at hand, we can now define a constraint called permits. When given the guard of a ε-labeled switch, it defines when the other switches from the same source location can be enabled without contradicting M-Invoke constraints. Definition 4.3 (permits constraint). Let a guard g := (x = k) ∧ g of a ε-labeled switch defined over a ε-labeled switch l → l such as x is a clock over T, k is a constant in Q ∪ {⊥} and g is any clocks constraint. Let y ∈ Y the clock that is commonly reset by all the switches whose target location is l. We define the following clauses: S 1 = (x < k), S 2 = (x > k)∧(x-y > k), S 3 = (x > k)∧(x-y ≤ k)∧inhib(g), and S 4 = (x = k)∧inhib(g).

The constraint permits(g) is defined as permits(g) = i∈{1,2,3,4}

S i

The four permits clauses S i , with i ∈ [START_REF] Van Der Aalst | The Application of Petri Nets to Workflow Management[END_REF][START_REF] Alur | Decision problems for timed automata: A survey[END_REF], play the following roles. S 1 captures the cases where the current clocks valuation v ensures that v(x) is still below k. S 2 captures the cases where v is above k and the location l has been entered after (x = k) was satisfied. This is checked through the clause (xy > k). S 3 captures the cases where l was entered before (x = k) was satisfied, but g i could not be satisfied. In such cases, the switches should not be disabled for the clocks valuations such that (x > k) is satisfied. Finally, S 4 captures the cases where (x = k) is satisfied but g i is not, hence the switches don't have to be disabled as well. Again considering the timed automaton of Figure 5: permits(g 1 ) = (x T 2 < 5)

S 1 (x T 2 > 5) ∧ (x T 2 -y l 2 > 5) S 2
, and permits(g 2 ) = (x T 1 < 10)

S 1 (x T 1 > 10) ∧ (x T 1 -y l 2 > 10) S 2 (x T 1 > 10) ∧ (x T 1 -y l 2 ≤ 10) ∧ (x T 2 -x T 1 ≤ -8) inhib(g 2 ) S 3 (x T 1 = 10) ∧ (x T 2 -x T 1 ≤ -8) inhib(g 2 ) S 4
. We can now define how the guards of the switches whose source locations offer ε-labeled switches need to be rewritten so as to enforce M-Invoke .

Definition 4.4 ( M-Invoke enforcement). Let l be a location of a protocol timed automaton

A that offers n > 0 ε-labeled switches:

{e ε 1 = (l, g ε 1 , ε, r 1 , l 1 ), • • • , e εn = (l, g εn , ε, r n , l n )}
The rewriting of the guard of each switch whose source location is l (including the ε-labeled ones) is performed as follows:

1. for each location l that offers a ε-labeled switch, augment the reset set of each switch whose target location is l with the clock y l ∈ Y 2. compute {permits(g ε 1 ), • • • permits(g εn )} 3. rewrite the guard g of each switch (l, g, a, r, l ) as (a) when a = ε, g = 0≤i≤n permits(g ε i )

(b) when a = ε and the switch guard is

g ε j (j ∈ {1, • • • , m}), g = 0≤i =j≤n
permits(g ε i )

As an example, we consider again the protocol timed automaton of Figure 5 that has been fixed to enforce M-Invoke semantics on Figure 6.

Correctness of the mapping

The following theorem states the correctness of the mapping. It shows that a timed protocol and its corresponding timed automaton (produced by the mapping described above) have equivalent behaviors (they both recognize the same set of timed words). Theorem 4.5. Let A be a protocol timed automaton produced by a mapping of a timed protocol P. Then, T races(P) = L(A).

This theorem states that the set T races(P) of timed traces that are compliant with a protocol P is exactly the same as the language L(A) that is recognized by the corresponding timed automaton A. Hence, the mapping proposed in the previous section preserves the semantics of the timed protocols.

Proof of Theorem 4.5 is quite straightforward in the particular case where the original timed protocol P does not contain any implicit transitions. Therefore, the main point to prove Theorem 4.5 is to show that the guard rewritings presented in the previous section capture the M-Invoke constraint semantics correctly. The following lemma shows that the function inhib works as expected, i.e., it can inhibit guards when a ε-labeled switch guard is totally satisfied, and allow them when it is not. Lemma 4.6. Let a protocol timed automaton A and a location l ∈ A such that there exists a switch e = (l, g = (x = k) ∧ g , ε, r, l ), with g = (x

1 # 1 k 1 ) ∧ • • • ∧ (x j # j k j ) ∧ (x j+1 - x j+1 # j+1 k j+1 ) ∧ • • • ∧ (x m -x m # m k m ) for m ∈ N and j ∈ {1, • • • , m}. Then: (i) (inhib(g) = true) =⇒ (g = false), and (ii) (inhib(g) = false) =⇒ (g = true).
Given a location that has several ε-labeled switches, the following lemma checks that only one of them can ever become satisfied, thus disabling and forcing the transition to another location. To do that, we express the following sanity-check type of boolean implication.

Lemma 4.7. Let a protocol timed automaton A and a location l ∈ A such that it offers n > 0 ε-labeled switches. For any i ∈ {1, • • • , n}, the guard g i of the i-th ε-labeled switch is of the form g i 1≤i =j≤n permits(g j ). Let i ∈ {1, • • • , n} and j ∈ {1, • • • , n} such that i = j.

Then: (g j = true) =⇒ (permits(g j ) = false) ∧ (permits(g i ) = true) This implication expresses the fact that when a M-Invoke guard is satisfied, then its derived permits constraint is false, and the permits clauses of every other M-Invoke guards are still true. Indeed, if any of the later permits clauses was to be false, then it would mean that its guard would have already been actionable in the past, yet not taken and hence not enforced.

The following lemma states that the mapping of a timed protocol to a protocol timed automaton is correct with respect to M-Invoke constraints. Lemma 4.8. Let a protocol timed automaton A obtained from a timed protocol P. Every ε-labeled switch e = (l, g = (x = k) ∧ g , ε, r, l ) of A is taken as soon as its guard g is satisfied.

Characterization of protocol timed automata

The previous sections described how a timed protocol can be mapped to a particular class of timed automata called protocol timed automata. In this section, we leverage the formal framework of timed automata to investigate the computational properties (i.e., decidability and closure properties) of the protocol operators. As explained in previous sections, the operators are very useful to perform compatibility and replaceability analysis.

We start by stating the following result regarding the intersection operator.

Theorem 4.9. The class of protocol timed automata is closed under intersection.

This theorem is derived from existing results in the literature (e.g., [START_REF] Alur | A theory of timed automata[END_REF]). Indeed, it is known that timed automata with ε transitions are closed under intersection (and hence also under compatible composition). It is easy to extend this result to protocol timed automata (i.e., to show that the intersection or compatible composition of two protocol timed automata is still a protocol timed automata). The next section describes a procedure that implements such an intersection operator.

Let us now turn our attention to the complementation operator which plays a critical role when it comes to characterizing the protocol difference and subsumption operators. While the case of TI and TC was easy to deal with, the complementation operator poses more challenges. Indeed, in the general case, non-deterministic timed automata extended with ε-labeled switches are not closed under complementation [START_REF] Alur | Decision problems for timed automata: A survey[END_REF]. In our case, since we consider deterministic automata, this negative result is mainly due to the presence of εlabeled switches. [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] investigated the expressive power of ε-labeled switches and identified cases where ε-labeled switches can be removed without a loss of expressiveness (e.g., case of ε-labeled switches that do not reset clocks). Unfortunately, this result is of no use in our case as the ε-labeled switches that we deal with do not belong to the identified cases. In fact, as stated by the following theorem, ε-labeled switches strictly increase the expressiveness of protocol timed automata and hence they cannot be removed without losing in expressiveness.

Theorem 4.10. ε-labeled switches strictly increase the expressiveness of protocol timed automata.

The proof of this theorem, based on the notion of precise actions introduced in [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF], is presented in the appendix. Despite these negative results, we are still able to prove that the class of protocol timed automata is closed under complementation. The cornerstone of the proof is to show that, although protocol timed automata include ε-labeled switches, they still exhibit a deterministic behavior which ensures that at each step of an execution, all clock values are solely determined by the input word. This result is a key for deriving the following theorem.

Theorem 4.12. The class of protocol timed automata is closed under complementation.

A procedure which extends the usual complementation construction to the case of protocol timed automaton is described in the next section. The proof of this theorem, provided in the appendix, is based on the observation that the proposed procedure preserves the M-Invoke constraints in timed automata as well as determinism. Thanks to this, a word that is rejected by a protocol timed automaton A is necessarily accepted by its complement A.

The closure of protocol timed automata under intersection and complementation allows to derive the following results regarding the timed protocol operators. The result on the intersection and parallel composition operators is straightforward since both TI and TC operators are based on the intersection using a different matching of the messages depending on their polarities:

• in the case of TI , two messages match when they have the same name and polarity (e.g., a(+) and a(+))

• in the case of TC , two messages match when they have the same name but a different polarity (e.g., a(+) and a(-)).

The result on the difference operator comes from the closure of protocol timed automata under both intersection and complementation. Indeed, P 1 TD P 2 is equivalent to P 1 TI P 2 , hence timed protocol are also closed under difference. This comes from the closure under complementation and intersection as well as from the decidability of the reachability problem [START_REF] Alur | A theory of timed automata[END_REF] (i.e., checking whether

L(A 1 ) ⊆ L(A 2 ) is equivalent to checking whether L(A 1 ∩ A 2 ) = ∅ or not).
With the results presented above, we have proved that our full set of operators can be implemented by exploiting already-known constructs on timed automata [START_REF] Alur | A theory of timed automata[END_REF] and also by establishing new results regarding the novel class of timed automata that we have identified. This makes it possible to conduct automated analysis for all of the compatibility and replaceability classes on timed protocols.

Protocol operators algorithms

In this section, we give the procedures that implement the intersection and complementation operators of protocol timed automata. The procedure for the other operators (compatible composition, subsumption and equivalence) can be straightforwardly derived from these ones. The proposed procedures extend the existing constructions given in [START_REF] Alur | A theory of timed automata[END_REF] to maintain closure in protocol timed automata.

Intersection of protocol timed automata

The protocol timed automata intersection procedure extends the classical construction on timed automata [START_REF] Alur | A theory of timed automata[END_REF], which in turns already extends the construction on (untimed) automata [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]. In the following steps, we removed the existing permits clauses from the automata guards as new ones are being computed.

Given two protocol timed automata

A 1 = (Σ 1 , L 1 , L 0 1 , L f 1 , X 1 ∪ Y 1 , E 1 ) and A 2 = (Σ 2 , L 2 , L 0 2 , L f 2 , X 2 ∪Y 2 , E 2 ), the intersection A 3 = A 1 ∩A 2 (with A 3 = (Σ 3 , L 3 , L 0 3 , L f 3 , X 3 ∪ Y 3 , E 3 )
) is built through the following steps.

1. The locations are

L 3 = L 1 × L 2 , the initial location is L 0 3 = (L 0 1 , L 0
2 ) and the final locations are

L f 3 = (l 1 , l 2 ) | l 1 ∈ L f 1 , l 2 ∈ L f 2 .
2. Two switches e 1 = (l 1 , g 1 , a 1 , r 1 , l 1 ) ∈ A 1 and e 2 = (l 2 , g 2 , a 2 , r 2 , l 2 ) ∈ A 2 are synchronized if and only if a 1 = a 2 = ε, producing a new switch e 1 e 2 which is added to A 3 :

e 1 e 2 = ((l 1 , l 2 ), g 1 ∧ g 2 , a 1 , {x e 1 e 2 }, (l 1 , l 2
)) (this introduces a new clock x e 1 e 2 in A 3 ). 3. ε-labeled switches are first added to A 3 with their guard being freed of permits clauses.

We consider their guards to be disjunction-free (i.e., a ε-labeled switch whose guard is disjunctive is equivalent to several ε-labeled switches with conjunctive guards). For each pair of ε-labeled switches e 1 = (l 1 , (x

1 = k 1 )∧g 1 , ε, r 1 , l 1 ) ∈ A 1 and e 2 = (l 2 , (x 2 = k 2 ) ∧ g 2 , ε, r 2 , l
2 ) ∈ A 2 , we add the following switches to E 3 :

   e 1 e ε = ((l 1 , l 2 ), (x 1 = k 1 ) ∧ g 1 ∧ ((x 2 = k 2 ) ∨ ¬g 2 ), ε, {x e 1 eε }, (l 1 , l 2 )) e ε e 2 = ((l 1 , l 2 ), (x 2 = k 2 ) ∧ g 2 ∧ ((x 1 = k 1 ) ∨ ¬g 1 ), ε, {x eεe 2 }, (l 1 , l 2 )) e 1 e 2 = ((l 1 , l 2 ), (x 1 = k 1 ) ∧ (x 2 = k 2 ) ∧ g 1 ∧ g 2 , ε, {x e 1 e 2 }, (l 1 , l 2 )) 4.
With the set of clocks in A 3 being X ∪ Y as per definition, make sure that for each location l offering at least one ε-labeled switch, a clock y l ∈ Y is reset on all of the incoming switches to l. 5. For each location l ∈ A 3 , compute the permits clauses. 6. The guards in A 3 need to be rewritten to refer to the clocks of the switches of A 3 as they still refer to those of A 1 and A 2 at this step. A map is maintained between each clock x e of A 1 or A 2 and the set of clocks {x e,e1 , x e,e2 , x e3,e , • • • } that correspond to the switches {(e, e1), (e, e2), • • • , } that were generated from e. Given a guard g of a switch in A 3 , a clause (x e # k) of g is rewritten as a disjunction (x e,e1 # k)∨(x e,e2 # k)∨• • • . Diagonal constraint clauses in g are also rewritten in a similar fashion using the mappings of its two clocks.

Compared to the classic timed automata intersection procedure, the protocol timed automata intersection has the following differences.

1. Clocks assignment remains "under control" to match the protocol timed automata requirement of having at most two clocks reset per transition. The classical timed automata intersection construction would simply combine the set of clocks from both input timed automata and merge the clocks in the reset sets of each switch. 2. M-Invoke semantics are enforced in the intersection by computing new permits clauses (the permits clauses of the input timed automata guards are discarded).

Complementation of protocol timed automata

We compute the complement of a protocol timed automaton using the following procedure which is derived from the one for deterministic timed automata as given in [START_REF] Alur | A theory of timed automata[END_REF], with the difference lying in the presence of ε-transitions. Given a protocol timed automaton A, we denote by A * its complete automaton which is build as follows.

1. A location q is added to A * whose role is to act as a rejection location: given any timed word w defined over L(A), the execution of w over A * goes to the location q as soon as an input symbol yields to a word which is not in L(A). Hence, any timed word w defined over the alphabet of A has a (unique) execution over A * . 2. For each location l of A (this includes q) and for each word a of the alphabet, a transition e = l, g 1≤i≤n permits(g εi ) , a, {x e }, q is added where: (a) g is defined as the negation of the disjunctions1 of the guards2 of the other alabeled transitions from l, and (b) each g εi = (x i = k i ) ∧ g εi appears in the guard of the i-th ε-labeled switch from l, given that l offers n ≥ 0 of such switches. As in [START_REF] Alur | A theory of timed automata[END_REF], the complement A of A is deduced from A * by inverting the final and the normal locations due to the fact that every timed word w ∈ L(A) has a unique run over A.

Implementation and usage

In the sections above, we have exposed the timed business protocols model and analysis techniques. We now turn our attention to the validation of our approach. We first present our prototype platform, and then we show a typical usage scenario of the tool to show how it supports service development. The concepts discussed in this paper have been implemented in ServiceMosaic, a CASE platform for supporting the service development lifecycle that includes facilities for modeling, analyzing, discovering, and adapting web service models [START_REF] Benatallah | Service mosaic: A model-driven framework for web services life-cycle management[END_REF]. We are releasing most tools at http://servicemosaic.isima.fr/downloads/protocols/ under the terms of the opensource LGPLv3 license. The ServiceMosaic tools are developed for the Java TM platform version 5. Specifically, we created libraries that provide the functionalities of our contributions (e.g., protocol operators) and we integrated them into the Eclipse platform (see http://www.eclipse.org/) as plug-ins (e.g., a plug-in provides the graphical user interface for applying the protocol operators). The components that we have developed for this work are depicted on Figure 7. We have created a library containing the object model of timed protocols. The AntLR parser generator (see http://www.antlr.org/) has been used to parse C-Invoke and M-Invoke constraints from strings representations. We have also created a timed protocol operators library. All of the operators (intersection, parallel composition, difference, subsumption and equivalence) have been implemented in Java TM . The subsumption and equivalence operators rely on the external UPPAAL timed automata model checker [START_REF] Behrmann | A tutorial on uppaal[END_REF], as they require testing for language emptiness. As a requirement of the subsumption operator definition, we have also implemented a complementation operator. The protocol extraction library relies on the protocols model library to extract the web services choreographies from a BPEL process. Figure 8 provides a screenshot of the prototype.

Protocol analysis at work

We now show how the prototype and protocol analysis approach can be used to facilitate service development on the following scenario. The scope of applications of protocol analysis goes however beyond just this example as we will see in the next section. We assume here that a developer is defining a BPEL process, related to the handling of a purchase order, and that the process invokes several services during its execution. The tool will assist the developer in checking if the selected services have a protocol which is fully or partially compatible with the defined BPEL process, will identify which conversations can and cannot be carried out, and will also tackle the case of non compatibility by supporting the development of protocol adapters.

BPEL process outline

Consider the BPEL process depicted on Figure 9. It orchestrates four web services to process a purchase order. For the sake of clarity, we have removed the assign BPEL instructions from the process diagram, normally required to prepare and reuse the messages exchanged with the involved web services. The first part of the process handles the payment options. If the customer asks for a loan, then the process will make an offer using the accounting web service. The customer can then accept or reject it. The asynchronous pick BPEL construction defines an alarm that will be fired after 72 hours to discard the process instance if the customer does not reply in time to the loan offer. The second part checks for the ordered goods availability with the warehouse web service. If some goods are not available, they will be ordered. In order to match quality of service requirements, the purchase is canceled if the warehouse does not manage to purchase the missing goods within 48 hours. The third an last part of the process handles the payment and prepares the goods delivery. Finally, the customer is notified that the purchase has successfully completed.

Business protocols extraction

Based on this BPEL process definition, we extract the timed protocols that the process supports when interacting with its partner services. To do this, we use our multi-party protocol BPEL extractor, and we then obtain the protocol governing the interaction of the process with each of the partner services by filtering the multi-party protocol based on each service partner link. The extractor, developed as part of the ServiceMosaic project, takes a BPEL process as its input and then outputs a multi-party protocol, an extension of a timed protocol where a message is also tagged with the partner link of the service which is sending or receiving the message. As such, a multi-party business protocol captures the message choreography of a BPEL process orchestrator. First, we identify protocol extraction patterns for each type of basic and complex BPEL activity. The extraction starts from the beginning of the process and goes through each activity to apply the protocol Figure 9: A BPEL process that handles purchase orders. extraction patterns as they are recognized. When a complex activity is encountered (e.g., if, switch, while, pick, ...), it is recursively processed on each of its complex activities until basic activities are reached. The obtained protocol fragments are assembled by inverse recursion. For instance, if a if activity comprises one invoke on each alternative branch, then a protocol fragment is derived from each invoke, then they are combined as different branches from the current state in the extraction process.

The protocol which is followed by the process while interacting with a given service (identified by its BPEL partner link ) can be obtained as follows. The idea is to perform a special form of filtering on the multi-party protocol. In a similar fashion as projection for timed automata [START_REF] Alur | Decision problems for timed automata: A survey[END_REF], we replace the messages with ε on the transitions that are not associated with the partner link of the service that we are interested in. Also, each temporal constraint that refers to a transition which is not from the target partner link is removed. Indeed, they do not make sense in the protocol that we want to obtain since they refer to events that are not "seen" by the orchestrated service. Finally, the service protocol is obtained by removing the ε transitions using standard techniques on automata [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]. This is possible only because if we mapped to timed automata, there would be no guard nor clock resets on these transitions [START_REF] Volker Diekert | Removing epsilon-transitions in timed automata[END_REF]. While still experimental, we have found out that the protocol extraction operator works well for a large majority of BPEL processes In this scenario, the resulting protocols are shown in Figure 10. Figure 11 shows instead the protocol of the warehouse service we are planning to use as one of the services invoked by our process. Note that this transformation is not reversible. When generating a protocol, we only care about possible ordering of messages and not about the many details prescribed by a BPEL process (such as why -based on which condition -a certain path is chosen). Nevertheless, we had developed developed techniques for generating service implementation templates in BPEL from protocols definitions [START_REF] Baïna | Model-driven web service development[END_REF].

Figure 11: The complete warehouse service protocol. We next apply the protocol analysis operators to assess compatibility between the protocols supported by our process and the protocols of the services we plan to use. For this, we assume that either the protocol or BPEL definition (from which we extract the protocol) of these services is available. Figure 12 shows the results of this analysis for the warehouse service. In particular, the compatible composition operator P 5 TI P 3 gives the set of the conversations that can occur between protocols P 3 and P 5 . Ideally, we would want this set to be equal to the conversations supported by P 3 , which means that P 5 is fully compatible with P 3 . However, in our example, we do not have such luck. In fact we see that the conversations supported by the compatible composition are a subset of those supported by P 3 . The figure further shows the conversations that are supported by the process but not by our partner service P 5 (which is empty in case of full compatibility), as well as the conversations that the partner supports but that the process does not support. The first of these two combined protocols is obtained by computing the inverse P -1 3 of P 3 and then the difference P -1

Protocol analysis

3 TD P 5 . The latter is instead computed as P 5 TD P -1 3 . As we will examine later, all these combined protocols will become helpful in examining if and which changes need to be made to the process.

In particular, while the first combined protocol of Figure 12 (compatible composition) tells us what we can do, the second one denotes what our process is prevented from doing when using this partner (hence we call these prevented interactions), while the third one denotes conversations that the partner would support, but we are not leveraging due to how we implemented the process. We call these neglected interactions.

It is interesting to note that no compatibility problem would have been spotted in the case of business protocols without timing constraints [START_REF] Benatallah | Representing, analysing and managing web service protocols[END_REF]. Indeed, the untimed version of P 5 would have supported all of the conversations of the untimed version of P 3 .

Managing partial replaceability scenarios

By looking at the three combined protocols, the developer can assess if the selected service is a good fit or not, and how to handle situations of partial replaceability or of no replaceability. In general, this depends on the specific business purpose of the process. For example, the service I am planning to invoke may not support a cancelP O operation, but I may be willing to take the risk and use it anyways even if cancellations are not allowed, for example because it offers cheaper rates. Or, conversely, the selected service supports several forms of payments (accessed via different protocols) but my process can only support one of them, and we may be fine with it as for example our company only issues payments via credit card and not via bank transfers.

Alternatively, we can modify the process definition to adapt it to the service we are using, either to:

1. ensure that our process does not generate conversations our partner cannot understand, or 2. leverage conversations supported by our selected services (e.g., extend our process to support bank transfers).

As another example, in our process, we can remove the onAlarm 48h handler of the second pick complex activity, so that the process will wait for the purchaseResponse message to arrive, thereby removing the problematic temporal constraints in the extracted expected warehouse protocol. However, the process may find itself being put on hold indefinitely if a problem occurs on the warehouse service and it does not send a purchaseResponse message back.

Another solution is to generate a protocol adapter [START_REF] Benatallah | Developing adapters for web services integration[END_REF] to reconcile the differences. It can be done with the ServiceMosaic tools using an aspect-oriented framework [START_REF] Kongdenfha | An aspect-oriented framework for service adaptation[END_REF] where adapters are plugged through advices written in BPEL. The adapter is developed as follows. The pointcut is triggered when a purchaseRequest message is received. The advice is a BPEL process where an alarm starts counting from the reception of the purchaseRequest message. If the service does not send a purchaseResponse withing the next 48 hours, then the adapter drops it when the warehouse service sends it afterwards. The BPEL engine will have already woken up the process instance by then, and taken action by replying to the client partner link with a cancelP O message.

Finally, it should be noted that for most BPEL engines, a message is simply dropped when it cannot be dispatched to any process instance for which it is waiting. An exception is then usually raised and logged inside the BPEL engine. In this example the adapter would be useful for diminishing the number of internally-thrown exceptions (raising exceptions has a significant performance cost). The choice of developing this adapter should be balanced in light of its development cost compared to the (limited) benefits, as BPEL engines can provide a form of "implicit" adapter in very specific mismatches cases such as this one.

Discussion

We now provide a discussion that includes related work as well as two limitations of our approach.

Related work

Timed automata

Many classes and extensions of timed automata have been studied. Deterministic timed automata [START_REF] Alur | A theory of timed automata[END_REF] are known to be closed under complementation. So are event-clock automata [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF], a subclass of deterministic timed automata which have the interesting property that every such indeterministic automaton has an equivalent deterministic automaton. Allowing diagonal constraints (xy # c) [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] make the model more concise but does not add to the expressiveness. Additive constraints (x + y # c) renders the emptiness checking problem decidable for 1 or 2 clocks, open for 3 clocks and undecidable starting from 4 clocks [START_REF] Bérard | Timed automata and additive clock constraints[END_REF]. Non-standard (x := 0) clocks resets make this problem decidable for x := c and x := x + 1 (if diagonal constraints are not allowed) but undecidable for x := x -1 [START_REF] Bouyer | Updatable timed automata[END_REF]. The class of Robust Timed Automata allows to recognize events with fuzziness w.r.t. dates [START_REF] Alur | Decision problems for timed automata: A survey[END_REF]. Previous work on timed automata augmented with ε-transition had suggested that the class of protocol timed automata would not have been closed under complementation [START_REF] Bouyer | Undecidability results for timed automata with silent transitions[END_REF][START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF][START_REF] Volker Diekert | Removing epsilon-transitions in timed automata[END_REF]. While the results presented in [START_REF] Volker Diekert | Removing epsilon-transitions in timed automata[END_REF] still hold in the general case where ε-transitions can reset an arbitrary number of clocks and have complex guards on transitions, we have identified a very specific class for which the traditionally "hard" problems become decidable (closure under complementation and language inclusion). The class of event-recording timed automata [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF] is a subset of deterministic timed automata. They also form a subset of protocol timed automata.

Standardization efforts

Standardization organizations (e.g., W3C, OASIS) have tried to provide specifications for describing the external behavior of web services in terms of both choreographies and orchestrations. They build on top of the existing widely used specifications for the static interfaces of web services (e.g., WSDL, XML-Schema). BPEL, WSCL and WSCI are examples of specifications that feature support for describing services conversations [START_REF] Papazoglou | Special issue on service oriented computing[END_REF], although the last two do not seem to have gained much adoption in practice. Our work is complementary to those specifications rather than competing. Choreography specifications (in WSCI or a WSCL extension) can be derived back and forth from timed protocols. BPEL orchestrations can be processed by our protocol extraction tool for obtaining the expected business protocol of each service that it orchestrates.

Models for web services

Research on web services has lead to various models being proposed to describe their behavior and/or implementation for the purpose of analysis and execution. A discussion on modeling web services interactions has been proposed in [START_REF] Bultan | Modeling interactions of web software (invited paper)[END_REF] and is further discussed in [START_REF] Bultan | Analyzing Conversations of Web Services[END_REF]. An approach for web services interfaces was defined in [START_REF] Beyer | Web service interfaces[END_REF]. A model with similar goals as timed protocols had been introduced in [START_REF] Berardi | Finite state automata as conceptual model for e-services[END_REF], but the timing constraints defined in the model have not been taken into account. A language for web services choreographies called Chor has been proposed in [START_REF] Qiu | Towards the theoretical foundation of choreography[END_REF] as a simplification of WS-CDL. All of these approaches share many similarities with this work and the base model for business protocols of [START_REF] Benatallah | Representing, analysing and managing web service protocols[END_REF]. Surprisingly, little work has been done on timing abstractions.

Verification techniques

Many works have tried to apply in various fields verification techniques such as checking for liveness, the absence of deadlocks or the conformance against specifications. A substantial amount of work has been done in the field of workflow systems [START_REF] Van Der Aalst | The Application of Petri Nets to Workflow Management[END_REF][START_REF] De | An automaton-based approach to the verification of timed workflow schemas[END_REF][START_REF] Bettini | Temporal reasoning in workflow systems[END_REF]. In the case of web services, timed automata have been used in [START_REF] Raman Kazhamiakin | Timed modelling and analysis in web service compositions[END_REF][START_REF] Díaz | Automatic generation of correct web services choreographies and orchestrations with model checking techniques[END_REF][START_REF] Berardi | Finite state automata as conceptual model for e-services[END_REF]. In the case of [START_REF] Berardi | Finite state automata as conceptual model for e-services[END_REF] the WSTL model had been designed with timing constraints as "first-class citizen", but they have never been leveraged. BPEL-based web services interactions have been analyzed in [START_REF] Fu | Analysis of interacting bpel web services[END_REF] by the mean of guarded automata with unbounded message queues where the automata synchronization problem is studied in synchronous and asynchronous communications. The same types of verifications can be easily done on protocol timed automata using TCTL, an extension of temporal logics for timed automata, and a model checker such as UPPAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF]. Such approaches are complementary to this work. Interestingly, we reused and extended results from the field of formal verification (e.g., timed automata), but not for the purpose of doing "classical" model-checking.

Compatibility and replaceability

Software components have some fundamental similarities with web services: they promote good practices such as loose coupling and reuse. Also, they can be remotely accessed over a network. Similar approaches for protocols compatibility and replaceability exist in the area of component-based systems [START_REF] Yellin | Protocol Specifications and Component Adaptors[END_REF][START_REF] Canal | Adding roles to corba objects[END_REF]. The importance of being able to check for services compatibility or replaceability has lead to several research works [START_REF] Mecella | Compatibility of e -services in a cooperative multi-platform environment[END_REF][START_REF] Foster | Leveraging eclipse for integrated model-based engineering of web service compositions[END_REF][START_REF] Beyer | Web service interfaces[END_REF]. Surprisingly, these approaches do not cater for timing constraints. They also perform "black or white" analysis. By contrast, our approach is able to provide a more fine-grained type of analysis by identifying the "partial cases" like the partial compatibility or the replaceability with respect to a client protocol. We believe that this flexibility will significantly prove to be useful in practice, as full compatibility or replaceability of business protocols can hardly be reached on the Internet which is an open service deployment environment. The notion of process inheritance has been studied in the domain of workflows [START_REF] Van Der Aalst | Inheritance of business processes: A journey visiting four notorious problems[END_REF][START_REF] Bussler | Process inheritance[END_REF]. It is similar to protocols replaceability. Different types of inheritance relations are proposed in [START_REF] Van Der Aalst | Inheritance of business processes: A journey visiting four notorious problems[END_REF]. They provide some flexibility much like we did with the different classes of protocol replaceability. However, these approaches do not consider temporal abstractions.

Model management

The work that has been done in the model management area focuses on manipulating models (e.g., database schemas, XML schemas) and matches between them (e.g., equivalence between 2 database schema) on an equal foot [START_REF] Bernstein | Industrial-strength schema matching[END_REF]. The matches relationships between 2 models can be used for matching, merging or composition purposes. The models can also be manipulated through various operators like the intersection, the union or the difference. A set of combined static and behavioral matching and merging techniques for statecharts-based specifications have been proposed in [START_REF] Nejati | Matching and merging of statecharts specifications[END_REF]. This work has been done in a similar fashion as the approaches for schema matching (including databases and XML) mentioned in [START_REF] Rahm | A survey of approaches to automatic schema matching[END_REF][START_REF] Bernstein | Industrial-strength schema matching[END_REF]. The work presented in this paper is largely inspired what has been done in this research field. Indeed, timed protocols are models and we have defined protocol manipulation operators (composition, difference and intersection) as well as comparison operators (subsumption and equivalence) that define matchings between protocols. The match operator of [START_REF] Nejati | Matching and merging of statecharts specifications[END_REF] could be used to identify compatibility and replaceability between two (untimed) business protocols of [START_REF] Benatallah | Representing, analysing and managing web service protocols[END_REF]. A clear benefit of this approach would be to detect matches when protocols have different messages names but similar semantics (e.g., login and connect), as in our case the operators match the messages only on name equality. The matches and mismatches could then be exploited to generate protocol adapters [START_REF] Benatallah | Developing adapters for web services integration[END_REF][START_REF] Reza | Semi-automated adaptation of service interactions[END_REF]. However, it requires human intervention as the heuristic results may contain missing and invalid matches. Also, it does not cater for timing constraints as they require proper analysis techniques as done on timed automata.

Limitations

Constraints with absolute dates

Timed protocol constraints are always expressed relatively to a transition of a given protocol being fired (e.g., C-Invoke(T 1 < 3h)). Absolute dates cannot be used in constraints (e.g., C-Invoke(T 1 < '2007-04-19 14:49:00') or C-Invoke(current time < '2007-04-19 14:49:00')). Such types of constraints can be found in some specifications such as BPEL [START_REF]Web Services Business Process Execution Language Version 2[END_REF] where both types of relative and absolute time expressions can be used. Let us briefly investigate the impact of introducing absolute dates into the model by looking at the involved mechanisms at the timed automata level. Allowing a constraint to compare a clock x to a constant date (e.g., x < '2007-04-19 14:49:00') which represents an absolute date requires the following assumptions. (i) x is set to a constant now which represents the current date when the automaton execution starts, and (ii) x is always compared to absolute dates, and (iii) x is never reset in the considered automaton.

We claim that making such an extension renders the timed language emptiness checking problem undecidable. The proof can be done by observing that now is actually a variable. In timed automata, the clocks are set to a constant value (usually 0) when the execution starts. Here, we would have some special clocks that would be initially set to a value which depends on the current time. Hence, the result of checking for the emptiness of such an extended timed automaton would only hold considering the time at which the checking has been performed (i.e., the results holds at time t but may not hold anymore at time t + δ with any δ ∈ R ≥0 ).

This limitation of timed protocols in terms of expressiveness is not a penalty as such constructs are of limited use in practice. In the case of BPEL, timers are mainly used for generating timeout exceptions in asynchronous operations (e.g., the pick complex activity). They can be also used for a wait activity (e.g., put the process in sleep to enforce legal regulations). In our experience, we have never found a need for expressing absolute dates in BPEL processes. Also, JBoss JBPM (see http://www.jboss.com/products/jbpm), a widely used business process management system, offers a workflow language called jPDL where time-related constructs are always expressed in a relative manner (i.e., jPDL does not allow specifying absolute dates for timers).

Message transport communications

Finally, our model is based on the assumption that there are no message transmission delays and losses. This is of course not the case in reality as web services messages are mostly transported over unreliable networks that can have substantial load variations, leading to greatly varying network latencies and even errors. As mentioned in related work, the class of Robust Timed Automata [START_REF] Alur | Decision problems for timed automata: A survey[END_REF] is a possible exploration path.

Conclusion

This paper has revisited the concepts presented in earlier work by providing an extended model for web services business protocols that supports timing abstractions. The level of abstraction that drove the design of this model was developed on the grounds of a study of real-world scenarios related to web services. The model can be leveraged for fine-grained protocol compatibility and replaceability analysis based on a set of protocol manipulation and comparison operators. We showed that the decision problems surrounding their implementation are decidable, thanks to the mapping and the identification of a novel class of timed automata which is closed under complementation and for which the language inclusion problem is decidable despite the presence of ε-transitions with clocks resets. We also presented our initial prototype as part of the ServiceMosaic project and gave a case study.

The results presented in this paper will pave the road for an agile web services composition development and management framework. Briefly, this environment will be centered around protocol repositories. They will be queried for compatibility at development time, allowing the rapid-prototyping of service compositions. In turn, they will be queried for replaceability at runtime to handle needs to substitute a service that becomes unavailable or whose protocol has changed. In both development and runtime environments, the framework will provide means to help at generating adapters.

We believe that modeling and analysis techniques with formal foundations such as the ones that we have presented will help at transforming the development and the maintenance of web services based applications from an "art", requiring a substantial amount of manual interventions, to a model-driven process that is automated to a large extent.

It is easy to check that A is a protocol timed automaton. A presents 2 ε-transitions lying on directed cycles, hence we don't know if they can be removed using the techniques presented in Section 8 in [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF].

Let us now suppose that L(A) can be recognized by a timed automaton A without any ε-transition. Note that A is free of diagonal constraints (e.g., constraints of the form xy # c). A can be rendered disjunction-free without any loss of generality (see [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] for techniques and discussion). In order to leverage the Theorem 24 of [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF], we define C max = 1 (no constant in the guards of A is larger than 1). Let also δ > 0. A can recognize timed words of the form

(b, δ 1 ) • (b, δ 2 ) • • • (b, δ d-1 ) • (a, d) • (a, d + 1) • • •
where d ∈ N, d ≥ C max and δ i ∈ (i -1, i) \ δN for all 0 < i < d. Let P a path of A that accepts such a timed word. Given that the a-labeled events occur at integer times, their occurrences should be precise in P . Also, d ≥ C max , hence from Theorem 24 of [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF], there exist some occurrence of b that should be precise in P which is not possible as δ i ∈ δN for any 0 < i < d. Consequently, L(A) cannot be recognized by a timed automaton without ε-transitions.

B Proof of Lemma 4.7

Proof. Let us check the implication.

(g j = false) (permits(g j ) = false) ∧ (permits(g i ) = true) = true is equivalent to (permits(g j ) = true) (permits(g j ) = false) ∧ (permits(g i ) = true) = true which reduces to (permits(g j ) = true) false as g j =true (permits(g i ) = true) = true permits(g i )=true

and the implication is verified. Indeed, permits(g i ) = true, else this would mean that the switch whose guard is g i had already been activated.

C Proof of Theorem 4.8

Proof. Let us compute the cases where inhib(g) evaluates to false. We assume that y ∈ Y is the clock that is reset on every switch whose target location is l. We compute and expand the negation: ¬ permits(g) = (x = k) ∧ ¬ inhib(g)

∨ (x ≥ k) ∧ (x -y ≤ k) ∧ ¬ inhib(g) = (x ≥ k) ∧ (x -y ≤ k) ∧ ¬ inhib(g) (1)
(1): ((x = k) = true) =⇒ ((xy ≤ k) = true). This means that disables switches when: 1. (x = k) is satisfied as well as g , resulting in the ε-labeled switch whose guard is g to be enabled, or 2. l was entered before (x = k) was satisfied, g was satisfied when (x = k) was, and the current clocks valuation satisfies (x ≥ k), forcing the ε-labeled switch to be taken.

D Proof of Lemma 4.11

Proof. Let us consider a location l that offers several switches, including n > 0 ε-labeled ones. By considering two switches from l, three cases are possible.

1. The switches have both labels that are not ε. By definition their guards are disjoint. 2. One switch e i (i ∈ {1, • • • , n}) has ε as its label with a guard (g i 1≤j =i≤n permits(g j ))

and the other switch has a label that is not ε and a guard (g 1≤j≤n permits(g j ))

The product of the guards contains a sub-clause (g i ∧ permits(g i )) which is false: the guards are disjoint.

3. The two switches have ε as their label. The product of their guards will make a sub-clause of the following form to appear: (x i = k i ) ∧ g i ∧ permits(g j ) ∧ (x j = k j ) ∧ g j ∧ permits(g i ) (i and j belong to {1, • • • , n} with i = j). As permits(g j ) ∧ g j is false, the guards are disjoint.

E Proof of Theorem 4.12

Proof. The construction of A * adds one location q to A as well as one new switch per symbol of the alphabet and per location of A plus q. We first show that the construction preserves determinism, and that given an input symbol, it can be recognized for any clocks valuation when the current location doesn't have any ε-labeled switch.

As every new switch guard is defined as the negation of the disjunctions of the guards of the switches from the same label, the intersection of the guards of every switch on the same label for a location l is necessarily false, meaning that those guards are disjoint. In the case where a location l does not offer any ε-labeled switch, it is also easy to check that the disjunction of the guards of the switches having the same label from l is true as in [START_REF] Alur | A theory of timed automata[END_REF].

Let us now consider a location l having n > 0 ε-labeled switches g εi (1 ≤ i ≤ n). We also consider any symbol a of the alphabet and the m > 0 guards of the a-labeled switches from l: {g 1 , • • • , g m } (again, given 1 ≤ j ≤ m, g j is considered without its permits constraint clauses). Let us compute the disjunction of the a-labeled switches guards:  which means that a is recognized from l under M-Invoke semantics. However, A must also recognize a when this expression evaluates to false, which is clearly not possible from l.

Let v be a clocks valuation such that a is to be recognized and We can make the following remarks: 1. the current location is not l anymore as a ε-labeled switch has been taken for the first clock valuation that stopped satisfying the previous expression, and 2. the current location change through the ε-labeled switch was instantaneous.

Let us call the current location l . By construction, it offers a-labeled switches. From the remarks above, the guard of every switch satisfies

Figure 1 :

 1 Figure 1: A timed protocol of an online financing service.

Figure 2 :

 2 Figure 2: Compatibility and replaceability analysis.

Figure 3 :

 3 Figure 3: A sample timed automaton A.

Figure 4 :

 4 Figure 4: A sample timed protocol P used as a mapping running example.

Figure 5 :

 5 Figure 5: A sample timed automaton that does not enforce M-Invoke semantics.

Figure 6 :

 6 Figure 6: A sample protocol timed automaton that does enforce M-Invoke semantics.

Lemma 4 . 11 .

 411 Protocol timed automata behave deterministically: given a protocol timed automaton A and a timed word w ∈ L(A), w has exactly one run over A.

Corollary 4 . 13 .

 413 Timed protocols are closed under TI , TC and TD .

Corollary 4 . 14 .

 414 The timed protocol comparison operators and ≡ are decidable.

6. 1 Figure 7 :

 17 Figure 7: Components of the ServiceMosaic protocol development and analysis prototype.

Figure 8 :

 8 Figure 8: Screenshot of the ServiceMosaic protocol development and analysis prototype.

Figure 10 :

 10 Figure 10: Timed protocols extracted from the BPEL process of Figure 9.

Figure 12 :

 12 Figure 12: Analysis of the common and differing conversations supported by P 3 and P 5 .

¬

  permits(g) = (x > k)∧ ((x ≤ k) ∨ (xy ≤ k)) ∧ ((x ≤ k) ∨ (xy > k) ∨ ¬ inhib(g)) ∧ ((x = k) ∨ ¬ inhib(g))we make a first development:= ((x = k) ∨ (x ≥ k) ∧ (xy ≤ k)) ∧ ((x < k) ∨ (x = k) ∧ (xy > k) ∨ (x = k) ∧ ¬ inhib(g) ∨ (x ≤ k) ∧ ¬ inhib(g) ∨ (xy > k) ∧ ¬ inhib(g) ∨ ¬ inhib(g))and a second one:= (x = k) ∧ ¬ inhib(g) ∨ (x = k) ∧ (xy > k) ∧ ¬ inhib(g) false ∨ (x > k) ∧ (xy ≤ k) ∧ ¬ inhib(g) ∨ (x = k) ∧ (xy ≤ k) ∧ ¬ inhib(g) ∨ (x ≥ k) ∧ (xy ≤ k) ∧ ¬ inhib(g)by reducing the last 3 disjunctions:



  By construction there exists j ∈ {1, • • • , m} such that g j = ¬ 1≤k =j≤m g k , hence the previous disjunction reduces to: 1≤i≤n permits(g εi )

  valuation v. Consequently, a can always be recognized from l and the locations available through its ε-labeled switches:

Table 2 :

 2 Characterization of the compatibility and replaceability classes.

e.g., given

a-labeled switches with guards g1 and g2, g = ¬(g1 ∨ g2)[START_REF] Alur | A theory of timed automata[END_REF] For each guard, we do not take into account the clauses that are obtained through the permits constraint.

Acknowledgments

We would like to thank the following people for their help: Cécile Maudelonde-Andrieu (RosettaNet PIPs), Sandrine Rivet (multi-party timed protocols extraction from BPEL) and Kevin Hivernat (protocol repositories). We would also like to thank the anonymous reviewers for their accurate and interesting remarks.

A Proof of Lemma 4.10 Proof. We need to show that ε-transitions in protocol timed automata cannot always be removed, i.e., there are protocol timed automata for which there doesn't exist equivalent automata without ε-transitions. To do that, we exhibit the protocol timed automaton A depicted on Figure 13 and use the notions of precise time and precise actions that were introduced in the Theorem 24 of [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] as a tool to identify timed languages that can only be recognized by timed automata featuring ε-transitions. The proof is virtually the same as the one of Corollary 29 in [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF].