Yuhong Yan
email: yuhong.yan@nrc.gc.ca

Philippe Dague

Yannick Pencolé

Marie-Odile Cordier

A Model-based Approach for Diagnosing Faults in Web Service Processes

Web services based on a service-oriented architecture framework provide a suitable technical foundation for business process management and integration. A business process can be composed of a set of Web services that belong to different companies and interact with each other by sending messages. Web service orchestration languages are defined by standard organizations to describe business processes composed of Web services. A business process can fail for many reasons, such as faulty Web services or mismatching messages. It is important to find out which Web services are responsible for a failed business process because we could penalize these Web services and exclude them from the business process in the future. In this paper, we propose a model-based approach to diagnose the faults in a Web service-composed business process. We convert a Web service orchestration language, more specifically BPEL4WS, into synchronized automata, so that we have a formal description of the topology and variable dependency of the business process. After an exception is thrown, the diagnoser can calculate the business process execution trajectory based on the formal model and the observed evolution of the business process. The faulty Web services are deduced from the variable dependency on the execution trajectory. We demonstrate our diagnosis technique with an example.

Introduction

Web services not only function as middleware for application invocation and integration, but also function as a modeling and management tool for business processes. In a Service Oriented Architecture paradigm, a business process can be composed of Web services distributed over the Internet. This kind of business processes can be flexible and optimal by using the best services from multiple companies. Various Web service process description languages are designed by standard bodies and companies. Among them, Business Process Execution Language for Web Service (BPEL4WS, denoted as BPEL after) [START_REF] Andrews | Business process execution language for web services (bpel4ws) 1.1[END_REF] is the de facto standard used to describe an executable Web service process. In this paper, we study the behavior of a business process described in BPEL.

As any other systems, a business process can fail. For a Web service process, the symptom of a failure is that exceptions are thrown and the process halts. As the process is composed of multiple Web services, it is important to find out which Web services are responsible for the failure. If we could diagnose the faulty Web services, we could penalize these Web services and exclude them from the business process in the future. The current throw-and-catch mechanism is very preliminary for diagnosing faults. It relies on the developer associating the faults with exceptions at design time. When an exception is thrown, we say certain faults occur. But this mechanism does not guarantee the soundness and the completeness of diagnosis.

In this paper, we propose a model-based approach to diagnose faults in Web service processes. We convert the basic BPEL activities and constructs into synchronized automata whose states are presented by the values of the variables. The process changes from one state to another by executing an action, e.g. assigning variables, receiving or emitting messages in BPEL. The emitting messages can be a triggering event for another service to take an action. The diagnosing mechanism is triggered when exceptions are thrown. Using the formal model and the runtime observations from the execution of the process, we can reconstruct the unobservable trajectories of the Web service process. Then the faulty Web services are deduced based on the variable dependency on the trajectories. Studying the fault diagnosis in Web service processes serves the ultimate goal of building self-manageable and self-healing business processes.

This paper is organized as follows: section 2 analyzes the fault management tasks in Web service processes and motivates the use of Model-based Diagnosis (MBD) for Web services monitoring and diagnosis; section 3 presents the principles for MBD; section 4 formally defines the way to generate an automaton model from a BPEL description; section 5 extends the existing MBD techniques for Web service monitoring and diagnosis; section 6 is the related work, and section 7 is the conclusion.

Advanced Fault Management for Web Service Processes

A Web service process can run down for many reasons. For example, a composed Web service may be faulty, an incoming message mismatches the interface, or the Internet is down. The symptom1 of a failed Web service process is that exceptions are thrown and the process is halted. The current fault handling mechanism is throw-and-catch, similar to programming languages. The exceptions are thrown at the places where the process cannot be executed. The catch clauses process the exceptions, normally to recover the failure effects by executing predefined actions.

The throw-and-catch mechanism is very preliminary for fault diagnosis. The ex-ception reports where it happened and returns some fault information. The exceptions can be regarded as associated with certain faults. When an exception is thrown, we deduce that its associated fault occurred. Customized exceptions are especially defined for this purpose. This kind of association relations rely on the empirical knowledge of the developer. It may not be a real cause of the exceptions. In addition, there may exist multiple causes of an exception which are unknown to the developer. Therefore, the current throw-and-catch mechanism does not provide sound and complete diagnosis.

For example, when a Web service throws an exception about a value in a customer order, not only the one that throws the exception may be faulty, but the one that generates these data may also be faulty. But a Web service exception can only report the Web service where the exception happens with no way to know who generated these data. In addition, all the services that modified the data should be also suspected. Not all of this kind of reasoning is included in the current fault handling mechanism. A systematic diagnosis mechanism which is based on the model of the Web service process and a solid theoretical foundation needs to be developed. This is the objective of this paper.

The diagnosis task is to determine the Web services responsible for the exceptions. These Web services will be diagnosed faulty. During the execution of a BPEL process, the exceptions come from the BPEL engine or the infrastructure below, e.g. Apache Tomcat, and Internet. We classify the exceptions into time-out exceptions and business logic exceptions.

The time-out exceptions are due to either a disrupted network or unavailable Web services. If there is a lack of response, we cannot distinguish whether the fault is in the network or at the remote Web service, except if information is transmitted by the network fault management in the first case. Since we cannot diagnose which kind of faults prevent a Web service from responding, we can do little with time-out exceptions. Indeed what can be done is more statistics at the level of process classes (and not process instances) that will be used by experts to improve the QoS.

The business logic exceptions occur while invoking an external Web service and executing BPEL internal activities. For example, mismatching messages (including the type of parameters and the number of parameters mismatching) cause the exceptions to be thrown when the parameters are passed to the remote method. BPEL can throw exceptions indicating the input data is wrong. During execution, the remote service may stop if it cannot process the request. The most common scenarios are the invalid format of the parameters, e.g. the data is not in a valid format, and the data is out of the range. The causes of the exceptions are various and cannot be enumerated. The common thread is that a business logic exception brings back information on the variables that cause the problem. In this paper, our major effort is on diagnosing business logic-related exceptions at the process instances level.

The advanced fault management mechanism serves the ultimate goal to build selfmanageable Web service processes. Fault management mechanisms can be among other self-manageable functions. Some functions related to fault management are:

• Monitoring the execution of Web service process, and record necessary and sufficient information for online/offline diagnosis. Insufficient information cannot produce correct diagnosis. In Web service processes, we need to keep a chronological record for some of the variables.

• Detecting faulty behavior. In other physical tasks, detecting needs to compare the observations with the predictions from the system description to discover the discrepancies. For Web service processes, this task is a trivial one to observe exceptions. But we can imagine to build new detectors in order to detect symptoms earlier and "closer" to the causes.

• Diagnosing the causes of exceptions. This is the major focus of this paper. See Section 5 for detail.

• Recovering from the failure effects. BPEL uses predefined compensation handlers and fault handlers to eliminate failure effects. As failure effects cannot be revealed by the empirical diagnosis mechanism in BPEL, the predefined compensation actions may not be sufficient. A more advanced recovery mechanism has to be defined, based on the model-based diagnosis developed in this paper, although it is not covered in this paper.

The Principle of Model-based Diagnosis for Discrete Event Systems

MBD is used to monitor and diagnose both static and dynamic systems. It is an active topic in both Artificial Intelligence (AI) and Control Theory communities. Automated diagnosis has been applied to all kinds of systems, such as communication systems, plant processes and automobiles. The early results in MBD are collected in (Hamscher, Console, & de Kleer, 1992). Let us briefly recall the terminology and notations adopted by the model-based reasoning community.

• SD: system description. In the AI-rooted diagnostic techniques, SD is symbolically modeled, e.g. in first-order logic sentences, and in DES as used in this paper.

• COM P S: a finite set of constants to represent the components in a system.

• System: a pair (SD, COM P S).

• D: a mode assignment to each component in the system. An assignment to a component is a unary predicate. For example, for a component c i ∈ COM P S, ¬ab(c i ) means c i working properly, and ab(c i ) means c i is in an abnormal mode.

Obviously a component has different behavior for different modes.

• Observables: the variables that can be observed/measured. For a physical system, the observables are the variables measured by sensors, or events reported by alarms, etc.

• OBS: a set of observations. They are the values of the Observables. They can be a finite set of first-order sentences, e.g. value assignments to some variables.

• Observed system: (SD, COM P S, OBS).

Diagnosis is a procedure to determine which components are correct and which components are faulty in order to be consistent with the observations and the system description. Therefore, logically, a consistency-based diagnosis is: Definition 1 D is a consistency-based diagnosis for the observed system SD, COM P S, OBS , if and only if it is a mode assignment and SD ∪ D ∪ OBS ⊥.

From Definition 1, diagnosis is a mode assignment D that makes the union of SD, D and OBS logically consistent. D can be partitioned into two parts:

• D ok which is the set of components which are assigned to the ¬ab mode;

• D f which is the set of components which are assigned to the ab mode.

Usually we are interested in those diagnoses which involve a minimal set of faults, i.e., the diagnoses for which D f is minimal for set inclusion.

if SD ∪ OBS ∪ {¬ab(C)|C ∈ CO} |= ⊥.
Similarly a minimal conflict is a conflict that is minimal for set inclusion. In [START_REF] Reiter | A theory of diagnosis from first principle[END_REF], Reiter introduces the hitting set algorithm for computing minimal diagnoses using the set of conflicts.

Definition 4 ( [START_REF] Reiter | A theory of diagnosis from first principle[END_REF]) Let C be a collection of sets. A hitting set for C is a set H ⊆ S∈C S such that H ∩ S = ∅ for each S ∈ C. A hitting set is minimal if no proper subset of it is a hitting set.

Theorem 1 ( [START_REF] Reiter | A theory of diagnosis from first principle[END_REF]) A set D ⊆ COM P S is a minimal diagnosis for SD, COM P, OBS if and only if D is a minimal hitting set for the collection of conflicts (or equivalently for the collection of minimal conflicts).

When the system description is in first order logic, the computation of all diagnoses is more generally rooted in automated reasoning, relying on prime implicates of SD ∪ OBS in the form of disjuncts of ab-literals, and on their prime implicants in the form of conjuncts of ab-literals (Hamscher et al., 1992).

When applying MBD, a formal system description is needed. Therefore, we need to study the proper formal model for Web service processes. As the interactions between Web services are driven by message passing, and message passing can be seen as discrete events, we consider the Discrete Event Systems (DES) suitable to model Web service processes. Many discrete event models, such as Petri nets, process algebras and automata, can be used for Web service process modeling. These models were invented for different purposes, but now they share many common techniques, such as symbolic representation (in addition to graph representation in some models) and similar symbolic operations. In this paper, we present a method to represent Web service processes described in BPEL as automata in Section 4. Here we introduce MBD techniques for automata. A classic definition of deterministic automaton is as below:

Definition 5 An automaton Γ is a tuple Γ = X, Σ, T, I, F where:

• X is a finite set of states;

• Σ is a finite set of events;

• T ⊆ X × Σ → X is a finite set of transitions;

• I ⊆ X is a finite set of initial states;

• F ⊆ X is a finite set of final states.

Definition 6, 7 and 8 are some basic concepts and operations about automata.

Definition 6 Synchronization between two automata Γ 1 = X 1 , Σ 1 , T 1 , I 1 , F 1 and Γ 2 = X 2 , Σ 2 , T 2 , I 2 , F 2 , with Σ 1 ∩ Σ 2 = ∅, produces an automaton Γ = Γ 1 Γ 2 , where Γ = X 1 × X 2 , Σ 1 ∪ Σ 2 , T, I 1 × I 2 , F 1 × F 2 , with: T ((x 1 , x 2 ), e) = (T 1 (x 1 , e), T 2 (x 2 , e)), if e ∈ Σ 1 ∩ Σ 2 T ((x 1 , x 2 ), e) = (T 1 (x 1 , e), x 2 ), if e ∈ Σ 1 \Σ 2 T ((x 1 , x 2 ), e) = (x 1 , T 2 (x 2 , e)), if e ∈ Σ 2 \Σ 1 Assume s = Σ 1 ∩ Σ 2 is
the joint event set of Γ 1 and Γ 2 , Γ can also be written as

Γ = Γ 1 s Γ 2 .
Example 1 In Figure 1, Γ 1 and Γ 2 are two automata. The third one Γ 3 is produced by synchronizing Γ 1 and Γ 2 . Example 2 The trajectories in the automaton Γ 3 in Figure 1 can be represented as the two formulas below, in which [ ] * means the content in [ ] repeated 0 or more times:

0 1 2 e1 e1 e2 0' 1' 2' Γ 1 Γ 2 Γ 3 = Γ 1 || Γ 2 e1 e4 0,0' 1,1' e1 e4 2,2' 0,2' e3 e2 2,0'
[(0, 0 ) e2 - → (2, 0 ) e3 - → ] * [(0, 0 ) e1 - → (1, 1 ) e4 - → (2, 2 )][ e3 - → (0, 2 ) e2 - → (2, 2 )] * , [(0, 0 ) e2 - → (2, 0 ) e3 - → ] * [(0, 0 ) e2 - → (2, 0 ) e1 - → (1, 1 ) e4 - → (2, 2 )][ e3 - → (0, 2 ) e2 - → (2, 2 )] * . Definition 8 Concatenation between two automata Γ 1 = X 1 , Σ 1 , T 1 , I 1 , F 1 and Γ 2 = X 2 , Σ 2 , T 2 , I 2 , F 2 , with Σ 1 ∩ Σ 2 = ∅ and F 1 ∩ I 2 = ∅, produces an automaton Γ = Γ 1 • Γ 2 , where Γ = X 1 ∪ X 2 , Σ 1 ∪ Σ 2 , T 1 ∪ T 2 , I 1 , F 2 ∪ (F 1 \I 2 ) .
The principle of diagnosis using DES models was founded by [START_REF] Sampath | Diagnosability of discrete-event systems[END_REF] and [START_REF] Cordier | Event-based diagnosis for evolutive systems[END_REF]. System description SD models both correct and faulty behavior of a system. Assume system description SD is an automaton Γ, and observed events in chronological order are represented as another automaton OBS. Assume the joint event set of Γ and OBS is s. In this context, we call Diagnosis the automaton produced by synchronizing Γ and OBS:

Diagnosis = Γ|| s OBS (1)
From the definition of synchronization, it is easy to prove that each trajectory in Diagnosis explains the sequence of observations in the sense that observable events in the trajectory occur in the identical chronological order as in OBS, i.e.:

Diagnosis |= OBS

(2) Therefore, Diagnosis for DES is what is called an abductive diagnosis in MBD theory.

Example 3 In Figure 1, Γ 1 is a system description in which e 2 and e 3 represent occurrences of faults which are not observable directly (otherwise, the diagnosis would be trivial). Γ 2 is an observation in which two events e 1 and e 4 are observed sequentially. The Diagnosis is Γ 3 .

It is not so easy to compute the trajectories of Diagnosis because there are several possibilities for trajectory expansion that can arise from partial observations. We need to get all the possible trajectories. For trajectory expansion, people basically use search algorithms. Other algorithms, rooted from search algorithms, can also be used. For example, planning tools and model checking tools are used for trajectory expansion. Of course, these tools have to be modified in order to get complete trajectories.

Diagnostic process is almost achieved when Diagnosis is obtained, because Diagnosis explains the observations based on SD (as an automaton Γ). If we want to obtain diagnoses {D} as mode assignments as in the consistency-based framework, we need a mapping function f : Diagnosis → {D}. Each trajectory t in Diagnosis is mapped into a D, i.e. t → D. As domain knowledge, a faulty event e f is known to be associated with a fault mode F (c i ) of some component c i , i.e. e f ↔ F (c i ) 2 . If e f is included in a trajectory t, we deduce that the correspondent fault F (c i ) occurs. Formally, Proposition 1 Assume t is a trajectory in Diagnosis, then t → D where mode assignment D is defined by D f = {c j |e f ↔ F (c j ) and e f ∈ t} (and thus D ok = {c j |c j ∈ COM P S\D f }.

As each fault event maps to a fault, practically we need only to know the set of faulty events in a trajectory:

t → {e f |e f ∈ t} (3)
From ( 3), if we know {e f }, we can easily get D f and thus D. In the following, we use {e f } to represent a D f . As there are often multiple trajectories {t i } in Diagnosis, the diagnoses {D i } are also multiple:

Proposition 2 Assume {t i } is the set of all trajectories in Diagnosis, then {t i } → {D i }, where D i f = {c j |e i f ↔ F (c j ) and e i f ∈ t i } ⊆ D i .
In general, we are interested only in minimal diagnoses, i.e. in Proposition 2 we keep only those D i f which are minimal.

Example 4 From Diagnosis Γ 3 in Figure 1, we get 2 kinds of possible sequences of faulty events:

{[e2, e3] * , [e3, e2] * }, {[e2, e3] * , e2, [e3, e2] * }.
From the above sequences, we can get three diagnoses:

{}, {e2}, {e2, e3}.

The minimal diagnosis is {}, which means no fault.

In Example 4, different trajectories give us different diagnoses. It can be no faults, or e2 (mapped to its fault), or both e2 and e3. They are all sound. Adding more observables is a way to clarify the ambiguity. To determine the observables for diagnosing a certain fault is the problem of diagnosability which is not covered in this paper. Below is another example without ambiguity:

Example 5 In Figure 2, Γ 1 is SD and Γ 2 is OBS. Γ 3 is Diagnosis.
Since e 3 is within the only trajectory, we can deduce that a fault represented by e 3 occurred.

We need to point out that the existing diagnosis methods for physical systems modeled as DES are not in general suitable for Web service processes. First, we cannot enumerate faults in Web service environments because we do not know how a Web service can be faulty if it belongs to another company. Second, it is relatively easy to keep a record for how the software is executed by recording any selected variables. In contrast, it is more difficult to insert a sensor in a physical system. Therefore it is very difficult to reconstruct the trajectories for a physical system, but it is not a key issue for

0 1 2 e1 e3 e1 e4 0' 1' 2' Γ 1 Γ 2 Γ 3 = Γ 1 || Γ 2 e1 e4 0,0' 1,1' e1 e3 0,1' 0,2' e4 Figure 2: An example of Diagnosis
diagnosing a Web service process. We will discuss the diagnosis of Web services in Section 5. Several advances have recently been made: the decentralized diagnoser approach (Pencolé & Cordier, 2005) (a diagnosis system based on several interacting DESs); the incremental diagnosis approach [START_REF] Grastien | Incremental diagnosis of discreteevent systems[END_REF]) (a monitoring system that online updates diagnosis over time given new observations); active system approaches [START_REF] Baroni | Diagnosis of large active systems[END_REF] (approaches that deal with hierarchical and asynchronized DESs); and diagnosis on reconfigurable systems [START_REF] Grastien | Extending decentralized discreteevent modelling to diagnose reconfigurable systems[END_REF]. The existing techniques, such as the diagnoser approach [START_REF] Pencolé | Incremental decentralized diagnosis approach for the supervision of a telecommunication network[END_REF] or the silent closure [START_REF] Baroni | Diagnosis of large active systems[END_REF], reconstruct the unobservable behavior of the system that are required to compute diagnoses.

4 Modeling Web Service Processes with Discrete-Event Systems

Description of the Web Service Processes

BPEL is an XML-based orchestration language developed by IBM and recognized by OASIS [START_REF] Andrews | Business process execution language for web services (bpel4ws) 1.1[END_REF]. BPEL is a so-called executable language because it defines the internal behavior of a Web service process, as compared to choreography languages that define only the interactions among the Web services and are not executable. BPEL defines fifteen activity types. Some of them are basic activities; the others are structured activities. Among the basic activities, the most important are the following:

1. the receive activity is for accepting the triggering message from another Web service;

2. the reply activity is for returning the response to its requestor;

3. the invoke activity is for invoking another Web service.

The structured activities define the execution orders of the activities inside their scopes. For example:

• Ordinary sequential control between activities is provided by sequence .

• Concurrency and synchronization between activities is provided by flow .

• Loop is provided by while .

• Nondeterministic choice based on external events is provided by pick and switch .

Execution orders are also modified by defining the synchronization links between two activities (cf. Section 4.3.3). Normally, BPEL has one entry point to start the process and one point to exit, though multiple entry points are allowed. The variables in BPEL are actually the Simple Object Access Protocol (SOAP) messages defined in Web Service Description Language (WSDL). Therefore, the variables in BPEL are objects that have several attributes (called "parts" in WSDL).

An Example: the Loan Approval Process

Example 6 The loan approval process is an example described in the BPEL Specification 1.1 [START_REF] Andrews | Business process execution language for web services (bpel4ws) 1.1[END_REF]. It is diagrammed in Figure 3. This process contains five activities (big shaded blocks). An activity involves a set of input and output variables (dotted box besides each activity). All the variables are of composite type. The edges show the execution order of the activities. When two edges are issued from the same activity, only one edge that satisfies a triggering condition (shown on the edge) will be activated. In this example, the process is triggered when a receive activity named receive1 receives a message of a predefined type. First, receive1 initializes a variable request. Then, receive1 dispatches the request to two invoke activities, invokeAssessor and invokeApprover, depending on the amount of the loan. In the case where the amount is large (request.amount >= 1000), invokeApprover is called for a decision. In the case where the amount is small (request.amount < 1000), invokeAssessor is called for risk assessment. If invokeAssessor returns with an assessment that the risk level is low (risk.level = low), a reply is prepared by an assign activity and later sent out by a reply activity. If the risk level is not low, invokeApprover is invoked for a final decision. The result from invokeApprover is sent to the client by the reply activity.

Modeling Web Services Process with Discrete-Event Systems

A Web service process defined in BPEL is a composition of activities. We are going to model a BPEL activity as an automaton. A BPEL code has a finite set of variables and a BPEL state is associated with an assignment of these variables. A BPEL activity is triggered when its initial state satisfies a finite set of triggering conditions which is a certain assignment of variables. After an activity is executed, the values of the state A BPEL state s is defined as an assignment of variables. A BPEL transition t is an operation on the state s i , i.e., (s j , post

(V 2 )) = t(s i , e, pre(V 1 )), where V 1 ⊆ V , V 2 ⊆ V , pre(V 1 ) ⊆ C
is a set of preconditions that s i has to satisfy and post(V 2 ) ⊆ C is a set of post-conditions that the successor state s j will satisfy. In another word, the transition t is triggered only when the starting state satisfies the preconditions, and the operation of this transition results in a state that satisfies the post-conditions. If a state s satisfies a constraint c, we annotate as c ∧ s. Then, the semantics of transition t is also represented as:

t : (s i ∧ pre(V 1 )) e - → (s j ∧ post(V 2 )).
Definition 9 A BPEL activity is an automaton X, Σ, T, I, F, C , where C is a constraint set that defines states X and T :

X × Σ × 2 C → X × 2 C .

Modeling Basic Activities

In the following, we enumerate the model for each basic activity.

Activity throw : {s o , s f }, {thrown}, {t}, {s o }, {s f }, C with t : (s o ∧ F ault.mode = Off ) thrown -----→ (s f ∧ F ault.mode = On) Activity wait : {s o , wait, s f }, {waiting, waited}, {t 1 , t 2 }, {s o }, {s f }, C with t 1 : (s o ∧ W ait mode = Off ) waiting -----→ (wait ∧ W ait mode = On) t 2 : (wait ∧ W ait mode = On) waited ----→ (s f ∧ W ait mode = Off )
This model is not temporal. We do not consider time, so the notion of delay is not considered in this activity.

Activity empty : {s o , s f }, {empty}, {t}, {s o }, {s f }, C t : (s o ) empty ----→ (s f )

Modeling Structured Activities

Structured activities nest other activities. We can model the structured activities as automata. Note that any automaton modeling a basic activity or a structured activity has only one initial state and one final state. In the following are the automata for the structured activities.

Sequence

A sequence can nest n activities A i in its scope. These activities are executed in sequential order. Assume

A i : S Ai , Σ Ai , T Ai , {s Aio }, {s A if }, C Ai , i ∈ {1, . . . , n}. Activity sequence : {s o , s f }∪ S Ai , {end}∪ {callA i }∪ Σ Ai , {t i }∪ T Ai , {s o }, {s f }, C Ai with t 0 : (s o ) callA1 ----→ (s A1o ) t i : (s A if ) callAi+1 ------→ (s Ai+1o ) t n : (s A nf ) end --→ (s f ) If assume s o = s A1o , s f = s A nf , and s A if = s Ai+1o , for i = [1, . . . , n -1], a short representation of sequence is the concatenation of the nested activities A 1 • A 2 • • • • A n .

Switch

Assume a switch has n case branches and one otherwise branch (see Figure 4(a)).

Assume A i : S Ai , Σ Ai , T Ai , {s Aio }, {s A if }, C Ai , i ∈ {1, . . . , n + 1}. Activity switch : {s o , s f } ∪ S Ai , {end} ∪ {switchA i } ∪ Σ Ai , {t io } ∪ {t if } ∪ T Ai , {s o }, {s f }, C Ai ∪ pre(V i ) . Assume V 1 , .
. . , V n are variable sets on n case branches, pre(V 1 ), . . . , pre(V n ) are the constraints defined by the attributes condition in case . The transitions are defined as below: Activity while :

t io : (s o ∧ ¬pre(V 1 ) ∧ • • • ∧ pre(V i ) • • • ∧ ¬pre(V n )) switchAi ------→ (s Aio ), ∀i ∈ {1, . . . n} t (n+1)o (s o ∧ ¬pre(V 1 ) ∧ • • • ∧ ¬pre(V i ) • • • ∧ ¬pre(V n )) swicthAn+1 ---------→ (s A (n+1)o ) t if : (s A if ) end --→ (s f ), ∀i ∈ {1, . . . n + 1} end S f S o S A1o S Aio S A(n+1)o S A1f event_A 1 S Aif S A(n+1)f … … switchA 1 switchA i switchA n+1 end end event_A i event_A (
{s o , s f }∪S A , {while, while end}∪Σ A , {t o , t f , t}∪T A , {s o }, {s f }, C∪ pre(W ) .
Assume W is a variable set, and pre(W ) is the constraint defined by the attribute condition in while .

t o : (s o ∧ pre(W )) while ---→ (s Ao ) t f : (s o ∧ ¬pre(W )) while end -------→ (s f ) t : (s A f ) - → (s o )
Flow A flow can nest n activities A i in its scope. These activities are executed concurrently. Assume

A i : S Ai , Σ Ai , T Ai , {s Aio }, {s A if }, C Ai , i ∈ {1, . . . , n}. Activity flow : {s o , s f } ∪ S Ai , {start, end} ∪ Σ Ai , {t io , t if } ∪ T Ai , {s o }, {s f }, C Ai with t io : (s o ) start ---→ (s Aio ) t if : (s A if ) end --→ (s f )
Notice that the semantic of automata cannot model concurrency. We actually model the n-paralleled branches into n automata and define synchronization events to build their connections. The principle is illustrated in Figure 5. At the left, each branch is modeled as an individual automaton. The entry state s o and the end state s f are duplicated in each branch. Events start and end are the synchronization events. At the right is the automaton resulted by synchronization. More complicated case in joining the paralleled branches is discussed in subsection 4.3.3. The key point in reasoning about decentralized automata is to postpone the synchronization until a synthesis result is needed, in order to avoid the state explosion problem [START_REF] Pencolé | Incremental decentralized diagnosis approach for the supervision of a telecommunication network[END_REF] (Pencolé & Cordier, 2005). In Web service diagnosis, it is the situation (cf. subsection 5.1).

Pick

Assume a pick has n onMessage and one onAlarm branches. onMessage branches are triggered by predefined events. Assume activities {A 1 , . . . , A n } are corresponding to the n branches respectively. onAlarm branch is triggered by a time-out event produced by a timer. Assume activity A n+1 is corresponding to onAlarm branch. Exactly one branch will be selected based on the occurrence of the event associated with before any others. Assume

A i : S Ai , Σ Ai , T Ai , {s Aio }, {s A if }, C Ai , i ∈ {1, . . . , n + 1}. Activity pick : {s o , s f }∪ S Ai , {start Ai }∪{end}∪ Σ Ai , {t io , t if }∪ T Ai , {s o }, {s f }, C Ai ∪ exists(event Ai ) with t io : (s o ∧ exists(event Ai )) start A i -----→ (s Aio ) t if : (s A if ) end --→ (s f ) S A2o S A1o end S A1f S A2f

Synchronization Links of Activities

Each BPEL activity can optionally nest the standard elements source and target . The XML grammar is defined as:

< source linkN ame = "ncname" transitionCondition = "bool -expr"?/ > < target linkN ame = "ncname"/ > A pair of source and target defines a link which connects two activities. The target activity must wait until the source activity finishes. Therefore, links define the sequential orders of activities. When one flow contains two parallel activities which are connected by a link, the two activities become sequentially ordered. An activity may have multiple source or target elements. Links can express richer logics, but they make the processes more difficult to analyse. source can be modeled similarly like an activity , with "transitionCondition" as the triggering condition.

Activity source : {s o , s f }, { }, {t}, {s o }, {s f }, transitionCondition with t : (s o ∧ transitionCondition) - → (s f ), When an activity is the target of multiple links, a join condition is used to specify how these links can join. The join condition is defined within the activity. BPEL specification defines standard attributes for this activity:

< activityN ame = "ncname", joinCondition = "bool -expr", suppressJoinF ailure = "yes|no"/ > t 9 : (x 7 ) received approval -------------→ (x 8 ∧ OutV ar = approval), and t e : (x 7 ) received aplError --------------→ (x 8 ∧ OutV ar = errorM essage) where Invar and OutV ar are the input and output variables. assign : {x 6 , x 9 }, {assigned}, {t 10 }, {x 6 }, {x 9 }, C with t 10 : (x 6 ) assigned ------→ (x 9 ∧ approval.accept = yes) setMessage to reply = {x 9 , x 10 }, { }, {t 11 }, {x 9 }, {x 10 }, C , with t 11 : (x 9 ) - → (x 10 ).

approval to reply = {x 8 , x 10 }, { }, {t 12 }, {x 8 }, {x 10 }, C , with t 12 : (x 8 ) - → (x 10 ).

reply : {x 10 , x 11 }, {replied}, {t 13 }, {x 10 }, {x 11 }, C with t 13 : (x 10 ∧ exists(approval)) replied ----→ (x 11 ∧ SoapM sg = approval), where SoapM sg is the message on the wire. A Web service process can run down for many reasons. For example, a composed Web service may be faulty, an incoming message mismatches the interface, or the Internet is down. The diagnosis task is to determine the Web services responsible for the exceptions. These Web services will be diagnosed faulty. In this paper, our major effort is on diagnosing business logic-related exceptions.

In our framework, COM P S is made up of all the basic activities of the Web service process considered, and OBS is made up of the exceptions thrown and the events of the executed activities. These events can be obtained by the monitoring function of a BPEL engine. A typical correct model for an activity A is thus:

¬ab(A) ∧ ¬ab(A.input) =⇒ ¬ab(A.output) (4)
For facilitating diagnosis, the BPEL engine has to be extended for the following tasks: 1) record the events emitted by executed activities; 2) record the input and output SOAP messages; and 3) record the exceptions and trigger the diagnosis function when the first exception is received. Diagnosing is triggered on the first occurred exception3 . The MBD approach developed relies on the following three steps with the techniques we introduced in the content above.

1) A prior process modeling and variable dependency analysis. All the variables in BPEL are global variables, i.e. they are accessible by all the activities. An activity can be regarded as a function that takes input variables and produces output variables. An activity has two kinds of relation to its input and output variables: defining and utilizing. We use Def (A, V ) and U til(A, V ) to present the relation that activity A defines variable V or utilizes V . An activity is normally a utilizer of its input variables, and is a definer of its output variables. This is similar to the view point of programming slicing, a technique in software engineering for software debugging (cf. Subsection 6.1). But BPEL can violate this relation by applying some business logic. For example, some variables, such as order ID and customer address, are not changeable after they are initialized in a business process. Therefore, a BPEL activity may be a utilizer of its output variables. In BPEL, it is defined in correlation sets. In this case, we use U til(A, (V 1, V 2)) to express that output V 2 is correlated to input V 1. In this case, Formula 4 can be simplified as:

¬ab(A.input) =⇒ ¬ab(A.output), if U til(A, (A.input, A.output)) (5)
In Example 8, we give a table to summarize the variable dependency for the load approval process. This table can be obtained automatically from BPEL. The approach is not presented due to lack of space.

Example 8 The variable dependency analysis for the loan approval process is in Table 1.

2) Trajectories reconstruction from observations after exceptions are detected. As mentioned earlier, the observations are the events and exceptions when a BPEL process is executed. The events can be recovered from the log file in a BPEL engine. The observations are formed in an automaton. The possible trajectories of the process are calculated by synchronizing the automaton of the observations with the automaton of the system description:

trajectories = trajectories of SD||OBS (6)
We do not require to record each event during the execution, but just enough to be able to identify the real trajectory of the process. This is very useful when some events are not observable and when there are too many events to record. Reference to Subsection 5.2 for more discussion.

Example 9 In the loan approval example, assume that OBS={received, invoked assessor, received risk, invoked approver, received aplErr} (as in Figure 7(a)). received aplErr is an exception showing that there is a type mismatch in received parameters. We can build the trajectory of evolution as below, also shown in Figure 7(b).

(x 0 ) received ------→ (x 1 ) - → (x 2 ) invoked assessor -------------→ (x 4 ) received risk ---------→ (x 5 ) - → (x 3 ) invoked approver -------------→ (x 7 ) received aplErr ------------→ (x 8 )
3) Accountability analysis for mode assignment Not all the activities in a trajectory are responsible for the exception. As a software system, the activities connect to each other by exchanging variables. Only the activities which change the attributes within a variable can be responsible for the exception.

Assume that activity A generates exception e f , and t is a trajectory ending at A. The responsibility propagation rules are (direct consequences of the contraposition of Formula 4 and 5): The first rule in (7) states that if an activity A generates an exception e f , it is possible that activity A itself is faulty, or any part in its A.InV ar is abnormal. Notice a variable is a SOAP message which has several parts. A.InV ar.part is a part in A.InV ar4 . The second rule in (8) propagates the responsibility backwards in the trajectory. It states that an activity A j ∈ t that defines a part of A i .InV ar which is known as faulty could be faulty; and its inputs could also be faulty. If there are several activities that define a part of A i .InV ar, only the last one counts, because it overrides the changes made by the other activities, i.e. A j is the last activity "between" A j and A i that defines A i .InV ar, as stated in (8). After responsibility propagation, we obtain a responsible set of activities RS = {A i } ⊆ t.

e f ∈ Σ A ab(A) ∨ {ab(A.InV ar.part)|A.InV ar.part ∈ A.InV ar} (7) ∀A i , A j ∈ t, A j = A i , A j is
The set CO = {A} ∪ {A i |A i ∈ RS} is a conflict set, because if all the components in CO are correct, there should be no exceptions. Then a diagnosis is any of A or A i in the responsible set is faulty:

{D f } = {{A}} ∪ {{A i }|A i ∈ RS} (9)
Each D f is a single fault diagnosis and the result is the disjunct of the D f . The algorithm is as following. Lines 1-2 apply rule (7). Lines 3-8 apply rule (8). This algorithm checks each activity in t. Therefore the complexity of this algorithm is O(|t|).

Example 10 For the loan approval example, we have the trajectory as in Example 9. We do the responsibility propagation. As invokeApprover generates the exception, Algorithm 1 Calculate Diagnosis for a Faulty Web Service Process INPUT: A 0 -the activity generating the exception. t -a list of activities in a reserved trajectory ending at A 0 , taken in reverse order with A 0 excluded. Variables: V -a list of faulty variable parts, initialized as {}. OUTPUT: D -the list of all possible faulty activities, initialized as {A 0 }. Notes about the algorithm: 1) list.next() returns the first element of a list; list.add(element) adds an element at the end of the list; list.remove(element) removes an element from the list. 2) Activity A has a list of input variables A.InV ars and output variables A.OutV ars. 3) a variable var has a list of parts var.P arts.

1: for each variable var in A 0 .InV ars do 2:

V.add(var.P arts)

3: while A = t.next()! = null do 4: if ∃p ∈ V, Def (A, p) then 5: D.add(A) 6: V.remove(v) 7:
for each variable var in A.InV ars do 8:

V.add(var.P arts) 9: return D according to Formula (7), invokeApprover is possibly faulty. Then its input request is possibly faulty. Among all the activities {receive1, invokeAssessor, invokeApprover} in the trajectory, receive1 defines request, invokeAssessor and invokeApprover utilize request. Therefore, receive1 is possibly faulty, according to Formula (8). receive1 is the first activity in the trajectory. The propagation stops. The diagnosis is:

{D f } = {{receive1}, {invokeApprover}}
Example 10 has two single faults {receive1} and {invokeApprover} for the exception received aplErr, which means either the activity receive1 or invokeApprover is faulty. In an empirical way, an engineer may associate only one fault for an exception. But our approach can find all possibilities. Second, if we want to further identify which activity is indeed responsible for the exception, we can do a further test on the data. For example, if the problem is wrong data format, we can verify the data format against some specification, and then identify which activity is faulty.

Multiple Exceptions

There are two scenarios where multiple exceptions can happen. The first scenario is the chained exceptions when one exception causes the others to happen. Normally the software reports this chained relation. We need to diagnose only the first occurred exception, because the causal relations for other exceptions are obvious from the chain.

The second scenario is the case when exceptions occur independently, e.g. two paralleled branches report exceptions. As the exceptions are independent, we diagnose each exception independently, the synthesis diagnoses are the union of all the diagnoses. Assume the minimal diagnoses for exception 1 are {D 1 i }, where i ∈ [1, . . . , n], and the minimal diagnoses for exception 2 are {D 2 j }, where j ∈ [1, . . . , m], the synthesis diagnoses are any combinations of D 1 i and D 2 j :

{D 1 i ∪ D 2 j |i ∈ [1, . . . , n], j ∈ [1, . . . , m]}.
What interests us most is the synthesis of the minimal diagnoses. So, we remove the D 1 i ∪ D 2 j that are supersets of other ones. This happens only if at least one activity is common to {D 1 i } and {D 2 j }, giving rise to a single fault that can be responsible for both exceptions. Such activities are thus most likely to be faulty (single faults being preferred to double faults).

Without Full Observability

Equation 6 can recover trajectories from OBS. Actually if we can record all the events in a model, trajectories are equal to OBS. It is a trivial case. The problem occurs when we do not have full observability. For example, a third party BEPL engine does not allow us to record all the events crucial for diagnosis, or the process is too large to record every event. Equation 6 gets all the possible trajectories satisfying OBS. Therefore, this method can deal with missing events. At the meantime, if there are multiple trajectories satisfying OBS, the diagnoses are the union of the diagnoses obtained from all the trajectories. This can result in a larger number of diagnoses, i.e. diagnosis is not precise.

It is a trade off between observability and diagnosability. Increasing observability, i.e. observing more events, can result in more precise diagnosis, while increasing the observing cost. It is our future work to study the minimal observables for diagnosing a fault.

Offline Diagnosability Analysis

Diagnosability analysis is normally conducted offline without executing the processes. We do not touch diagnosability analysis problems in this paper. But diagnosability is related to the method of diagnosis. Assuming an exception at a place in a BPEL process, diagnosability analysis of this exception involves to calculate all the trajectories from the process entry point to the assumed exception and find diagnoses on each trajectory. The method is similar as the three steps in Section 5, just the second step is replaced by a graph traverse algorithm to compute all the trajectories between two nodes on the graph formed by the automaton model.

Multiple Trajectories

Lack of full observability and offline diagnosability analysis can cause multiple trajectories. Assume trajectories {t 1 , ..., t n }. Using our diagnosis algorithm, each trajectory t i has conflict set CO i . But as the trajectories are the possible execution paths, they do not occur at the same time, the conflict sets are not all contradictory at the same time. Indeed only one of these trajectories, even if which one is unknown, really happened. In this case, we do not have to use hitting set algorithm to compute diagnoses. We define simply the synthesis diagnoses as the disjunction of all the diagnoses, ∨{D i }, which means diagnoses are in any of {D i }.

Obtaining the Dependency Table

The variable dependency table can be automatically constructed from BPEL. Regard a BPEL activity A as a function OutV ar = f A (InV ar). Then A is the utilizer of InV ar and definer of OutV ar. Before, we have defined A as an automaton. Then InV ar is the variables used in s o and Outvar is the variables used in s f .

Due to some business logic, some variables, such as order ID and customer address, are not changeable after they are initialized in a business process. BPEL uses correlation set to define that two variables are identical in values. The correlation set is referenced by an activity. When an activity has a correlation set within its scope, the correlation indicates if this activity initiates the variables by setting the attribute initiate. If initiate is "yes", this activity is the definer for both of the variables, otherwise, this activity is the utilizer for both of the variables.

Implementation

There are many BPEL engines in the market. We extended ActiveBPEL (Active Endpoint, 2007), an open source from Active Endpoints, to implement our diagnosis mechanism. ActiveBPEL allows us to record every executed activity and messages in the execution. These activities and messages are the observations during execution and they correspond to a subset of the events and states in our formal model. Therefore, from the synchronization of the observations and the formal model result the execution trajectories. The diagnosis function is a java package that is invoked when an exception is caught. It takes the observations and the dependency table as inputs, calculates the trajectories and uses Algorithm 1 to calculate diagnoses.

Related Work and Discussion

A Brief Comparison to Program Slicing

Program slicing is a well known technique in software engineering for software debugging [START_REF] Weise | Program slicing[END_REF]. If we have a specific program Π, a location within this program #n (n is a number given to a line), and a variable x, then a slice is itself a program that is obtained from the original program by removing all statements that have no influence on the given variable at the specified position. Since slices are usually smaller than the original program they focus the user's attention on relevant parts of the program during debugging. Slices can be computed from Program Dependence Graph (PDG) [START_REF] Ottenstein | The program dependence graph in software development environment[END_REF] as a graph reachability problem. A PDG G Π for a program Π is a direct graph. The vertices of G Π represent assignment statements and control predicates that occur in program Π. In addition G Π includes the distinguished entry vertex. The edges of the graph represent either control or data dependencies. Given a criterion n, x , the slice is computed in two steps. First, the vertex v representing the last program position before n where variable x is defined must be localized. Second, the algorithm collects all vertices that can reach v via a control or flow dependency edge. The statements represented by the collected vertices (including vertex v) are equal to the program slice for Π.

Wotawa has discussed the relationship between MBD based debugging and program slicing [START_REF] Wotawa | On the relationship between model-based debugging and program slicing[END_REF]. In his work, each statement in a program is viewed as a component with a mode, inputs and outputs. The logic representation of a statement #n is ¬ab(n) → out(n) = f (in(n)), i.e. if #n is not faulty, the output out(n) is a function of the input in(n) according to the syntax of the program. He observed that the strongly connected components in the PDG have an influence one each other. Only if all the components are not faulty, the super component composed by these components is not faulty. He defined a dependency model whose nodes are the strongly connected components in the PDG and added a logic rule to describe the relation between the super component and the components within it. Assume {s 1 , s 2 , ..., s n } are strongly connected and the name of the super component is SC, then the rule is ¬ab(s 1 ) ∧ ... ∧ ¬ab(s n ) → ¬ab(SC). With the additional rule, logic deduction can more precisely identify the faulty components. Under this kind of modeling, slices of a single variable are equivalent to conflicts in MBD. And MBD and program slicing should draw equivalent conclusions on which statements are faulty.

We consider that diagnosing Web service processes is not equivalent to program debugging. First, we are interested in the faults due to the unknown behavior of the external Web services and due to the interaction between Web services. We assume that the Web service processes are described correctly in BPEL or a Web service process description language. This implicitly excludes the structured activities to be faulty. This is equivalent to consider only data dependency in program slice. Second, though Web service process description languages are like programs, they are simpler than programs. For example, they do not use pointers or other complicated data structures as in programs, and they do not use Goto and its other restricted forms as in unstructured program. This makes it possible that diagnosing Web service processes can be simpler than diagnosing programs.

The diagnosis method developed in this paper can be compared to dynamic slicing introduced in [START_REF] Korel | Dynamic program slicing[END_REF]. Similar to our method, dynamic slicing considers the bugs should be within the statements that actually affect the value of a variable at a program point for a particular execution of the program. Their solution, following after Weiser's static slicing algorithm, solves the problem using data-flow equations, which is also similar to the variable dependency analysis presented in this paper, but not the same. An external Web service can be seen as a procedure in a program, with unknown behavior. For a procedure, we normally consider the outputs brought back by a procedure are generated according to the inputs. Therefore, in slicing, the outputs are considered in the definition set (the set of the variables modified by the statement). For Web services, we can know some parts in SOAP response back from a Web service should be unchanged, e.g. the name and the address of a client. This relation is defined as correlation set. We should point out that the variable dependency analysis in this paper is different from slicing. As a consequence, the diagnosis obtained from MBD approach in this paper can be different from slicing, and actually more precise.

As MBD approach can integrate more business logic into its model, it is less rigid than slicing. In this sense, MBD is more business oriented, not program oriented, which makes it more suitable for diagnosing Web service processes than slicing.

MBD in Diagnosing Component-based Software

Besides Wotawa's work mentioned above, some other people have applied MBD on diagnosing component-based software systems. We found that when diagnosing such systems, the modeling is rather at the component level than translating lines of statements into logic representations. Grosclaude in [START_REF] Grosclaude | Model-based monitoring of software components[END_REF]) used a formalism based on Petri nets to model the behaviors of component-based systems. It is assumed that only some of the events are monitored. The history of execution is reconstructed from the monitored events by connecting pieces of activities into possible trajectories. Console's group is working towards the same goal of monitoring and diagnosing Web services like us. In their paper [START_REF] Ardissono | Cooperative model-based diagnosis of web services[END_REF], a monitoring and diagnosing method for choreographed Web service processes is developed. Unlike BPEL in our paper, choreographed Web service processes have no central model and central monitoring mechanism. [START_REF] Ardissono | Cooperative model-based diagnosis of web services[END_REF] adopted grey-box models for individual Web services, in which individual Web services expose the dependency relationships between their input and output parameters to public. The dependency relationships are used by the diagnosers to determine the responsibility for exceptions. This abstract view could be not sufficient when dealing with highly interacting components. More specifically, if most of the Web services claim too coarsely that their outputs are dependent on their inputs, which is correct, the method in [START_REF] Ardissono | Cooperative model-based diagnosis of web services[END_REF] could diagnose almost all the Web services as faulty. Yan et al. [START_REF] Yan | Monitoring web service networks in a model-based approach[END_REF] is our preliminary work to the present one, focusing on Web service modeling using transition systems. The major work in this paper is to complete the monitoring and diagnosis methods and present the diagnosis algorithm. The syntax of modeling in this paper is improved from [START_REF] Yan | Monitoring web service networks in a model-based approach[END_REF] with simplified representation of states and explicit definition of constraints. As a result, the model for a process can be more readable and a slightly fewer states. This paper is also self-contained with MBD background and discussions on fault management tasks for Web service processes.

Related Work in Web Service Monitoring, Modeling and Composition

Several groups of researchers work on Web service monitoring frameworks. [START_REF] Baresi | Towards self-healing compositions of services[END_REF] proposes BPEL 2 which is the original BPEL with monitoring rules. Monitoring rules define how the user wants to oversee the execution of BPEL. But [START_REF] Baresi | Towards self-healing compositions of services[END_REF] does not specify the monitoring tasks. [START_REF] Mahbub | A framework for requirents monitoring of service based systems[END_REF] proposes a framework for monitoring requirements of BPELbased service compositions. Their approach uses event calculus for specifying the requirements that must be monitored. Requirements can be behavioral properties of the coordination process or assumptions about the atomic or joint behavior of the deployed services. Events, produced by the normal execution of the process, are stored in a database and the runtime checking is done by an algorithm based on integrity constraint checking in temporal deductive databases. These frameworks can be used for recording the events and messages used for diagnosis.

In addition to automata used in this paper, Petri nets and process algebra are also used as formal models for Web service processes. For example, [START_REF] Salaün | Describing and reasoning on web services using process algebra[END_REF][START_REF] Ferrara | Web services: a process algebra approach[END_REF][START_REF] Viroli | Towards a formal foundation to orchestration languages[END_REF] map BPEL into different Process Algebra; [START_REF] Ouyang | Formal semantics and analysis of control flow in ws-bpel[END_REF][START_REF] Schmidt | A petri net semantic for bpel: validation and application[END_REF] present different semantics of BEPL in Petri nets; [START_REF] Fisteus | Formal verification of bpel4ws business collaborations[END_REF][START_REF] Foster | Model-based verification of web service compositions[END_REF][START_REF] Fu | Analysis of interacting bpel web services[END_REF]) use automata to model BPEL for verification. These models have similar expression power and similar reasoning or computing techniques.

Web service composition techniques are relevant to this paper because they generate new Web service processes. AI planning methods are the most commonly used techniques for Web service composition. [START_REF] Narayanan | Simulation, verification and automated compostion of web services[END_REF] starts from DAML-S descriptions and automatically transforms them into Petri nets. Other works, as [START_REF] Berardi | Automated composition of e-services that export their behavior[END_REF][START_REF] Lazovik | Planning and monitoring the execution of web service requests[END_REF][START_REF] Pistore | Automated composition of web services by planning at the knowledge level[END_REF], rely on transition rules systems. [START_REF] Rao | A survey of automated web service composition methods[END_REF]) is a survey paper on automated Web service composition methods. Re-planning is relevant to this paper because it can be used to modify the Web service processes for fault recovery. [START_REF] Canfora | Qos-aware replanning of composite web services[END_REF] presents a re-planning technique based on slicing techniques. When the estimated QoS metrics are not satisfied, the re-planning selects other Web services to replace the ones in the process.

Conclusion

Web services are the emergent technology for business process integration. A business process can be composed of distributed Web services. The interactions among the Web services are based on message passing. To identify the Web services that are responsible for a failed business process is important for e-business applications. Existing throw-and-catch fault handling mechanism is an empirical mechanism that does not provide sound and complete diagnosis. In this paper, we developed a monitoring and diagnosis mechanism based on solid theories in MBD. Automata are used to give a formal modeling of Web service processes described in BPEL. We adapted the existing MBD techniques for DES to diagnose Web service processes. Web service processes have all the features of software systems and do not appear to function abnormally until an exception is thrown and they are stopped, which makes the diagnosis principle different from diagnosing physical systems. The approach developed here reconstructs execution trajectories based on the model of the process and the observations from the execution. The variable dependency relations are utilized to deduce the actual Web services within a trajectory responsible for the thrown exceptions. The approach is sound and complete in the context of modeled behavior. A BPEL engine can be extended for the monitoring and diagnosis approach developed in this paper.

Figure 1 :

 1 Figure 1: An example of synchronization

Figure 3 :

 3 Figure 3: A loan approval process. Activities are represented in shaded boxes. The inV ar and outV ar are respectively the input and output variables of an activity.

  Activity receive : {s o , s f }, {received}, {t}, {s o }, {s f }, C with t : (s o ∧ SoapM sg.type = M sgT ype) received ------→ (s f ∧ RecM sg = SoapM sg), where M sgT ype is a predefined message type. If the incoming message SoapM sg has the predefined type, RecM sg is initialized as SoapM sg. Activity reply : {s o , s f }, {replied}, {t}, {s o }, {s f }, C with t : (s o ∧ exists(RepM sg)) replied ----→ (SoapM sg = RepM sg ∧ s f ), where exists(RepM sg) is the predicate checking that the replay message RepM sg is initialized. SoapM sg is the message on the wire. Activity invoke Synchronous invocation: {s o , wait, s f }, {invoked, received}, {t 1 , t 2 }, {s o }, {s f }, C with t 1 : (s o ∧ exists(InV ar)) invoked -----→ (wait), and t 2 : (wait ∧ SoapM sg.type = M sgT ype) received ------→ (s f ∧ exists(OutV ar)) where InV ar and OutV ar are the input and output variables. Asynchronous invocation: {s o , s f }, {invoked}, {t}, {s o }, {s f }, C with t : (s o ∧ exists(InV ar)) invoked -----→ (s f ), asynchronous invocation does not wait for a return message. Activity assign : {s o , s f }, {assigned}, {t}, {s o }, {s f }, C with t : (s o ∧ exists(InV ar)) assigned ------→ (s f ∧ OutV ar = InV ar)

  The automaton for switch . (b)The automaton for while .

Figure 4 :

 4 Figure 4: The automata for switch and while

Figure 5 :

 5 Figure 5: Build concurrency as synchronized DES pieces. (a) Concurrency branches for DES pieces; (b) The joint DES model.

Figure 6 :

 6 Figure 6: Automaton modeling loan approval process

Figure 7 :

 7 Figure 7: (a) the observations; (b) the loan approval process evolution trajectory up to the exception.

  Definition 2 A diagnosis D is minimal if and only if there is no other diagnosis D for SD, COM P S, OBS such that D f ⊂ D f . Definition 3 A set CO ⊆ COM P S is a conflict for SD, COM P S, OBS , if and only

	The dual concept of a diagnosis is a conflict.

Table 1 :

 1 The variable dependency analysis for the loan approval process.

	Variables	Parts	Definer	Utilizer
	request	firstname	receive1	invokeAssessor, invokeApprover
		lastname	receive1	invokeAssessor, invokeApprover
		amount	receive1	invokeAssessor, invokeApprover
	risk	level	invokeAssessor
	approval accept	assign, invokeApprover reply
	error	errorCode invokeApprover

In diagnosis concept, sympton is an observed abnormal behavior, while fault is the original cause of a sympton. For example, an alarm from a smoke detector is a symptom. The two possible faults, a fire or a faulty smoke detector, are the causes of the symptom.

F (c i ) is a specific fault mode. When we do not know a specific fault mode, we use ab(c i ) to represent c i is faulty.

When a Web service engine supports multiple instances of a process, different instances are identified with a process ID. Therefore, diagnosis is based on the events for one instance of the process.

Sometimes, the exception returns the information about the part A.InV ar.part is faulty. Then this rule is simplified.

where joinCondition is the logical OR of the liveness status of all links that are targeted at this activity. If the condition is not satisfied, the activity is bypassed, and a fault is thrown if suppressJoinF ailure is no.

In this case, the synchronization event end as in Figure 5(a) is removed. If the ending state of flow is the starting state s o of the next activity, the precondition of s o is the joinCondition. For example, either of the endings of the two branches can trigger the next activity can be represented as:

Modeling the Loan Approval Process

In this section, we present the complete DES model for the process in Example 6.

Example 7 The loan approval process in Example 6 contains five activities: receive1 , invokeAssessor , invokeApprover , assign , reply . The five activities are contained in a flow . Six links, receive to assess , receive to approval , assess to setMessage , assess to approval , approval to reply , and setMessage to reply , connect the activities and change the concurrent orders to sequential orders between the activities. In this special case, there are actually no concurrent activities. Therefore, for clarity, the event caused by flow is not shown. Assume the approver may return an error message due to an unknown error. Below is the formal representation of the process (also reference to Figure 6). receive1 = {x 0 , x 1 }, {received}, {t 1 }, {x 0 }, {x 1 }, C , with t 1 : (x 0 ∧ SoapM sg.type = M sgT ype) received ------→ (x 1 ∧ request = SoapM sg), where M sgT ype is a predefined message type. If the incoming message SoapM sg has the predefined type, request is initialized as SoapM sg.

receive to assess = {x 1 , x 2 }, { }, {t 2 }, {x 1 }, {x 2 }, C , with t 2 : (x 1 ∧ request.amount < 1000) - → (x 2 ).

invokeAssessor = {x 2 , x 4 , x 5 }, {invoked assessor, received risk}, {t 4 , t 5 }, {x 2 }, {x 5 }, C with t 4 : (x 2 ∧ InV ar = request)

invoked assessor -------------→ (x 4 ), and t 5 : (x 4 ) received risk ---------→ (x 5 ∧ OutV ar = risk) where InV ar and OutV ar are the input and output variables.

assess to setMessage = {x 5 , x 6 }, { }, {t 6 }, {x 5 }, {x 6 }, C , with t 6 : (x 5 ∧ risk.level = low) - → (x 6 ).

assess to approval = {x 5 , x 3 }, { }, {t 7 }, {x 5 }, {x 3 }, C , with t 7 : (x 5 ∧ risk.level = high) - → (x 3 ). invokeApprover = {x 3 , x 7 , x 8 }, {invoked approver, received approval, received aplError}, {t 8 , t 9 , t e }, {x 3 }, {x 8 }, C with t 8 : (x 3 ∧ InV ar = request) invoked approver -------------→ (x 7 ), and