Keywords

1 Introduction

With the great success of Service Oriented Computing (SOC) [1], web services are becoming the main model for automated interaction between distributed systems on the Web. SOC is based on the composition of several services that are typically designed to interact with other web services through the Internet to form larger applications. Standard web service framework are essentially based on three technologies: SOAP [2], WSDL [3] and UDDI [4]. The WSDL (Web Service Description Language) provides an abstract language to describe messages to be exchanged between services. The SOAP (Simple Object Access Protocol) is a protocol for exchanging structured information between the involved parties and the UDDI (Universal Description Discovery and Integration) is used to publish and discover web services.

Having the possibility of constructing new web services by composing existing ones has opened a new interesting prospective and has significantly influenced the way industrial applications are developed. BPEL (Business Process Execution Language) [6] is the standard of web services composition and orchestration. Among the interesting features of this expressive language, we found the fault and the compensation handling mechanism. In fact, sometime it is useful to give the end-users the possibility to cancel some services if other fails. For example, if Alice wants to book a plane ticket and a hotel for a given period of time but after booking the hotel she does not find an appropriate plane ticket, then it is desirable to allow her to cancel the hotel reservation. Compensation are introduced in BPEL to give the possibility to remedy a situation where an activity of a group fails whereas others terminated with success.

Even if the global ideas of the fault handler and the compensation handler are clear, it remains that there are a large number of particular cases that need to be handled: Which fault handler catches which error? Which compensation handler needs to be called after a given error? Which activities need to be stopped when an error occurs? What happens if an error occurs during a compensation? What happens if an error occurs in a fault handler itself? These are only a part of the particular situations that need to be clarified. Combined with other features, like event handler and termination handler, the number of these kind of questions explode justifying the urgent need of a suitable formalization for BPEL.

Contribution: The main contribution of this paper is a detailed formalization of the EFCT of BPEL, that address the above questions, based on a dedicated process algebra endowed with a small step operational semantics.

The remainder of this paper is organized as follows. Section 2 presents a simplified language that abstracts BPEL for XML syntax and formalizes it. Section 3 gives some related work. Finally, some concluding remarks are given in Sect. 4.

2 BPEL Formalisation

2.1 Syntax of AV-BPEL: Abstracted Version BPEL

Let b be a metavariable that ranges over Boolean expressions and Exp ranges over classical expressions like arithmetic and string expressions. The syntax of AV-BPEL, a fragment of BPEL that is abstracted from XML syntax, is given by the BNF grammar given in Table 1.

Table 1. Syntax of BPEL.
Full size table

A basic activity A contains an empty process (NOP action) 1, an exit process 0, a Boolean expression b, an assignment expression \(x:=Exp\), a throw action \(\Rsh _e\), a send action \(a!\overrightarrow{v} \) and a receive action \(a?\overrightarrow{x}\).

A composed activity S can be any basic activity in A, a different composition of two activities or or a scope \(<\mathcal{E},F,C,T,E,S>_n\).

A process Pr (either \(<\mathcal{E}, F,E,S>_n\) or \(<\mathcal{E}, F,E, I>_n\)) has a name n, a running environment \(\mathcal{E}\), a fault handler F an event handler E and either a normal activity S or an instantiation bloc I.

An instantiation bloc I allows a service to fork an activity when a request of an operation is received (\(a?\overrightarrow{x} \)).

An event handler E always starts by waiting for some event (receiving a message or an alarm based on a “timing out”).

A compensation handler (respectively a termination handler) can be a basic activity, an indication to compensate a particular scope \(\$_n\) or \(\$\), an indication to compensate all the reached scopes that terminated with success. It can also be a root scope RS (similar to a normal scope except that it cannot contains a compensation handler itself.).

A fault handler can be a basic activity, a catch for a named error (\(\Lsh _e\)), a catch all \(\Lsh \), an indication to compensate a particular scope \(\$_n\) or \(\$\), an indication to compensate all the reached scopes that terminated with success. It can also be a root scope RS.

Besides the above constructors, we introduce a deployment D that does not belongs to the syntax of BPEL, it is useful to formalize asynchronous communications where the sent action is not blocking whereas the receiving is blocking.

2.2 Semantics

Let \(\mathcal{D}\) be set of all possible deployments, and let P , Q and R range over \(\mathcal{D}\). The operational semantics of AV-BPEL is defined by the transition relation \(\longrightarrow \in {\mathcal D} \times \mathcal{A} \times \mathcal{D}\). Table 3 gives some standard rules that are true for all deployments P, \(P_1\), Q and \(Q_1\). Also, it uses the equivalent relation \(\equiv \in \mathcal{D} \times \mathcal{D}\) defined by Table 2.

Table 2. Axiom of BPEL.
Full size table

We denote by \(<\mathcal{E}, F,C^?,T^?,E,P>_n\) a root scope or a process, i.e., the termination handler and the compensation handler are optional.

Table 3. Classical Rules for \(\longrightarrow \).
Full size table

\(\bullet \) Communication: Sending values \(\overrightarrow{v}\) on a channel a, denoted by \(a!\overrightarrow{v}\), is not a blocking action and its produces a floating message, denoted by \(a\!\uparrow \!\overrightarrow{v}\), meaning that the message has not been received yet. Receiving messages on a channel a, denoted by \(a?\overrightarrow{x}\) is however always blocking until seeing a floating message \(a\!\uparrow \!\overrightarrow{v}\) such that the correlation values in \(\overrightarrow{x}\) match with the correlation values in \(\overrightarrow{v}\). This matching is denoted by \(\overrightarrow{v}\sqsubseteq \overrightarrow{x}\), where \((x_1,\ldots ,x_n)\sqsubseteq (v_1,\ldots ,v_n)\) if \(x_i=v_i\) or \(x_i\) is a variable (i.e., there exists a substitution \(\sigma \) from variables to values such that \(\sigma (\overrightarrow{x})=\overrightarrow{v}\).).

To formalize this asynchronous communication, we introduce the relation \(-\!\!\!\twoheadrightarrow \in {\mathcal D} \times \mathcal{A} \times \mathcal{D}\) that aims to show whether a process is ready to perform an action. This relation is not blocking even for the reception as shown in Table 4.

Table 4. Definition of \(-\!\!\!\twoheadrightarrow \).
Full size table

Now, the communication rules are formalized as shown hereafter.

$$(R_{Exp}^1) \frac{\displaystyle { P~~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{x:=Exp}~~ Q}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_{n}^{m}~~~\mathop {\longrightarrow }\limits ^{\tau } ~~~<\mathcal{E}\dagger [x\mapsto v],F,C^?,T^?,E,Q>_{n}^{m'}} } \llbracket \mathcal{E}(Exp) \rrbracket =v$$
$$(R_{b}^1) \frac{\displaystyle { P~~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{b}~~ Q}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_{n}^{m}~~~\mathop {\longrightarrow }\limits ^{\tau } ~~~<\mathcal{E},F,C^?,T^?,E,Q>_{n}^{m'}} } \llbracket \mathcal{E}(b) \rrbracket =1$$
$$(R_\uparrow ^!) \frac{\displaystyle { P~~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{a\!\uparrow \!\overrightarrow{v}}~~ Q}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_{n}^{m}~~~\mathop {\longrightarrow }\limits ^{\mathcal{E}(a)\!\uparrow \!\overrightarrow{\mathcal{E}(v)}} ~~~<\mathcal{E}',F',C'^?,T'^?,E',Q>_{n}^{m'}\Vert ~\mathcal{E}(a)\!\uparrow \!\overrightarrow{\mathcal{E}(v)}} } $$
$$(R_\uparrow ^?) \frac{\displaystyle { P~~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{a?\overrightarrow{x}}~~ Q\quad D \mathop {-\!\!\!\twoheadrightarrow }\limits ^{a\!\uparrow \!\overrightarrow{v}} D' }}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_{n}^{m}\Vert ~D ~~~\mathop {\longrightarrow }\limits ^{a?\overrightarrow{v}} ~~~<\mathcal{E}\dagger (\overrightarrow{x}\mapsto \overrightarrow{v}),F,C^?,T^?,E,Q>_{n}^{m'}\Vert ~D'} } \overrightarrow{v}\sqsubseteq \overrightarrow{x}$$

where \(m, m' \in \{ F,C, FT0, FT1, TC,\}\), and \(\llbracket - \rrbracket \) is a function that evaluates an expression (Boolean expression, arithmetic expression, string expression, etc.). For the moment, we are not interested by having more details about it. The operator \(\dagger \) is defined as follows:

$$\mathcal{E}\dagger (x\mapsto v)(y)=\left\{ \begin{array}{ll} \mathcal{E}(y) &{} \text{ if } y\ne x\\ v &{} \text{ if } y= x\ \end{array}\right. $$

\(\bullet \) Creating an Instance of a Process: The sysntax of BPEL gives two possibilities to explicitly specify the fact that we want to create an instance of a process when a message is received: first with the parameter createInstance=YES used within the definition of a “Receive” action. This case is transformed to \((a?\overrightarrow{x})^+\) in our syntax. Or by using a “Pickup” activity that contains only “OnMessage” (same as Receive, but it does not have the createInstance option). This case is specified by \((\sum _{i\in \varTheta }a_i?x_i.S_i)^+\) in our abstracted syntax.

The operational rule showing the creation of an instance are as shown here after.

$$(R_+^4) \frac{\displaystyle { I ~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{(a?\overrightarrow{x})^+} ~I' ~~~~ D ~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{a\!\uparrow \!\overrightarrow{v} } ~D'}}{\displaystyle {<\mathcal{E},F,E,I>_{n}^{m}\Vert ~D ~~~\mathop {\longrightarrow }\limits ^{a?\overrightarrow{v}} ~~~<\mathcal{E},F,E,I>_{n}^{m}\Vert <\mathcal{E}'\dagger (\overrightarrow{x}\mapsto \overrightarrow{v}),F',E',I'>_{n}^{m'}\Vert ~D'} } \overrightarrow{v}\sqsubseteq \overrightarrow{x}$$

\(\bullet \) Principal Activity: Some basic rules showing the evolution of an activity are shown by Table 3. Further behaviors are dictated by specific rules described hereafter.

  • Each error thrown by the principal activity should be caught by the fault handler of the same scope.

    $$\begin{aligned} (R_{A}^2) \frac{P \mathop {\longrightarrow }\limits ^{\Rsh _{e}} Q \quad F \mathop {\longrightarrow }\limits ^{\Lsh _{e}} F'}{<\mathcal{E},F,C^?,T^?,E,P>_n^{FT} \mathop {\longrightarrow }\limits ^{\tau } <\mathcal{E},F',C^?,T^?,E,Q>_n^{FT0} } \end{aligned}$$

  • If a throw \(\Rsh _{e}\) doesn’t have a dedicated catch in the fault handler, then it should be handled by the “catch all” activity.

    $$(R_{A}^3) \frac{\displaystyle {P \mathop {\longrightarrow }\limits ^{\Rsh _{e}} Q \quad F~~ \mathop {\not \!\!\!\longrightarrow }\limits ^{\Lsh _{e}} \quad F \mathop {\longrightarrow }\limits ^{\Lsh } F'}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n \mathop {\longrightarrow }\limits ^{\tau } <\mathcal{E},F',C^?,T^?,E,Q>_n^{FT0} } } $$

  • If there is neither a specific catch nor a “catch all” activity for a specific error, the fault handler execute the “Compensate all” activity (\(\$\)).

  • When the principal activity of a scope terminates with success, the scope is stored, in a compensation mode, for an eventual future compensation.

    $$(R_{A}^5) \frac{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n \mathop {\longrightarrow }\limits ^{a}<\mathcal{E}',F',C,T'^?,E',1>_n}}{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n.S \mathop {\longrightarrow }\limits ^{a} S.<\mathcal{E}',F',1,T'^?,E',C>_n^C } } $$
    $$(R_{A}^6) \frac{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n \mathop {\longrightarrow }\limits ^{a}<\mathcal{E}',F',C,T'^?,E',1>_n}}{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n \mathop {\longrightarrow }\limits ^{a} <\mathcal{E}',F',1,T'^?,E',C>_n^C } } $$

  • In a compensation mode, a scope is executed like in a normal mode, except that we do not need to store it anymore when it terminates with success. More precisely:

    • If the activity didn’t finished yet, the compensation mode behaves like normal mode.

      $$(R_{C}^1) \frac{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n \mathop {\longrightarrow }\limits ^{a}<\mathcal{E}',F',C',T'^?,E',Q>_n }}{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n^C \mathop {\longrightarrow }\limits ^{a} <\mathcal{E}',F',C',T'^?,E',Q>_n^C} } Q\ne 1 $$

    • If the activity of the compensation mode terminates, the scope is uninstalled.

      $$(R_{C}^2) \frac{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n \mathop {\longrightarrow }\limits ^{a}<\mathcal{E}',F',C',T'^?,E',1> }}{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n^C \mathop {\longrightarrow }\limits ^{a} 1} } $$

\(\bullet \) Fault Handler, Termination Handler and Compensation Handler: When an error occurs during the execution of the main activity of a scope, the control is passed to the fault handler which executes a list of treatments in the following order:

  1. 1.

    It stops all the running activities of the scope by the help of the relation \(\longrightarrow _t\). The termination produces always a silent action \(\tau \).

    $$(R_{FT}^1) \frac{\displaystyle {P \mathop {\longrightarrow _t}\limits ^{\tau } Q }}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^{FT0}~~\mathop {\longrightarrow }\limits ^{\tau } ~~<\mathcal{E},F,C^?,T^?,E,Q>_n^{FT0} } } $$

    • Stopping a scope consists on terminating its principal activity.

      $$(R_{T}^1) \frac{\displaystyle {P \mathop {\longrightarrow _t}\limits ^{\tau } Q }}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n~~\mathop {\longrightarrow _t}\limits ^{\tau } ~~<\mathcal{E},F,C^?,T^?,E,Q>_n } } $$

    • Terminating two parallel activities turns to terminate each one of them.

      $$(R_{T}^2) \frac{\displaystyle {P_1 \mathop {\longrightarrow _t}\limits ^{\tau } Q_1 }}{\displaystyle {P_1\Vert P_2~~\mathop {\longrightarrow _t}\limits ^{\tau } ~~Q_1\Vert P_2 } } $$

    • Terminating an iterative activity consists in removing its code.

      $$(R_{T}^3) \frac{\displaystyle {\Box }}{\displaystyle {P_1^*P_2~~\mathop {\longrightarrow _t}\limits ^{\tau } ~~1} } $$

    • Stopping a sequence turns to remove all it code except those related to a compensation.

      $$(R_{T}^4) \frac{\displaystyle {}}{\displaystyle {P_1.P_2~~\mathop {\longrightarrow _t}\limits ^{\tau } ~~P_2} } P_1\ne <\mathcal{E},F,C^?,T^?,E,1>$$
  2. 2.

    Once an activity is stopped, the termination handler of the scope is executed.

    $$(R_{T}^6) \frac{\displaystyle {P~~ {\not \!\!\!\longrightarrow _t} }}{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n^{FT0}~~\mathop {\longrightarrow }\limits ^{\mathcal{E}(a)} ~~<\mathcal{E}\dagger a,F',C,T^?,E,P>_n^{FT1} } } $$

    • The termination handler can compensate activities

      • The activity of a compensation handler is executed via the relation \(\longrightarrow _c\) and it can be invoked only by a fault handler, a termination handler or another compensation handler.

        $$(R_{TC}^2) \frac{\displaystyle {<\mathcal{E},F,C^?,T,E,P>_n^{C}~~\mathop {\longrightarrow _c}\limits ^{a} ~~<\mathcal{E}',F',C '^?,T',E',Q>_n^{C} }}{\displaystyle {<\mathcal{E},F,C^?,T,E,P>_n^{TC}~~\mathop {\longrightarrow }\limits ^{a} ~~<\mathcal{E}',F',C '^?,T',E',Q>_n^{TC} } } a\ne \Rsh _n \text{ and } Q\ne 1 $$

      • Once the compensation is successfully terminated, the control is turned back to the calling activity (fault handler).

        $$(R_{TC}^3) \frac{\displaystyle {<\mathcal{E},F,C^?,T,E,P>_n^{C}~~\mathop {\longrightarrow _c}\limits ^{a} 1 }}{\displaystyle {<\mathcal{E},F,C ^?,T,E,P>_n^{TC}~~\mathop {\longrightarrow }\limits ^{a} ~~<\mathcal{E},F,C^?,T,E,1>_n^{TF1} } } a\ne \Rsh _e$$

      • If an error occurs during the execution of a compensation handler, its remaining activity is ignored and the control is turned back to the calling fault handler without reporting it.

        $$(R_{TC}^4) \frac{\displaystyle {<\mathcal{E},F,C^?,T,E,P>_n^{C} \mathop {\longrightarrow _c}\limits ^{\Rsh _n} S' }}{\displaystyle {<\mathcal{E},F,C ^?,T,E,P>_n^{TC}~~\mathop {\longrightarrow }\limits ^{\tau } ~~<\mathcal{E},F,C^?,1,E,1>_n^{F} } } $$

    • The termination handler can run activities others than calling a compensation handler, but it can never signal an error.

      $$(R_{TC}^5) \frac{\displaystyle {<\mathcal{E},F,C ^?,T^?,E,T>_n~~\mathop {\longrightarrow }\limits ^{a} ~~<\mathcal{E}',F,C^?,T^?,E,T'>_n }}{\displaystyle {<\mathcal{E},F,C^?,T,E,P>_n^{FT1}~~\mathop {\longrightarrow }\limits ^{ a} ~~<\mathcal{E}' ,F,C,T',E,P>_n^{FT1} } } a\ne \Rsh _e$$
  3. 3.

    Once the termination handler finished, the fault handler runs it own activity.

    $$(R_{F}^5) \frac{\displaystyle { T ~~ {\not \!\!\!-\!\!\!\twoheadrightarrow } }}{\displaystyle {<\mathcal{E},F,C^?,T,E,P>_n^{FT1}~~\mathop {\longrightarrow }\limits ^{\tau } ~~<\mathcal{E},F,C^?,T,E,P>_n^{F}} } $$

    • The fault handler can compensate an activity if this is specified in its activity.

      where

      $$P^{-1}=\left\{ \begin{array}{ll} Q^{-1}.a &{} \text{ if } P=a.Q\\ Q^{-1}+R^{-1} &{} \text{ if } P=Q+R\\ Q^{-1}~\Vert ~R^{-1} &{} \text{ if } P=Q~\Vert ~R\\ P&{} \text{ else } \end{array}\right. $$

      • The code of the compensation handler is executed by the relation \(\longrightarrow _c\).

        $$(R_{FC}^2) \frac{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^{C}~~\mathop {\longrightarrow _c}\limits ^{a} ~~<\mathcal{E}',F',C'^?,T'^?,E',Q>_n^{C}}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^{FC}~~\mathop {\longrightarrow }\limits ^{a} ~~<\mathcal{E}',F',C'^?,T'^?,E',Q>_n^{FC} } } a\ne \Rsh _e \text{ and } Q\ne 1 $$

      • Once a compensation handler terminate with success, the fault handler continues its activity.

        $$(R_{FC}^3) \frac{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^{C}~~\mathop {\longrightarrow }\limits ^{a} ~~ 1 }}{\displaystyle {<\mathcal{E},F,C ^?,T^?,E,P>_n^{FC}~~\mathop {\longrightarrow }\limits ^{\mathcal{E}(a)} ~~<\mathcal{E}\dagger a,F,C^?,T^?,E,1>_n^F } } a\ne \Rsh _e$$

    • A fault handler can run activities different from compensations.

      $$(R_{F}^1) \frac{\displaystyle {<\mathcal{E},F,C ^?,T^?,E,F>_n~~\mathop {\longrightarrow }\limits ^{a} ~~<\mathcal{E}',F,C^?,T^?,E,F'>_n }}{\displaystyle {<\mathcal{E},F,C ^?,T^?,E,P>_n^{F}~~\mathop {\longrightarrow }\limits ^{a} ~~<\mathcal{E}',F',C^?,T^?,E,P>_n^F } } a \ne \Rsh _e$$

    • A process or a scope that produces an error fails (i.e. becomes 0) regardless of its fault handler terminates with success or not as shown here after.

      • If an error occurs inside a compensation handler, the fault handler propagates it to the parent scope and the current scope fails.

        $$(R_{FC}^4) \frac{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^{C}~~ \mathop {\longrightarrow _c}\limits ^{\Rsh _e} Q \quad }}{\displaystyle {<\mathcal{E},F,C,T^?,E,P>_n^{FC}~~\mathop {\longrightarrow }\limits ^{\Rsh _e} ~~0} } $$

      • If an error occurs inside a fault handler itself, the error is propagated to the parent scope.

        $$(R_{F}^2) \frac{\displaystyle {F \mathop {\longrightarrow }\limits ^{\Rsh _e} F'}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^F~~\mathop {\longrightarrow }\limits ^{\Rsh _e} ~~0 } } $$

      • If a fault handler terminates with success, its scope or process terminates in a fail mode (0).

        $$(R_{F}^3) \frac{\displaystyle {F \mathop {\longrightarrow }\limits ^{a} 1}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_n^F~~\mathop {\longrightarrow _c}\limits ^{\mathcal{E}(a)} ~~0 } } a\ne \Rsh _e$$

\(\bullet \) Event Handler:

  • Once an event is received, the activity of it corresponding event handler is executed in parallel with the principal activity of the scope.

    $$(R_{E}) \frac{\displaystyle { E~~\mathop {-\!\!\!\twoheadrightarrow }\limits ^{a?\overrightarrow{x}}~~ E' \quad D \mathop {-\!\!\!\twoheadrightarrow }\limits ^{a\!\uparrow \!\overrightarrow{v}} D' }}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P>_{n}^{m}\Vert ~D ~~~\mathop {\longrightarrow }\limits ^{a?\overrightarrow{v}} ~~~<\mathcal{E}\dagger (\overrightarrow{x}\mapsto \overrightarrow{v}),F,C^?,T^?,E,E'\Vert P>_{n}^{m'}\Vert ~D'} } \overrightarrow{v}\sqsubseteq \overrightarrow{x}$$

  • Each error produced by an event handler is treated by the fault handler of the corresponding scope.

    $$(R_{E}^\Rsh ) \frac{\displaystyle {E \mathop {\longrightarrow }\limits ^{\Rsh _{n}} E' \quad F \mathop {\longrightarrow }\limits ^{\Lsh _{n}} F'}}{\displaystyle {<\mathcal{E},F,C^?,T^?,E,P> \mathop {\longrightarrow }\limits ^{\tau } <\mathcal{E},F',C^?,T^?,E,P>^{FT0} } } $$

3 Related Work

Several interesting contributions were appeared during the last years to formalize the semantics of BPEL. Most of them tried to match the constructors of BPEL with some terms in an existing process algebra and only few works have attempted to define a new algebra that fit better with BPEL’s features. In [7–9] the authors have presented a two-way mapping between a fragment of BPEL and the process algebra LOTOS. They have considered most of BPEL’s activities including fault, compensation and event handlers. In [5] the authors have proposed a mapping from a BPEL process to a \(\pi \)-based calculus, named web\(\pi \infty \). They advocated that the different mechanisms (fault handler, termination handler and compensation handler) for error handling are not needed and they proposed the idea of event notification to substitute them. The authors of [11] have proposed an approach based on two-way mapping between the \(\pi \)-based orchestration calculus and BPEL. [10] presented a formalization of BPEL 2.0 based on the \(\pi \)-calculus.The authors of [12] proposed an approach based RECATNet to model and verify a fragment of BPEL processes. The authors of [13] present a novel correct-by-construction formal approach based on refinement using the Event-B method. A Petri net sematics for BPEL has also been introduced in [14]. The main drawback of these works is that they are either too abstract to handle most of the interesting details related to BPEL or they lead to complex representation of some intuitive aspects like compensation. In [8, 15, 16], Pu et al. introduced an interesting process algebra to specify the activities of BPEL. Mostly, the authors focus on fault and compensation handling. Several other interesting formal semantics were proposed in the literature including [17, 18] to formalize handlers in BPEL, but no one of them take into account all the details. Some of other advantages of AV-BPEL semantics are:

  • Compensations can be executed in parallel in some cases as specified by the semantic of BPEL. But, this is not the case for [17, 18].

  • Receive action is blocking while send action is not which reflect better reality. Floating message give a simple way to integrate this kind of communication.

4 Conclusion

This paper introduces a process algebra called AV-BPEL to disambiguate some important but very confusing features of BPEL. These include fault handler, compensation handler, termination handler and event handler (EFCT). Despite that the global idea of these handlers can be easily understood, their full semantics hide many details making them the major source of difficulty behind BPEL. Compared to existing related work, the main advantage of our formalization is that it shows the real complexity hidden behind EFCT aspects by taking into account almost all details related to them.