An operational semantics of WS-BPEL based on abstract BPEL machine

It is very difficult to construct a correct BPEL engine, which is the runtime environment supporting the execution of BPEL processes. The main reason is the complexity of informal specification. It leads to that the programmers build the system without knowing precisely what they do. In this paper, we provide an operational semantics of BPEL based on Abstract BPEL Machine (ABM). ABM is a formal model that simulates the execution environment of BPEL. The functional behavior of a BPEL engine can be described as the input-output state transitions on ABM. It can be further divided into the execution behavior of each BPEL constructs, such as activities and handlers. The aim of our work is to provide the precise understanding on execution model of BPEL, and narrow the gap between BPEL specification and BPEL implementation. The result can be used as a formal specification to construct a correct BPEL engine.