Extending and refining an abstract operational semantics of the Web Services architecture for the business process execution language

The Business Process Execution Language for Web Services (BPEL) is a forthcoming industrial standard for automated business processes, proposed by the OASIS1 Web Services BPEL Technical Committee. BPEL is a service orchestration language which extends the underlying Web services interaction model and enables Web services to support long running business transactions.; We formally define an abstract operational semantics for BPEL based on the abstract state machine (ASM) paradigm. Specifically, we model the dynamic properties of the key language constructs through the construction of a BPEL Abstract Machine in terms of partially ordered runs of distributed real-time ASMs. The goal of our work is to provide a well defined semantic foundation for establishing the key language attributes by eliminating deficiencies hidden in the informal language definition.; This work combines two well-defined ASM refinement techniques to complement our previous efforts on the core model of the BPEL Abstract Machine. First, we elaborate the core model with regard to structural and behavioural aspects to make it more robust and flexible for further refinements. Specifically, we formalize the process execution model of BPEL and its decomposition into execution lifecycles of BPEL activities. We also introduce an agent interaction model to facilitate the interaction between different Distributed Abstract State Machine (DASM) agents of the BPEL Abstract Machine. We then extend the core model through two consecutive refinement steps to include data handling and one of the most controversial issues in BPEL, fault and compensation handling. The resulting abstract machine model provides a comprehensive formalization of the BPEL dynamic semantics and the underlying Web services architecture.; 1Organization for the Advancement of Structured Information Standards.