CLIENT SYNTHESIS FOR WEB SERVICES BY WAY OF A TIMED

SEMANTICS

Serge Haddad

LAMSADE, Université Paris Dauphine

Place du Maréchal de Lattre de Tassigny, 75775 Paris Cedex 16, FRANCE

Patrice Moreaux

LISTIC-ESIA, Université de Savoie

Domaine universitaire d’Annecy le vieux, BP 806, 74016 Annecy Cedex, FRANCE

Sylvain Rampacek

CReSTIC, Université de Reims Champagne-Ardenne

UFR Sciences de Reims, BP 1039, 51687 Reims Cedex 02, FRANCE

Keywords:

Web Services, BPEL4WS, Algebra of timed processes, Timed Automata.

Abstract:

A complex Web service described with languages like BPEL4WS, consists of an executable process and its ob-

servable behaviour (called an abstract process) based on the messages exchanged with the client. The abstract

process behaviour is non deterministic due to the internal choices during the service execution. Furthermore

the speciﬁcation often includes timing constraints which must be taken into account by the client. Thus given

a service speciﬁcation, we identify the synthesis of a client as a key issue for the development of Web services.

To this end, we propose an approach based on (dense) timed automata to ﬁrst describe the observable service

behaviour and then to build correct interacting clients when possible. The present work extends a previous

discrete time approach and overcomes its limitations.

1 INTRODUCTION

From elementary Web services to complex ones

Web services are “self contained, self-describing

modular applications that can be published, located,

and invoked across the Web” (Tidwell, 2000). They

are based on a set of independent open platform stan-

dards to reach a high level of acceptance. Web ser-

vices framework is divided into three areas: commu-

nication protocol, service discovery and service de-

scription. The “Web Services Description Language”

(WSDL) (WSDL, 2001) provides a formal, computer-

readable description of Web services. Such a de-

scription speciﬁes the software component interfaces

listing the collection of operations that are network

accessible through standard XML messaging. It in-

cludes all information that an application needs to

invoke such as the message structure, the response

structure and some binding information like the trans-

port protocol, the port address, etc. However sim-

ple operation invocation is not sufﬁcient for some

kind of composite services. They require in addi-

tion a long-running interaction derived by an explicit

process model. This kind of services may often be

encountered in two cases. First when a Web service is

developed, it is composed by a set of accessible oper-

ations and a process model which schedules the invo-

cation to a correct use of the service. Secondly, fac-

ing to the capability limits of Web services, composite

services may be obtained by aggregating existing Web

services in order to create more sophisticated services

(and this in a recursive way). In order to deal with the

behavioural aspects of complex services, some indus-

trial and academic speciﬁcations languages have been

introduced. Among them, “Business Process Execu-

tion Language for Web Services” (BPEL4WS or more

succinctly BPEL) has been proposed by leading ac-

tors of industry (BEA, IBM, and Microsoft) and has

quickly become a standard (Andrews et al., 2003).

The two facets of complex Web services BPEL

supports two different types of business processes -

see for instance (Juric, 2005), (Juric et al., 2005):

• Executable processes specify the exact details of

business processes. They can be executed by an

orchestration engine.

Haddad S., Moreaux P. and Rampacek S. (2006).

CLIENT SYNTHESIS FOR WEB SERVICES BY WAY OF A TIMED SEMANTICS.

In Proceedings of the Eighth International Conference on Enterprise Information Systems - SAIC, pages 19-26

DOI: 10.5220/0002460700190026

 SciTePress

• Abstract business protocols specify the public mes-

sage exchange between the client and the service.

They do not include the internal details of process

ﬂows but are required in order for the client to cor-

rectly interact with the service.

Given the description of an executable process, its

associated interaction protocol is obtained by an ab-

straction mechanism (which masks all the internal op-

erations of the service). However the issues raised

by these two types of processes are very different. A

speciﬁcation of an executable process is close to the

deﬁnition of a program whereas the speciﬁcation of

interaction protocol mainly raises an difﬁcult prob-

lem: how to synthetize a client which will correctly

handle the interaction with the service.

The synthesis problem Indeed by construction, the

external behaviour of a service is non deterministic

due to its internal choices. It is then a priori unclear

whether a client, i.e. a deterministic program, can be

designed to interact with it. Furthermore the spec-

iﬁcation often includes timing constraints (e.g. im-

plicit detection of the withdrawal of an interaction

by the client) implying that these timing constraints

must also be taken into account by the client. How-

ever since no semantics of the interaction process is

given for BPEL (not to be confused with the seman-

tics of the service execution), this problem could not

be formally stated.

A discrete time solution (Melliti and Haddad,

2003; Haddad et al., 2004b) In this work, the au-

thors have speciﬁed what is an external behaviour, i.e.

they have given an operational semantics to an ab-

stract BPEL speciﬁcation in terms of a discrete time

transition system. The semantics is obtained by a set

of rules in a modular way. Given a constructor of the

language and the behaviour of some components, a

rule speciﬁes a possible transition of a service built

via this constructor applied on these components. As

previously discussed, the transition system is gener-

ally non deterministic.

Then they have deﬁned a relation between two

communicating systems which formalizes the concept

of a correct interaction. There are standard relations

between dynamic systems like the language equiva-

lence and the bisimulation equivalence but none of

them matches their needs. Thus they have intro-

duced the interaction relation which can be viewed

as a bisimulation relation modiﬁed in order to capture

the nature of the events (i.e. the sending of a message

is an action whereas the reception is a reaction).

Afterwards they have focused on the synthesis of

a client which is in an interaction relation with the

transition system corresponding to the system. The

client they look for must be implementable, in other

words it should be a deterministic automaton. It has

appeared that some BPEL speciﬁcations do not ad-

mit such a client i.e. they are inherently ambiguous.

Thus the algorithm they have developed either detects

the ambiguity of the Web service or generates a deter-

ministic automaton satisfying the interaction relation.

The core of this algorithm is a kind of determinisation

of the transition system of the service.

Our present contribution In the previous solution,

the discrete time semantics is preferred for simplic-

ity reasons. However such a solution has the follow-

ing drawbacks. First, the passing of a unit of time

is modelled by an explicit transition in the transition

system which means that the compact representation

of timing constraints by values is now hidden in the

model by their combination with logical transitions.

In other words, whereas handling correctly the inter-

action with the service, the client automaton is hardly

understandable by a user. Moreover if two timing

constraints are not of the same order, the time unit

must be chosen w.r.t. the shorter one leading to a

combinatory explosion of the automaton due to the

“translation” of the longer one.

Here we develop a dense time semantics for a

BPEL speciﬁcation as a timed automaton (Alur and

Dill, 1994). A preliminary version of this seman-

tics for XLANG (Thatte, 2001) was given in (Haddad

et al., 2004a). Switching from XLANG to BPEL is

relatively easy thanks to the way the operational se-

mantics is deﬁned. The construction of this automa-

ton is based on modular rules which works similarly

to the discrete case. However they are more intri-

cate since, on the one hand, the values of the timing

constraints are handled symbolically with the help of

clocks and, on the other hand, given some expression

we must determine which clocks are active and how

they govern the guards of the transitions. Next, we

revisit the interaction relation. Contrary to the previ-

ous relation, we manage explicitly the time since now

an execution is a discrete event sequence where the

events are stamped by the time of their occurrence.

The last part of the work is the most difﬁcult one. Let

us recall that the core of the former synthesis algo-

rithm for the client automaton is similar to an automa-

ton determinisation. It is well-known that the non de-

terministic timed automata are strictly more expres-

sive than the deterministic ones. Thus we have de-

signed an original procedure which decides whether

a speciﬁcation is (potentially) ambiguous and in the

negative case produces such a deterministic automa-

ton. Similarly to the approaches which determinise

subclasses of timed automata (Alur et al., 1999), we

require that the deterministic automaton has the same

clocks as those of the original one.

ICEIS 2006 - SOFTWARE AGENTS AND INTERNET COMPUTING

Related work The platform WSAT (Fu et al.,

2004a; Fu et al., 2004b) enables designers of a Web

service composition to model check properties ex-

pressed by LTL formulas with SPIN tool. The for-

mal semantics is obtained by gluing patterns for each

BPEL construction. One pattern is connected from its

ﬁnal state to the initial state of next pattern according

to the BPEL description with local transitions. This

work does not cover the time features and it focuses

only on message exchanges: the conversation is ob-

tained by a virtual watcher that is supposed to record

all messages sequences sent by each peer enrolled in

the composition.

Another research of Web services formal semantics

is based on a BPEL to Finite State Processes (FSP)

translation (Foster et al., 2003). This work lies on

message sequence charts and the core of the veriﬁca-

tion mechanism consists to check trace equivalence.

Again, the time features of the speciﬁcation are not

taken into account.

(Turner, 2005) uses the notation CRESS (Chisel

Representation Employing Systematic Speciﬁcation)

to formalise Web services. This model presents two

main advantages: automatic translation into formal

languages for analysis as well as into implementation

languages for deployment. Then the CRESS speci-

ﬁcation is translated into LOTOS and analysed with

tools like TOPO, LOLA and CADP. Again, the tem-

poral aspects are not present.

These different contributions share with our ap-

proach the design of a formal semantics for Web

services. However they study the BPEL execution

process and not the interaction protocol, they do not

include the time features of BPEL and they perform

component veriﬁcation whereas we perform compo-

nent synthesis.

Organization of the paper In section 2, we de-

scribe how to associate a formal semantics with a

business process leading to the building of a timed

automaton. Section 3 presents the client-service inter-

action relation. The synthesis of a client automaton is

described in section 4. We summarize our results in

section 5 and we present some directions for future

works.

2 A FORMAL SEMANTICS FOR

BPEL ABSTRACT PROCESSES

BPEL provides a set of operators describing in a

modular way the observable behaviour of an abstract

process. As shown in (Staab et al., 2003), this kind

of process description is close to the process alge-

bra paradigm illustrated for instance by CCS (Mil-

ner, 1989), CSP (Hoare, 1985) and ACP (Bergstra

and Klop, 1984). However, time is explicitly present

in some of the BPEL constructors and thus the stan-

dard process algebra semantics are inappropriate for

the semantics of such a process.

Thus our semantics associates a timed automaton

(TA) with an abstract process. Let us brieﬂy de-

scribe what is a TA. A TA is a (non deterministic)

ﬁnite automaton enhanced with a ﬁnite set of clocks

(C). An execution of a TA consists of (possibly null)

time steps interleaved with discrete transitions. A TA

conﬁguration is composed of a state and a value per

clock (called a clock valuation). The discrete tran-

sitions correspond to the edges between the states.

The clocks control the behaviour of the TA as fol-

lows. An elementary constraint about a clock x,is

x<v, x ≤ v,x>v, x ≥ v where v is an integer

constant. A constraint is a conjunction of elementary

constraints. The set of constraints is denoted Γ.A

constraint called an invariant is attached to each state.

Time can elapse in a state if the invariant associated

with the state is satisﬁed during all the successive con-

ﬁgurations. In addition to its label, the speciﬁcation of

an edge also includes a constraint, here called a guard,

and a subset of clocks to be reset. In order to fol-

low this edge from a conﬁguration, the corresponding

guard must be true and the clock valuation after the

reset operation must satisfy the invariant of the new

state.

Deﬁnition 1 (Timed automaton

(Alur and Dill, 1994))

A Timed Automaton (TA) is a tuple T =

(L, C, A, Inv, E, l

) where

• L is the set of locations or control states,

• C is the set of clocks,

• A is the set of actions,

• Inv a mapping from L to Γ deﬁnes the invariants,

• E ⊆ L × Γ × A × 2

× L is the set of edges.An

edge e is (s, g, a, r, d) with s the source location, g

the guard of e, a the action, r the subset of clocks

reset by e and d the destination location.

• l

is the initial location.

2.1 The Alphabet of the TA

The ﬁrst step for the deﬁning a semantics consists in

specifying the action alphabet for a BPEL process.

We have four kinds of actions:

• Silent actions, denoted by τ cannot be observed

by the client. They correspond to decisions taken

by the server (evaluation of a condition for switch,

while, etc.). The exception events set of BPEL4WS

is denoted by E

• Timeout expirations which are denoted by to.

• Sending and receiving messages: the set of types

of messages will be denoted by M. The emis-

sion is denoted by !m and the reception is denoted

CLIENT SYNTHESIS FOR WEB SERVICES BY WAY OF A TIMED SEMANTICS

by ?m. We also set !M = {!m |m ∈ M} and

?M = {?m |m ∈ M} and the wildcard ∗ may be

substituted for ! or ?.

• In order to control that the client correctly detects

the end of the service, we introduce

√

, the termi-

nation event. This action will also simplify the de-

ﬁnition of the operational semantics.

2.2 The States and the Edges of the

Each state will be associated with a BPEL process

obtained by successive transformations from the ini-

tial process. Two states have different associated

processes. At the beginning of the construction, there

is a single state (the initial one) corresponding to this

process. Each time an edge is deﬁned, a new process

is computed and if this process does not label an ex-

isting state then such a state is created. Due to the

semantic rules given in the next subsection, it can be

proved that the number of derived processes is ﬁnite

(and thus the number of states is also ﬁnite).

The edges starting from a state are obtained by

a top down analysis of the process expression la-

belling this state. This analysis is usually deﬁned

with the help of operational semantic rules. The deﬁ-

nition of a semantic rule [op

] for a generic process

P = op

,...) is given as for Algebra of

Timed Processes (Nicollin and Sifakis, 1994). Com-

ponents of a rule are:

• a boolean expression over some potential

transitions of selected components of P :

Bexp({P

o(i)

−→ P



o(i)

});

• this condition is enforced by a second condition on

the occurring labels denoted by guard({α

}).

• If the two conditions are fulﬁlled then a state tran-

sition for P is possible where the label Lexp ({α

})

is an expression depending on the labels of sub-

processes transition and

• the new process is an expression Nexp(P, {P



o(i)

})

depending on the original process and the new sub-

processes.

So, a generic rule, presented with the usual style has

the following structure:

[op

Bexp({P

o(i)

−→ P



o(i)

})

Lexp({α

})

−→ Nexp(P, {P



o(i)

})

where guard ({α

})

The guard and reset associated with an edge will

be deﬁned in the next subsection. For sake of read-

ability, we do not follow the (verbose) XML syntax

of a BPEL process. Instead we have chosen a simpli-

ﬁed syntax close to the one used for process algebra

whose meaning should be immediate for who knows

BPEL. As usual, we begin the deﬁnition of rules by

giving the ones corresponding to the basic processes

of BPEL. These basic processes are

empty, ?o[m],

!o[m] and

throw[e].

The

empty process empty can only terminate (the

notation 0 is the null process).

empty

√

−−− → 0

The ?o[m] and !o[m] processes The process ?o[m]

(which corresponds to the input operation of WSDL)

consists in receiving a message of type m. The

process !o[m] (which corresponds to the notiﬁcation

operation of WSDL) consists in sending a message of

type m. We consider only these two types of WSDL

operations. The two other types can be built with the

sequence constructor (see below).

∗o[m]

∗m

−−−−→ empty with ∗∈{?, !}

The throw process The process throw[e] raises an

exception e which must be catched in some

scope

process.

∀e ∈ E

, throw[e]

−−→ 0

The sequence process ( ; ) The process P ; Q

executes the process P then the process Q. Since

the operator “;” is associative, we safely restrict the

number of operands to two processes. The

sequence

process acts as its ﬁrst subprocess while this process

does not indicate its termination. In the latter case, the

sequence process acts as the second process can do.

∀a =

√

−−→ P



P ; Q

−−→ P



; Q

∀a,

√

−−− → and Q

−−→ Q



P ; Q

−−→ Q



where a ∈{!m, ?m,

√

,τ}

Note that if there is an action a =

√

such that P

−−→



, then P

√

−−− → cannot occur.

The

switch process The process switch[{P

}

i∈I

]

chooses to behave as one process among the set {P

Each branch of its execution is guarded by an internal

condition. Conditions are evaluated w.r.t. the order of

their appearance in the description. However since the

client has no way to predict the choice of the service,

this order is irrelevant. The main consequence is that

from the point of view of the client, this choice is non

deterministic. The switch process becomes one of

its subprocesses in a silent way. Let us note that we

have implicitly supposed that at least one condition

is fulﬁlled. In the other case, it is enough to add the

process empty as one of the subprocesses.

∀i ∈ I, switch[{P

|i ∈ I}]

−−→ P

ICEIS 2006 - SOFTWARE AGENTS AND INTERNET COMPUTING

The while process The process while[P ] iterates

an inner process as long as an internal condition is

satisﬁed. Like switch, while evaluates in a silent

way its condition. Thus we have two rules depending

on this internal evaluation.

while[P ]

−−→ P ; while[P ]

while[P ]

−−→ empty

The flow process The process flow[{P

}

i∈I

}] si-

multaneously activates a set of processes {P

}.For

the moment considering that the synchronization

primitives of BPEL are internal ones we have not yet

implemented this synchronization. Thus this paral-

lel execution is similar to a “fork-join” in the sense

that the combined process ends its interaction when

all subprocesses have completed their execution. Sub-

processes of a flow process act independently except

for one action: they simultaneously indicate their ter-

mination. In the latter case, the flow process be-

comes the null process. Furthermore internal actions

are considered as immediate and consequently the oc-

currence of such an action in a subprocess prevents

the occurrence of a delayed action (sending or recep-

tion of a message) in another subprocess.

• Individual actions:

∀a ∈ E

{τ },

∃j ∈ I, P

−−−→ P



flow[{P

|i ∈ I}]

−−−→ flow[{P

|i ∈ I\{j}} {P



}]

∀m ∈ M,

∃ j∈I, P

∗m

−−−−→P



and

∀i = j, ∀ a ∈ E

{τ }, not ∃k ∈ I, (P

−−−→)

flow[{P

|i ∈ I}]

∗m

−−−−→ flow[{P

|i ∈ I\{j}} {P



}]

• Termination:

∀i ∈ I, P

√

−−− → P



flow[{P

|i ∈ I}]

√

−−− → 0

The scope process scope(P, E) with

def

=[{(m

) |i ∈ I}, (d, Q), {(e

) |j ∈ J}]

may evolve due to P evolution, reception of a mes-

sage m

, expiration of the timeout with duration d

or occurrence of an exception e

. We note M

|i ∈ I} and E

= {e

|j ∈ J}.

• P actions: The termination exits the scope whereas

another action does not.

√

−−−→

scope(P, E)

√

−−−→ 0

−−−→ P



scope(P, E)

−−−→ scope(P



,E)

• Receiving a message m

∀i ∈ I,

∀a ∈ E

{τ,

√

}, ¬(P

−−→)

scope(P, E)

−−−−→ P

• Exception handling: which depends whether the

raised exception is catched in this scope.

∀j ∈ J,

−−−→

scope(P, E)

−−→ R

∀e/∈ E

−−→

scope(P, E)

−−→ 0

If an exception e is never catched at any level then

the process is an erroneous one which can straightfor-

wardly checked by examining whether an exception

labels an edge of the TA.

The

pick process can be viewed as a particular

case of the

scope process.

2.3 The Clocks of the TA

We associate a clock with each scope process and

a special clock (x

) for handling the immediate ac-

tions. Given a process, we determine by a top down

analysis which clocks are active, i.e. which

scope

subprocesses are activated. The invariant associated

with a state depends whether an immediate action is

possible. If it is the case, the invariant is x

=0else

the invariant is a conjunction over the active clocks

of elementary conditions x ≤ d where d is the value

deﬁned in the scope corresponding to x.

The clocks to be reset when following an edge are

simply the clocks which were inactive in the source

process and become active in the target process. x

is always reset.

There is no guard for the transitions deﬁned by

the operational rules. However, we add to each state

which owns active clocks, a set of edges labelled by

to (one per subset of active clocks which can simul-

taneously reach their bound). For each such edge the

guard speciﬁes that these active clocks have reached

their bound while the other ones have not.

2.4 The Overall TA Construction

The computation of the timed automaton of the ser-

vice can now be summarized as follows.

• It manages a set of processes to be examined and

a current version of the TA. It starts with the initial

process and a automaton reduced to a single state.

• When examining a process, it ﬁrst builds the edges

corresponding to the operational rules and for each

target process not already present in the TA, it adds

it to the set of processes to be examined.

CLIENT SYNTHESIS FOR WEB SERVICES BY WAY OF A TIMED SEMANTICS

• Then it determines the set of active clocks of the

current process. Based on this information and

the previous edges, it determines the invariant of

the state. Afterwards, it generates the “time-out”

edges.

• The information updating about the clock reset may

take place at two different moments. If an edge

points to an already encountered state then (based

on the active clocks of the two states) this informa-

tion is immediately updated. Otherwise, it will be

updated when the target state will be examined.

3 INTERACTION RELATION

It should be clear that the TA is a compact descrip-

tion of the observable behaviour of the BPEL process.

However, as brieﬂy sketched above, TA have them-

selves a formal semantics deﬁned in terms of a Timed

Transition System (TTS). A TTS over the set of ac-

tions A is a tuple (S, s

,A,→) where S is a set

of states, s

∈ S is the initial state, A is a ﬁnite

set of actions disjoint from time passing, and →⊆

S ×(A∪IR

≥0

) ×S is a set of edges. If (q, e,q



) ∈→,

we also write q

−−→ q



. q

−−→ q



with d ∈ IR

≥0

corresponds to d units of time passing. The states of

the TTS associated with a TA are simply the reach-

able conﬁgurations and its edges are either its discrete

transitions or time passing in a location.

We ﬁrst informally what should be a correct inter-

action between two TTS. As for the bisimulation re-

lation, we require a relation between pairs of states of

the two systems. Obviously the pair consisting of the

initial states should belong to this relation.

Furthermore, the states of a pair should have a co-

herent view of the next interaction steps to occur. At

ﬁrst, this implies that the relation must take into ac-

count the mutually observable steps. Thus we intro-

duce the observable transition relation of a TTS by

⇒ s



iff s

∗

aτ

∗

→ s



, s



⇒ s



iff s

∗

→ s



and s

⇒ s



iff s

τ ...τ d

→ s



with



= d.

Once it is done, we could require (like for bisimu-

lation) that if a state s of the pair (s, s



) may evolve

by an observable transition of its TTS to some new

state s

, s



should have a similar observable transi-

tion leading to a state s



which would compose with

, a new pair of consistent views.

However we need to be careful. First, if a TTS

sends a message the other one must be able to receive

the message. So it is necessary to introduce the no-

tion of complementary actions

?m =!m, !m =?m

and ∀a/∈{!m}

m∈M

∪{?m}

m∈M

a = a and to re-

quire that the synchronized evolution is obtained via

complementary actions.

But this requirement is too strong as it does not cap-

ture the different nature of the sending and reception

of a message. A sending is an action whereas a re-

ception is a reaction and will not spontaneously oc-

cur. Therefore a more appropriate relation will ﬁrst

require that if, in s belonging to the pair (s, s



), a TTS

may receive a message m, then there is a third state



of the other TTS indistinguishable from s



w.r.t.

the observable transitions which can send m and sec-

ond that in s



the other TTS can send a message (not

necessarily m). The ﬁrst condition expresses that the

former TTS is not over speciﬁed and the second one

that it will not wait indeﬁnitely for a message.

These considerations yield the following formal de-

ﬁnition.

Deﬁnition 2 (Interaction relation) Let A

(S, s

,A,→

) and A

=(S, s

,A,→

) be two

TTS. Then A

and A

correctly interact iff ∃∼

⊆ S

× S

such that:

• s

∼ s

•∀s

such that s

∼ s

– Let a/∈{?m |m ∈ M};if∃s

==⇒



, then

∃s

==⇒



with s



∼ s



and if ∃s

==⇒



then ∃s

==⇒



with s



∼ s



– Let m ∈ M;ifs

===⇒



then

∗∃s

−

===⇒

, ∃s

−

===⇒

, ∃s

===⇒



with s

∼ s

and s



∼ s



where w is a

word

∗∃s



====⇒



– Let m ∈ M;ifs

===⇒



then

∗∃s

−

===⇒

, ∃s

−

===⇒

, ∃s

===⇒



with s

∼ s

and s



∼ s



where w is a

word

∗∃s



====⇒



4 CLIENT TIMED AUTOMATON

SYNTHESIS

We are now in position to present the client synthesis

algorithm. First as the client must be implementable,

we require that it is deterministic. Second as it must

handle clocks to manage on its side the timeout of the

service, we need to express its behaviour by a TTS.

These consideration lead to choose as model for our

client a deterministic timed automaton. Last, we must

produce a TA which is in interaction relation with the

TA of the BPEL process.

Before developing we emphasize that there ex-

ist BPEL process which do not admit clients. For

instance, process switch[?o[m], ?o[m



]] internally

ICEIS 2006 - SOFTWARE AGENTS AND INTERNET COMPUTING

Figure 1: A step of the client synthesis algorithm.

chooses to receive either a message m or m



and thus

no deterministic TA can correctly interact with it since

it would imply that, in its initial state, the client should

send either m or m



while the server would wait the

other message. Note also the difference with process

switch[!o[m], !o[m



]] where a client can be easily de-

signed: just wait for either m or m



. We say that a

process is ambiguous if it does not admit a determin-

istic TA which is in interaction relation with it.

4.1 The Synthesis Algorithm

Our algorithm does not look for any deterministic TA

but restricts its search for a TA which has the same

clocks as the TA of the BPEL process. Thus when

the algorithm outputs “ambiguity”, it just means that

no TA with this constraint exists. In other words, our

procedure is not complete. However this restriction

seems to be reasonable (see the next subsection about

incompleteness of our algorithm).

The general principle of our algorithm (see ﬁgure

1) is similar to a determinisation procedure: a state of

the TA client will correspond to a subset of states of

the TA of the service (see ﬁg. 2).

More precisely, each potential state s of the TA

client is associated with a subset of states S

(s) of the

TA service which are related to s via the interaction

relation. During the construction, there is a stack of

client states to be processed. At the beginning of the

algorithm, the stack contains an initial client state s

such that S(s

)={s

}, s

being the initial state

Figure 2: Service subset of states (left) - client state (right).

Figure 3: A false detection of ambiguity.

of the service. It stops either when the stack is empty

(i.e. the client has been built) or when it has detected

the ambiguity of the service.

First, we compute the -closure by τ -transitions. If

this subset (call it S



) of service states is already asso-

ciated with a state s of the client, then the edge of the

client TA which has generated the subset is redirected

to s. Otherwise, one creates a new client state (say

snew).

We compute a subset of S



(say S



) that con-

tains only states who has not output τ-immediate-

transition.

Next, we compute the set of clocks for each state

of S



. If this clock set is not unique, then there is an

ambiguity (temporal ambiguity case) and we stop the

construction. Afterwards, we check the interaction re-

lation for discrete transitions. If it is not fulﬁlled then

we also stop the construction.

The construction of the clocks guard has two steps.

The ﬁrst one consists to copy clock guards of the

edges and clock invariants of the vertice of the TA

server and, next, the complementary transitions are

constructed.

4.2 Incompleteness of the Algorithm

As already discussed, our algorithm is incomplete.

We give now an example of a false detection (see ﬁg-

CLIENT SYNTHESIS FOR WEB SERVICES BY WAY OF A TIMED SEMANTICS

ure 3 corresponding to process switch (!o[c], scope

(!o[a], [{(b, empty)}, (4, empty), {}]) ): a process

starting by a

switch such that one branch of this

switch starts with a scope process and another

branch does not activate a timing constraint is de-

tected as an ambiguous service. Indeed in one branch

there is an active clock whereas in the other there is

none.

In a discrete time framework, the previous (com-

plete) method (Haddad et al., 2004b) produces a

client. Indeed the time elapsing is symbolized by an

action (χ) and we implicitly work at a (discrete) TTS

level. Here we work at a higher level (the TA one).

Thus incompleteness is the price to pay in order to

obtain a more compact representation of the client.

5 CONCLUSION

We have shown that the interaction with a Web service

requires a theoretical development relative to its se-

mantics. Extending a previous work in discrete time,

we have proposed in this paper a dense time semantics

for BPEL: from the deﬁnition of a service - an abstract

process - we build a timed automaton corresponding

to its formal semantics. Then we have deﬁned an

interaction relation between client and service con-

sidering them as timed transition systems. We have

also designed an algorithm synthetising a determinis-

tic timed automaton (the client) when this is possible

and detecting ambiguous service otherwise.

This approach is implemented in our framework

ICIS and will be soon reachable from the net. For sake

of simplicity, we have considered a perfect communi-

cation channel (no loss and no delay). We are cur-

rently working on the generalization of our approach

by including the speciﬁcation of the channel charac-

teristics.

REFERENCES

Alur, R. and Dill, D. L. (1994). A theory of timed automata.

Theoretical Computer Science, 126(2):183–235.

Alur, R., Fix, L., and Henzinger, T. A. (1999). Event-clock

automata: a determinizable class of timed automata.

Theoretical Computer Science, 211(1–2):253–273.

Andrews, T., Curbera, F., Dholakia, H., Goland, Y., Klein,

J., Leymann, F., Liu, K., Roller, D., Smith, D., Thatte,

S., Trickovic, I., and Weerawarana, S. (2003). Busi-

ness process execution language for web services.

Bergstra, J. and Klop, J. (1984). Process algebra for syn-

chronous communication. Information and Control,

60(1-3):109–137.

Foster, H., Uchitel, S., J.Magee, , and J.Kramer (2003).

Model-based veriﬁcation of web service composi-

tions. In Proc. of. the 18th Int. Conf. on Automated

Software Eng.

Fu, X., Bultan, T., and Su, J. (2004a). Analysis of interact-

ing bpel web services. In Proc. of the 13th Interna-

tional World Wide Web Conference (WWW’04), USA.

ACM Press.

Fu, X., Bultan, T., and Su, J. (2004b). Wsat: A tool for

formal analysis of web services. In Proc. of the 16th

International Conference on Computer Aided Veriﬁ-

cation (CAV’04).

Haddad, S., Melliti, T., Moreaux, P., and Rampacek, S.

(2004a). A dense time semantics for Web services

speciﬁcations languages. In Proc. of the 1st Int. Conf.

on Information & Communication Technologies: from

Theory to Applications (ICTTA’04), pages 647–648,

Damascus, Syria. IEEE France.

Haddad, S., Melliti, T., Moreaux, P., and Rampacek, S.

(2004b). Modelling web services interoperability. In

Proc. of the 6th Int. Conf. on Enterprise Information

Systems (ICEIS04), Porto, Portugal.

Hoare, C. (1985). Communicating Sequential Processes.

Prentice Hall, Englewood Cliffs, NJ, USA.

Juric, M. (2005). BPEL and Java. On line journal theserver-

side.com. http://www.theserverside.com/

articles/article.tss?l=BPELJava.

Juric, M., Sarang, P., and Mathew, B. (2005). Business

Process Execution Language for Web Services. Packt

Publishing.

Melliti, T. and Haddad, S. (2003). Synthesis of agents for

web services interaction. In Workshop Semantic Web

Services for Enterprise Application Integration and E-

Commerce of the Fifth International Conference on

Electronic Commerce, Pittsburgh, USA.

Milner, R. (1989). Communication and Concurrency.

Prentice-Hall, Englewood Cliffs, NJ, USA.

Nicollin, X. and Sifakis, J. (1994). The algebra of timed

processes, atp: theory and application. Inf. Comput.,

114(1):131–178.

Staab, S., van der Aalst, W., Benjamins, V., Sheth, A.,

Miller, J., Bussler, C., Maedche, A., Fensel, D., and

Gannon, D. (2003). Web services: Been there, done

that? IEEE Intelligent Systems, 18:72–85.

Thatte, S. (2001). Xlang: Web services for busi-

ness process design. World Wide Web page.

http://www.gotdotnet.com/team/xml/wsspecs/xlang-

c/default.htm.

Tidwell, D. (2000). Web services - the web’s next revolu-

tion. IBM developerWorks.

Turner, K. J. (2005). Formalising web services. In Proc.

of Formal Techniques for Networked and Distributed

Systems (FORTE 2005), volume LNCS 3731, pages

473–488, Taipei, Taiwan. Springer.

WSDL (2001). Web services description language (wsdl)

1.1. Technical report, World Wide Web Consortium.

http://www.w3.org/TR/wsdl.

ICEIS 2006 - SOFTWARE AGENTS AND INTERNET COMPUTING