High level specification and validation of the Business Process Execution Language for Web Services
Mona Vajihollahi · Summit (Simon Fraser University) · 2004
The Business Process Execution Language for Web Services (BPEL) is an XML based formal language for the design of networking protocols for automated business processes. Originally introduced by leading e-business vendors, including IBM and Microsoft, BPEL is now a forthcoming industrial standard as the work on the language continues at OASIS' within the technical committee on the Web Services Business Process Execution Language (WSBPEL TC). We formally define an abstract executable semantics for the language in terms of a distributed abstract state machine (DASM). The DASM paradigm has proven to be a feasible, yet robust, approach for modeling architectural and programming languages and has been used as the basis for industrial standardization before. The goal of this work is to support the design and standardization of BPEL by eliminating weak points in the language definition and validating key system attributes through experimental validation. The necessity of formalisation in the standardization process is well recognized by the OASIS WSBPEL TC and is formulated as one of the basic issues by the technical committee. There is a need for formalism. It will allow us to not only reason about the current specification and related issues, but also uncover issues that would otherwise go unnoticed. Empirical deduction is not suflcient. 2 We take a hierarchical refinement approach to model the language. Starting from an abstract ground model of the core attributes of the language, we perform step-wise 1 Organization for the Advancement of Structured Information Standards (OASIS), www.oasis-open.org Issue #42, WSBPEL Issue List, WSBPEL TC at OASIS refinements obtaining a hierarchy of ground models at different levels of abstraction which leads to the final executable model. The executable model is then used together with a graphical visualization tool to experimentally validate the key attributes of the language through simulation of abstract machine runs.