There have been several efforts to express the BPEL semantics in a formal language – on both the previous and the current version.

Most of that work is focused on proving certain properties; an approach where a formal system – in this case, a process description – is transformed into a mathematical model. On this model, certain properties of interest may be examined, for example the reachability of activities. A property of the mathematical model may then be proven to be a property of the original system.

The work differs, both in what model is used and to what level of abstraction that is modeled.Note that some of the work we present here is based on the previous version of WS-BPEL, that is, BPEL4WS version 1.1.

Petri Net

Stahl presents a pattern-based algebraic high-level Petri net semantics for the previous version of BPEL [Sta05].

The approach used is to create at least one Petri net pattern for each activity. Some activities have more than one pattern to choose from, based on their usage. These patterns can then be plugged together, the same way activities are composed, into a complete process description.

The focus of Stahl’s work is on the control flow, but the idea is not to execute actual process instances, rather his Petri nets are aimed to be used with a model checker, to evaluate certain properties of process descriptions.

Stahl’s Petri net model is feature complete, allowing any process description to be transformed into a Petri net – with some limitations. One example is, that at most one correlation set can be used, per activity.

For the purpose of model checking, not all parts of the language needs to be modeled. For example, while Stahl’s high level Petri net do model data, it abstracts from actual data manipulation. Also, it does not model details of fault generation, such as the specific fault conditions. It does however handle faults, but only in order to investigate properties of the control flow.

Lohmann extends the work of Stahl, presenting a feature-complete Petri net semantics for the current version of BPEL [Loh07]: A full model of both control flow and data aspects.

However, aspects outside the standard specification, such as XPath, XSTL and WSDL, are not included in the model. For example, the evaluation of a boolean expression is abstracted to its possible outcomes. This is sufficient for a number of static analysis on process descriptions, which is the goal of his work.

Abstract State Machine

Fahland presents the first complete abstract operational semantics for the previous version of BPEL [Fah05]. The work of Fahland is an extension of Farahbod et al., who constructed a distributed real-time Abstract State Machine, but with focus on the execution life cycle of BPEL activities [Far05].

Both Fahland and Farahbod et al. aims at resolving issues of ambiguous requirements and inconsistencies in the standard specification. And both papers have perspectives towards formal verification of implementations. Fahland points out three parts of the standard specification, where he found that insufficient semantics were provided by the informal descriptions. Note, that this work is on the previous version of BPEL.

Pi-Calculus

Aiming towards verification of behavioral compatibility between interacting services, and consistency in implementation of abstract process definitions, Weidlich presents a “lightweight formalization” of BPEL [Wei07]. It has its focus on the positive control flow – that is, the non-faulted behavior. Weidlich abstracts from any data manipulation, except for partner link assignments. This and an abstraction from modeling the activity life cycle, results in a reduced state space, thus, more efficient verification – compared to other approaches based on process algebras.

Lucchi and Mazzara have focus on the negative control flow, that is, the fault handling behavior, in their work [Luc05]. They introduce a new language, called web∞. It is based on the pi-calculus, but extended with a transactional mechanism. They argue that event, fault and compensation handling can be simplified to one mechanism, and shows that their language is more expressive than BPEL. However, they only define semantics for a subset of the BPEL activities.

Extended Timed Finite Automata

Geguang et al. propose a language they call μ-BPEL [Geg05], based on a simplification of the previous version of BPEL. They define full operational semantics for their language and map its constructs into composable Extended Timed Automata (ETA).

For the operational semantics they use a labeled transition system; a notation form where language constructs are formulated as transitions from one state into another. Using this notation the complete set of valid transitions, also called interference rules, are defined.
Geguang et al. used an extended form of Timed Automata, including initial and ending states, synchronization channels and variables.

References

Sta05: Christian Stahl, A Petri Net Semantics for BPEL (2005)

Loh07: Niels Lohmann, A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and its Compiler BPEL2oWFN (2007)

Fah05: Dirk Fahland, Complete Abstract Operational Semantics for the Web Service Business Process Execution Language (2005)

Far05: Roozbeh Farahbod, Uwe Glässer and Mona Vajihollahi, Abstract Operational Semantics of the Business Process Execution Language for Web Services (2005)

Wei07: Matthias Weidlich, Efficient Analysis of BPEL 2.0 Processes using π-Calculus (2007)

Luc05: Roberto Lucchi and Manuel Mazzara, A pi-calculus based semantics for WS-BPEL (2005)

Geg05: Pu Geguang, Zhao Xiangpeng, Wang Shuling, and Qiu Zongyan, Towards the Semantics and Verification of BPEL4WS (2005)