Formal Modelling and Verification of Transactional Web Service Composition: A Refinement and Proof Approach with Event-B

Abstract

Several languages for describing Web service compositions, like BPEL (Business Process Execution Language), make use of fault and compensation constructs to handle internal and/or external runtime errors of the composed service. This situation particularly occurs for transactional services. However, the absence of a rigorous definition of these BPEL constructors makes it difficult to correctly define the transactional behaviour of a BPEL process. The definitions of such constructs are usually given by their informal descriptions available in the standards. Our contribution proposes an approach to formally define the semantics of these operators. Thus, this paper presents a new Event-B semantics for formal modelling of Web service compositions that covers the scope, the fault and the compensation handlers introduced by the BPEL language specification. It also proposes a methodology showing how we can use Event-B method to design transactional BPEL processes. The proposed approach is illustrated by a case study.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Service-oriented architectures (SOA) are increasingly used in various application domains. Indeed, a wide range of services operate on the Web and access different distributed and shared resources like databases, data warehouses and scientific calculation repositories. Moreover, the compositions of such services define complex systems not only in the area of computing but also in various businesses like manufacturing or scheduling. Some of these services performing transactional activities are called transactional Web services. This kind of services must satisfy the relevant properties related to transactional systems (atomicity, consistency, isolation and durability (ACID) properties) traditionally required by database management systems. Although the notion of transactions is well mastered by traditional shared and distributed databases, SOA suffers from a lack of formal semantics of transactional Web services. Indeed, in the current SOA tools, overall business transactions may fail or be cancelled when many ACID transactions are committed.

BPEL (Business Process Execution Language [22]) is considered as a standard of Web service composition specification. It offers a compensation mechanism by providing resources for flexible control of reversal and/or resume activities. To reach this goal, BPEL offers the possibility to define fault handling and compensation in an application-specific manner. BPEL has an XML-based textual representation, and its dynamic semantic description is still informally defined in the standards. Due to the lack of formal semantics of BPEL, ambiguous interpretations remain possible, especially the use of different mechanisms (fault handlers and compensation handlers) to handle transactional behaviour. Such languages do not offer the capability to formally handle the transactional Web service aspects and to ensure their correct behaviour.

Several approaches have proposed formal semantics to the BPEL language using different formal descriptions. Petri nets, transition systems, pi-calculus and process algebra have been set up to model BPEL processes; they are summarised in Sect. 8. In our previous work ([5, 6]), we have defined an Event-B-based [2] semantics for the various elements of data and service descriptions and for simple and structured BPEL activities. In this paper, we propose to extend this work to cover the scope, the fault and the compensation handlers introduced by the BPEL language specification. We also propose a methodology to design a transactional BPEL process by assisting a designer for detecting and verifying a transactional behaviour in a BPEL process.

This paper is structured as follows. The next section presents the Event-B method, and Sect. 3 gives an overview of the BPEL language and the case study used in this paper to illustrate the proposed approach. Sections 4, 5 and 6 present, respectively, the proposed approach for analysing transactional Web services and how Event-B method is used to encode these scope, fault and compensation constructs. Section 7 presents an application of the proposed approach to a case study. Section 8 discusses our approach compared to the state of the art in formal verification of BPEL processes and transactional Web services. Finally, a conclusion and some perspectives are outlined.

2 The Event-B Method

The Event-B method [2] is a recent evolution of the B method [1]. This method is based on the notions of preconditions and post-conditions [16], the weakest precondition [9] and the calculus of substitution [1]. It is a formal method based on first-order logic and set theory.

2.1 Event-B Model

An Event-B model is defined by a set of variables, defined in the VARIABLES clause that evolves thanks to events defined in the EVENTS clause. It encodes a state transition system where the variables represent the state and the events represent the transitions from one state to another.

An Event-B model is made of several components of two kinds: Machines and Contexts. The Machines contain the dynamic parts (states and transitions) of a model, whereas the Contexts contain the static parts (axiomatisation and theories) of a model. A Machine can be refined by another one, and a Context can be extended by another one. Moreover, a Machine can see one or several Contexts (Fig. 1).

Fig. 1

MACHINE and CONTEXT relationships

The refinement operation [3] offered by Event-B encodes model decomposition. A transition system is decomposed into another transition system with more and more design decisions while moving from an abstract level to a less abstract one. A refined Machine is defined by adding new events, new state variables and a gluing invariant. Each event of the abstract model is refined in the concrete model by adding new information expressing how the new set of variables and the new events evolve.

A Context is defined by a set of clauses (Fig. 2) as follows:

• CONTEXT represents the name of the component that should be unique in a model.

• EXTENDS declares the Context extended by the described Context.

• SETS describes a set of abstract and enumerated types.

• CONSTANTS represents the constants used by a model.

• AXIOMS describes, in first-order logic expressions, the properties of the attributes defined in the CONSTANTS clause. Types and constraints are described in this clause as well.

• THEOREMS are logical expressions that can be deduced from the axioms.

Fig. 2

The structure of an Event-B development

Similarly to Contexts, a Machine is defined by a set of clauses (Fig. 2). Briefly, the clauses mean:

• MACHINE represents the name of the component that should be unique in a model.

• REFINES declares the Machine refined by the described Machine.

• SEES declares the list of Contexts imported by the described Machine.

• VARIABLES represents the state variables of the model of the specification. Refinement may introduce new variables in order to enrich the described system.

• INVARIANTS describes, by first-order logic expressions, the properties of the variables defined in the VARIABLES clause. Typing information, functional and safety properties are usually described in this clause. These properties shall remain true in the whole model. Invariants need to be preserved by events. It also expresses the gluing invariant required by each refinement for property preservation.

• THEOREMS defines a set of logical expressions that can be deduced from the invariants. They do not need to be proved for each event like for the invariant.

• VARIANT introduces a decreasing natural number which states that the “convergent” events terminate.

• EVENTS defines all the events (transitions) that occur in a given model. Each event is characterised by its guard and by the actions performed when the guard is true. Each Machine must contain an “Initialisation” event. The events occurring in an Event-B model affect the state described in VARIABLES clause.

  An event consists of the following clauses (Fig. 3):

  • status can be “ordinary”, “convergent” (the event has to decrease the variant) or “anticipated” (the event must not increase the variant).

  • refines declares the list of events refined by the described event.

  • any lists the parameters of the event.

  • where expresses the guard of the event. An event is fired when its guard evaluates to true. If several guards evaluate to true, only one is fired with a non-deterministic choice.

  • then contains the actions of the event that are used to modify the state variables.

  Fig. 3

  

  Event structure

Event-B offers three kinds of actions that can be deterministic or not (Fig. 4). For the first case, the deterministic action is represented by the “assignment” operator that modifies the value of a variable. This operator is illustrated by the action (1). For the case of the non-deterministic actions, the action (2) represents the “before-after” operator acting on a set of variables whose effect is represented by a predicate, expressing the relationship between the contents of variables before and after the triggering of the action. Finally, the action (3) represents the non-deterministic choice operator, acting on a variable, by modifying its content with an undetermined value in a set of values.

Fig. 4

The kinds of actions of an event

2.2 Proof Obligation Rules

Proof obligations (POs) are associated to any Event-B model. They are automatically generated. The proof obligation generator plug-in in the Rodin platform [24] is in charge of generating them. These POs need to be proved in order to ensure the correctness of developments and refinements. The obtained PO can be proved automatically or interactively by the prover plug-in in the Rodin platform.

The rules for generating proof obligations follow the substitution calculus [1] close to the weakest precondition calculus [9]. In order to define some proof obligation rules, we use the notations defined in Figs. 2 and 3 where s denotes the seen sets, c the seen constants and v the variables of the Machine. Seen axioms are denoted by A(s, c) and theorems by T(s, c), whereas invariants are denoted by I(s, c, v) and local theorems by T(s, c, v). For an event evt, the guard is denoted by G(s, c, v, x), and the action is denoted by the before-after predicate BA(s, c, v, x, v′) (the action (2) of Fig. 4).

• The theorem proof obligation rule: this rule ensures that a proposed context or machine theorem is indeed provable:

  $$\displaystyle\begin{array}{rcl} & A(s,c)\Longrightarrow T(s,c) & {}\\ & A(s,c) \wedge I(s,c,v)\Longrightarrow T(s,c,v)7& {}\\ \end{array}$$

• Invariant preservation proof obligation rule: this rule ensures that each invariant in a machine is preserved by each event:

  $$\displaystyle{A(s,c) \wedge I(s,c,v) \wedge G(s,c,v,x) \wedge \mathit{BA}(s,c,v,x,v')\Longrightarrow I(s,c,v')}$$

• Feasibility proof obligation rule: the purpose of this proof obligation is to ensure that a non-deterministic action is feasible:

  $$\displaystyle{A(s,c) \wedge I(s,c,v) \wedge G(s,c,v,x)\Longrightarrow\exists v'.\mathit{BA}(s,c,v,x,v')}$$

• The numeric variant proof obligation rule: this rule ensures that under the guards of each convergent or anticipated event, a proposed numeric variant is indeed a natural number:

  $$\displaystyle{A(s,c) \wedge I(s,c,v) \wedge G(s,c,v,x)\Longrightarrow V (s,c,v) \in \mathbb{N}}$$

• The variant proof obligation rule: this rule ensures that each convergent event decreases the proposed numeric variant. It also ensures that each anticipated event does not increase the proposed numeric variant. The rule in the case of a convergent event is

  $$\displaystyle{A(s,c) \wedge I(s,c,v) \wedge G(s,c,v,x) \wedge \mathit{BA}(s,c,v,x,v')\Longrightarrow V (s,c,v') <V (s,c,v)}$$

  The rule in the case of an anticipated event is

  $$\displaystyle{A(s,c) \wedge I(s,c,v) \wedge G(s,c,v,x) \wedge \mathit{BA}(s,c,v,x,v')\Longrightarrow V (s,c,v') \leq V (s,c,v)}$$

There are other rules for generating proof obligations to prove the correctness of refinement. These rules are given in [2].

2.3 Semantics of Event-B Models

The new aspect of the Event-B method [2], in comparison with classical B [1], is related to the semantics. Indeed, the events of a model are atomic events of state transition systems. The semantics of an Event-B model is trace-based semantics with interleaving. A system is characterised by the set of licit traces corresponding to the fired events of the model which respects the described properties. The traces define a sequence of states that may be observed by properties. All the properties will be expressed on these traces.

This approach proved the capability to represent event-based systems like railway systems, embedded systems or Web services. Moreover, decomposition (thanks to refinement) supports building of complex systems gradually in an incremental manner by preserving the initial properties, thanks to the preservation of a gluing invariant.

3 Service Composition Description Languages

The Web service composition description languages are XML-based languages. The most popular languages are BPEL [22], CDL [30], OWL-S [29], BPMN [23] and XPDL [31]. If these languages are different from the description point of view, they share several concepts, in particular the service composition. Among the shared concepts, we find the notions of activity for producing and consuming messages; attributes, for instance, correlation; message decomposition; service location; compensation in case of failure; events; and event handling. These elements are essential to describe service compositions and their behaviour.

However, due to their XML-based definition, these languages suffer from a lack of semantics. It is usually informally expressed in the standards that describe these languages using natural language or semiformal notations. Hence, the need of a formal semantics expressing this semantics emerged. Formal description techniques and the corresponding verification procedures are very good candidates for expressing the semantics and for verifying the relevant properties.

The formal approach we develop in this paper uses BPEL as a service composition description language and Event-B as a formal description technique. The proposed approach can be extended to be used with other service composition description language.

3.1 Overview of BPEL

BPEL (Business Process Execution Language [22]) is a standardised language for specifying the behaviour of a business process based on interactions between a process and its service partners (partnerLink). It defines how multiple service interactions, between these partners, are coordinated to achieve a given goal. Each service offered by a partner is described in a WSDL document through a set of operations and of handled messages.

WSDL (Web Service Description Language [28]) is a standardised language for describing the published interface (input and output parameter types) of the Web service. It provides with the address of the described service, its identity, the operations that can be invoked and the operation parameters and their types. Thus, WSDL describes the function provided by Web service operations. It defines the exchanged messages that envelop the exchanged data and parameters. The composition of such Web services is described in languages, like BPEL, supporting such composition operators.

A BPEL process uses a set of variables to represent the messages exchanged between partners. They also represent the state of the business process. The content of these messages is amended by a set of activities which represent the process flow. This flow specifies the operations to be performed, their ordering, activation conditions, reactive rules, etc. Figures 5 and 6 show the XML structure of a WSDL description and a BPEL process.

Fig. 5

The XML WSDL (Web Service Description Language) description of BankTransfer services

Fig. 6

The XML BPEL description of BankTransfer process

BPEL offers two categories of activities: (1) atomic activities representing the primitive operations performed by the process (they are defined by the invoke, receive, reply, assign, terminate, wait and empty activities and correspond to basic Web services) and(2) structured activities obtained by composing primitive activities and/or other structured activities using the sequence, if, while and repeat Until composition operators that model traditional sequential control constructs. Three other composition operators are defined by the pick operator defining a non-deterministic choice, the flow operator defining the concurrent execution and the scope operator defining subprocess execution. BPEL also introduces systematic mechanisms for fault handling by defining a set of activities to be executed for handling possible errors anticipated by the Web service composition designer. A compensation handler can be associated to the fault handler; it starts from the erroneous process itself to undo some steps that have already been completed and return the control back at the identified checkpoints.

3.2 A Case Study

We have chosen to illustrate our approach on the pedagogical case study of the BankTransfer commonly used to describe transactional Web services (Figs. 5, 6 and 7). This example describes a service processing a bank transfer between two bank accounts from two different banks. On receiving the transfer order from a customer, the process makes, in sequence, a debit from the source bank account and a credit to the target bank account. The BPEL description of Fig. 6 shows how the BankTransfer process is decomposed into a sequence of ReceiveTransferInfos, AssignTransferInfos, InvokeDebit, InvokeCredit, AssignResponse and Reply activities. The transaction order information, sent by the customer, is stored in the TransactionIn message, and the transaction receipt is sent to the customer in the TransactionOut message. The DebitInfo and CreditInfo messages contain the information sent to the two bank accounts to make the transfer.

Fig. 7

The graphical BPEL description of BankTransfer process

4 Event-B for Analysing Transactional Web Services

Our idea is to provide assistance to BPEL developers using the Event-B method [2]. The choice of this formal method is guided by the fact that proof-based methods do not suffer from the state number explosion problem and proofs are eased by the refinement thanks to the decomposition it provides. Our motivation for the use of this formal method is detailed in the previous work [5, 6]. More precisely, our objective is to provide a methodology for detecting the BPEL process parts that handle critical resources. Traditionally, the developer builds its BPEL process and describes the process behaviour without using fault and compensation handlers to guarantee transactional constraints. He/she adds these constraints by observing the behaviour of the obtained process.

In the approach we promote, the designed BPEL process is translated into an Event-B model according to the rules defined in [5] and [6]. Then, the transactional properties and the properties related to the consistencies of resources used by the BPEL process are expressed in the form of consistency invariants (consistency property). These invariants are defined by the designer because there is no BPEL resource supporting their expression nor a technique for their checking. Once this enrichment is performed, proof obligations (POs) are generated. Some of these POs related to invariants involving the transactional properties are unprovable because triggering some events separately violates the consistency invariants. Then, BPEL activities related to the event source of these unprovable POs are detected and isolated in a BPEL scope element. This element allows the designer to define a particular BPEL part on which specific mechanisms only apply to this isolated part in an atomic manner. In our case, for transactional BPEL parts, we recommend to apply the mechanisms for fault and compensation handling to the scope element (compensational atomicity property: guarantees that a transaction consisting of a Web service request will run in such a way that either all of its requests are completed successfully or all requests that occurred during the processing of this transaction will be compensated) and the “isolated” attribute of the corresponding scope is set to “true”. As a consequence, the execution of this part is isolated by the orchestration tools (isolation property), and at the same time, consistency of the resources used by these activities is guaranteed. Transactional properties may require a redesign of the defined BPEL process. From a methodological point of view, our approach relies on the following steps.

Step 1:

Translate the BPEL model into an Event-B model.

Step 2:

Introduce, in the Event-B model, the relevant invariants related to the suited transactional behaviour.

Step 3:

Isolate the events of the Event-B model whose POs, associated to the introduced invariant of step 2, are not provable.

Step 4:

Redesign the BPEL model of step 1 by introducing a BPEL scope embedding the events identified at step 3 and compensation/fault handlers.

This step-based approach is applied until the associated Event-B model is free of unproven POs.

In the following sections, we present the Event-B models for scope, fault handler and compensation handler BPEL concepts. These models extend the proposed ones of the general approach of [5] and [6] to support transactional BPEL processes modelling or checking the behaviour of composed Web services in the case of an internal or external runtime error of a BPEL process.

5 Modelling Scope, Fault and Compensation Handlers

Before addressing the formal modelling of the transactional behaviour, we reviewed the proposed Event-B formal semantics of BPEL ([5, 6]).

5.1 Formal Modelling of BPEL ([5, 6])

Our approach for formal modelling of BPEL with Event-B is based on the observation that a BPEL definition is interpreted as a transition system interpreting the process coordination. A state is represented in both languages by a variables element in BPEL and by the VARIABLES clause in Event-B. The various activities of BPEL represent the transitions. They are encoded by events of the Event-B EVENTS clause. For a better understanding of this paper, the transformation rules from BPEL to Event-B models are briefly recalled below. This translation process consists of two parts: static and dynamic.

5.1.1 Static Part

The first part translates the WSDL definitions that describe the various Web services and their data types, messages and port types (the profile of supported operations) into the different data types and functions offered by Event-B. This part is encoded in the Context part of an Event-B model.

A BPEL process references data types, messages and operations of the port types declared in the WSDL document. In the following, the rules translating these elements into an Event-B Context are inductively defined:

1:

The WSDL message element is formalised by an abstract set. Each part attribute of a message is represented by a functional relation corresponding to the template part ∈ message → type_part from the message type to the part type. On the case study in Fig. 5, a set named InfosMessage is defined in the SETS clause, and the application of this rule corresponds to the axiom a12 and a13 declarations in the BankTransferContext in Fig. 8.

Fig. 8

The Event-B CONTEXT of BankTransfer process

2:

Each operation of a WSDL portType is represented by a functional relation corresponding to the template operation ∈ input → output mapping the input message type on the output message type. On the case study in Fig. 5, the BankTransferOperation operation is encoded by the functional relation described by axiom a18 in Fig. 8.

5.1.2 Dynamic Part

The second part concerns the description of the orchestration process of the activities appearing in a BPEL description. These processes are formalised as Event-B events; each simple activity becomes an event of the Event-B model, and each structured or composed activity is translated to a specific event construction. This part is encoded in a Machine of an Event-B model.

A BPEL process is composed of a set of variables and a set of activities. Each BPEL variable corresponds to a state variable in the VARIABLES clause, and the activities are encoded by events. This transformation process is inductively defined on the structure of a BPEL process according to the following rules:

3:

The BPEL variable element is represented by a variable in the VARIABLES clause in an Event-B Machine. This variable is typed in the INVARIANTS clause using messageType BPEL attribute. The variables and invariants corresponding to the case study are given in Fig. 9. For example, the BPEL variable DebitInfo is declared and typed.

Fig. 9

The Event-B MACHINE of BankTransfer process (part 1)

4:

Each BPEL simple activity is represented by a single event in the EVENTS clause of the Event-B Machine. For example, in Fig. 10, the ReceiveTransferInfos BPEL atomic activity is encoded by the ReceiveTransferInfos Event-B event.

Fig. 10

The Event-B MACHINE of BankTransfer process (part 2)

5:

Each BPEL structured activity is modelled by an Event-B description which encodes the carried composition operator. Modelling composition operations in Event-B follow the modelling rules formally defined in [4]. Again, on the same example (Fig. 6), the structured activity BankTransferProcess is encoded by a sequence of six events controlled by the varSeq_1 variable initialised to value 6 (Fig. 10).

When the Event-B models formalising a BPEL description are obtained, they may be enriched by the relevant properties that formalise the user requirements and the soundness of the BPEL-defined process like BPEL type control, orchestration and service composition, deadlock freeness, no live-lock, precondition for calling a service operation and data transformation ([5, 6]).

5.2 An Event-B Model for Scope

The BPEL language provides a particular mechanism for subprocess description thanks to the scope construct. Scope encapsulates subprocess behaviours and includes a context used by the execution of the activities that describe its behaviour. This context contains a state composed by a set of variables. Each scope has a required primary activity that describes its behaviour (Fig. 11).

Fig. 11

A BPEL scope element containing fault and compensation handlers

The scopeModel MACHINE in Fig. 12 formalises the scope behaviour. This MACHINE introduces a mainActivity event that models the main activity of a scope and a scopeName event that models the end of a scope execution. The variable varScope is initialised to 1. This variable triggers the scopeName event at the end of the mainActivity event. If the scope’s main activity is of structured type, the transformation rules defined for structured activities in [5] are applied. Similarly, the scope variables are modelled according to the variable transformation rules defined in [5].

Fig. 12

An Event-B model for a BPEL scope element

G _sa , G′, S _sa and S′ represent the guards and the actions of the mainActivity and scopeName events. They result from variable and activity modelling and are related to the data manipulation and to the process behaviour. The same reasoning applies for fault and compensation handler models presented below.

5.3 An Event-B Model for Fault Handler

A BPEL fault handler is a process that is triggered when an error rose from a partner Web service or an internal BPEL process. It provides a mechanism to define a set of customised “fault-handling” activities. A catch element is defined to intercept (to catch) a specific kind of fault, defined by a “faultName” attribute. If no predefined name is associated to the intercepted fault, this fault will be processed by a catchAll element (see Fig. 11).

The faultHandlerModel MACHINE in Fig. 13 formalises a fault Handler as described in Fig. 11. The mainActivity event models the normal behaviour of the scope. Different types of errors are taken into account by the defined fault handler. Error types are defined by an enumerated set called faultType in the SETS clause. It contains all fault types identified by the designer and used in the BPEL process description. The model in Fig. 13 formalises the case of errors called fault_1 among other faults. A varFault variable is introduced to determine whether the current behaviour of the process is catching errors (varFault=1) or describes a normal execution (varFault=0).

Fig. 13

An Event-B model for a BPEL fault handler

The occurrence of an error is formalised by the faultOccurs event that is arbitrarily triggered (non-deterministic occurrence of the event). When this event is triggered, it ceases the normal behaviour described by the mainActivity event thanks to the action varFault:=1. The fault processing, corresponding to the error defined by the currentFault variable content, starts. If this variable contains the fault_1 value, the catchFault_1 event, formalising the processing of the fault_1 error, is triggered. Otherwise (currentFault=otherFault), the catchAllFaults event, formalising the catchAll element processing, is triggered.

Similarly, this model can be used to formalise a fault handler associated to a BPEL process.

5.4 An Event-B Model for Compensation Handler

A compensation handler is a wrapper for a process that performs compensation. A compensation handler for an activity is available for invocation only when the activity completes successfully. Generally, the invocation of a compensation handler is achieved by a fault handler to undo the effects of already completed activities in the case of a runtime error.

The BPEL process described in Fig. 14 contains two behaviours: the normal behaviour described by the mainActivity sequence element and the error catching behaviour described by the fault handler. The normal behaviour consists of a sequence of activities, and one of these activities is required to be a scope. This scope contains a compensation handler to cancel its effect in the case of a runtime error. Then, the fault handling process consists of triggering the compensate activity.

Fig. 14

BPEL fault and compensation handlers

The compensationModel MACHINE described in Fig. 15 formalises a BPEL process conforming to Fig. 14. The normal behaviour described by a sequence activity is modelled by a mainActivity event according to the defined rules in [5]. Being the jth activity of this sequence, the scope is modelled by the scopeName event which represents part of the scope model obtained using the rules defined in Sect. 5.2. The scopeName event is triggered when varSeq=j.

Fig. 15

An Event-B model for BPEL fault and compensation handlers

The fault handler part is modelled by the catchScope event. It formalises a compensate activity named catchScope. This part describes the scopeFault handling process. The catchScope event triggers the compensation handler contained in the scopeName scope, in the case that currentFault is “scopeFault”. This action is done by assigning value 1 to the varComp variable.

The compensation process is described by the compensationActivity event. It can be triggered if the scopeName scope has completed its execution (varSeq < j) and the catchScope event is triggered (varComp = 1). The compensationActivity specifies the process of compensation. It can be described by one or a set of activities. In this case, the transformation rules of BPEL activities defined in [5] are applied to detail this description.

6 Use of the Tools

The proposed approach is implemented by integrating various plug-ins in the Rodin platform which is based on the Eclipse core. We have used existing plug-ins of Eclipse platform (BPEL editor ¹) and of Rodin platform (Event-B editor, prover [24] and ProB model checker [18]) and developed plug-ins (BPEL2B plug-in [5]). These plug-ins are used at different steps of our approach:

• Designing BPEL process with the BPEL editor and translating the obtained model into an Event-B model using the BPEL2B plug-in (step 1).

• Introducing the relevant invariants related to the suited transactional behaviour with the Event-B editor (step 2). Isolating the events of the model whose POs, associated to the introduced invariant of step 2, cannot be proved within the Rodin prover.

• The ProB model checker assisting the developer to confirm the diagnostic and to get a counterexample associated to the isolated events (step 3).

• Redesigning the BPEL model of step 1 by introducing a BPEL scope embedding the events identified at step 3 and a compensation/fault handler (step 4). The graphical view of the BPEL editor can be used at this step to facilitate the insertion of the new elements.

7 Application to the Case Study

The application of the approach outlined in Sect. 4 on the example in Fig. 6 is given in the following steps. The reader can find all Event-B CONTEXTs and MACHINEs source codes on this website.²

Step 1 :

This step on the BankTransfer BPEL process in Fig. 6 leads to the Event-B model in Figs. 8, 9 and 10 described in Sect. 5.1.

Step 2 :

The transactional properties are expressed in the form of invariant in the Event-B model of step 1. Starting from the model in Figs. 8 and 10, we obtain the model in Fig. 16 by defining a default fault handler with the defaultFaultHandler event. BankAccount1 and BankAccount2 variables formalise the contents of two bank accounts and the amount variable contains the value to be transferred. The InvokeDebit and InvokeCredit events invoke Web services that make the transaction. The consistency property is expressed by invariant i12. The sum of BankAccount1 and BankAccount2 variables shall be constant to ensure consistency of the contents of two bank accounts before triggering InvokeDebit event and after triggering InvokeCredit event. Invariant i13 expresses the state after triggering InvokeDebit event and before triggering the InvokeCredit event.

Fig. 16

The consistency property expression of BankTransfer process

Step 3 :

The POs are generated by the Rodin platform, and those associated to the invariant i12 and to the action varSeq_1:=0 of defaultFaultHandler event, which aborts the BPEL process, cannot be proved (Fig. 17). An inconsistency state results from this abortion.

Fig. 17

The Rodin diagnostic

The invariant violation is usually caused by defaultFaultHandler event triggering when the faultOccurs event is triggered after InvokeDebit event. This diagnostic is confirmed by the ProB model checker [18] that gets a counterexample corresponding to this scenario (Fig. 18). The inconsistency state is varSeq=0 (defaultFaultHandler event) and BankAccount1 + BankAccount2 = ConsistencyState − amount.

Fig. 18

The ProB diagnostic

Step 4 :

If an error occurs during the transaction, a fault handler should restore a consistent state of the process before aborting it. The InvokeDebit and InvokeCredit activities are isolated in the BPEL scope, a fault handler is associated to this scope, and the mechanism for compensation handling is applied to the InvokeDebit and InvokeCredit activities (compensational atomicity property). The “isolated” attribute of this scope is also set to “true” (isolation property). The BPEL process obtained by this step is given in Figs. 19 and 20.

Fig. 19

The BPEL description of a redesigned BankTransfer process

Fig. 20

The graphical BPEL description of a redesigned BankTransfer process

When applying again step 1 on the obtained BPEL process, the Event-B model in Fig. 21 with BankTransferContext and BankTransferMachine components is obtained. Only elements that differ from the Event-B model in Figs. 8 and 10 are shown in Fig. 21. The BankTransferProcess is encoded by a sequence of five events. One of them is BankTransferScope which formalises the BankTransferScope scope. The main activity of this scope is a BankTransfer activity which is decomposed to a sequence of InvokeDebit and InvokeCredit activities controlled by the varSeq_2 variable initialised to value 2. The scopeFaultOccurs event formalises the triggering of a runtime error inside the scope. This event triggers the scope fault handler by assigning the currentFault variable to “scopeFault”. The fault handler process is described by the compensate, rethrow and scopeFaultHandler events. The compensate event triggers different compensation handlers that consist of invoking InvokeCancelDebit and InvokeCancelCredit events to cancel the effect of the InvokeDebit and InvokeCredit events.

Fig. 21

The Event-B model of the redesigned BankTransfer process

In this case, the invariant i12 is changed and adapted to the modifications made by introducing a scope. All POs are proved, and unlike the case in Fig. 16, the invariant i12 is not violated by the fault handler process if scopeFaultOccurs event is triggered after InvokeDebit event (Fig. 22). The scopeFaultHandler event triggers the compensation process (compensate event) before aborting the BPEL process.

Fig. 22

The Rodin statistic view about i12 invariant

8 Related Work

Various approaches have been proposed to model and to analyse BPEL processes. Most of the work in the literature shows that the proposed approaches use transition systems for representing the business processes, activities and workflows and model checking as the underlying formal verification technique for property validation. Hinz et al. [15] and van der Aalst et al. [27] have used Petri nets to encode BPEL processes. Nakajima [21] has mapped a BPEL activity part to a finite automaton encoded in Promela. FSP (finite state process) and the associated tool (LTSA) are used by Foster et al. [12] to check if a BPEL Web service composition behaves like an MSC Web service composition specification captured by message sequence charts (MSCs). Marconi et al. [20] present the approach that translates a BPEL process to a set of state transition systems. These systems are composed of parallel and the resulting parallel composition is annotated with specific Web service requirements. Salaun et al. [25] show how BPEL processes are mapped to processes expressed by LOTOS and CCS process algebra operations. Abstract state machines (ASM) have been developed by Farahbod et al. [11] and Fahland [10] to model BPEL composition process descriptions. Borger et al. [7] have used ASM for modelling workflow, specifically BPMN process. The B method and StaAC were used by Butler et al. [8] to model business transactions and their compensation with an application to a BPEL process. Other approaches proposed formal models for Web service compositions. An overview of these approaches can be found in [26].

In all these proposals, a BPEL description is transformed to a formal model to be checked. However, some of this work did not take into account the fault and compensation mechanisms that enable transactional behaviours of BPEL processes. No formal generic approach handling the full transactional Web service design process is available. Some approaches have given formal semantics for the fault and compensation handlers and encoded them in other formal techniques like Petri nets [14, 19], pi-calculus [13], ASM [11], StaAC and B [8] or SAL [17]. In these approaches, the designer describes by himself/herself the parts that are handled by the fault and compensation handlers, and they check properties related to the behaviour like deadlock freeness. There is no systematic formal modelling approach for handling transactions. Moreover, there is no way to detect the transactional part to be isolated in order to guarantee a correct behaviour of the transactional Web service. Furthermore, existing approaches do not provide the possibility to check if the consistency of the execution context is guaranteed. This is due to the abstraction of data in the model checking techniques applied to Web service validation for reducing the state space exploration. As a consequence, these works don’t describe nor check properties related to the consistency of data produced by the BPEL processes.

Our work is proof oriented; it translates the BPEL language and its constructs into an Event-B model. We encode manipulated data and transactional behaviour, check traditional properties like deadlock freeness and transactional properties [5, 6] and offer to the developer assistance to improve his/her BPEL design by isolating transactional parts to ensure a correct process behaviour. Moreover, it is tool supported.

Notice that this work applies for all transactional-based process compositions.

9 Conclusion

In this paper, we propose an extension of the BPEL Event-B semantics proposed in [5] and [6] by covering the scope, the fault and the compensation handlers. We have also sketched a methodology showing how the obtained Event-B model can be used to handle a transactional behaviour in Web services. Transactional services that access and manage critical resources are isolated in a scope elements with compensation and fault handlers. When modelling fault and compensation handlers by a set of events, it becomes possible to model and check the properties related to transactional Web services. Moreover, the obtained results are not specific to Web service compositions. These results can be reused for the definition of transactional service compositions that occur for areas like telecommunication and network, manufacturing or scheduling. Indeed, the fact that services are Web based is not specific to the proposed approach. BPEL is used as a language for service composition description whatever is the nature or the application domain of the manipulated services.

This work opens several perspectives. One of them is related to the explicit semantics carried by the services. For example, composing in sequence a service that produces distances expressed in centimetres with another one consuming distances expressed in inches should not be a valid composition. Up to now, our approach handles implicit semantics only; it does not handle such a composition. Formal knowledge models carried out by ontologies expressed besides the Event-B models should be investigated.