A model for BPEL-like languages

Web service is increasingly being applied in solving many universal interoperability problems. Business Process Execution Language (BPEL) is a de facto standard for specifying the behavior of business processes. It contains several interesting features, including scope-based compensation, fault handling and shared-labels for synchronization. In this paper we explore an observation-oriented model for BPEL-like languages, which can be used to study program equivalence. The execution states of a program are divided into five types: completed state, waiting state and divergent state, as well as error state and undo state. The last two states are especially for dealing with compensation and fault handling. Based on the formalized model, a set of algebraic laws is investigated, including traditional laws and BPEL featured laws. The concept of guarded choice is also introduced in this model, which can be used to support the transformation of a parallel program into the form of guarded choice. Two special scopes are introduced: canonical structure and compensation structure, which are used to eliminate undo and compensation construct from finite processes.