Modeling Control Flow in WS-BPEL with Chu Spaces

Modeling Control Flow in WS-BPEL with Chu Spaces

Xutao Du (Institute of Electronic System Engineering, China), Chunxiao Xing (Tsinghua University, China), Lizhu Zhou (Tsinghua University, China) and Ke Han (Institute of Electronic System Engineering, China)
DOI: 10.4018/978-1-4666-2649-2.ch012
OnDemand PDF Download:
List Price: $37.50


This paper presents a Chu spaces semantics of typical control flow of WS-BPEL including fault handling and link semantics. BPEL-CF is proposed as a simplification of this subset of WS-BPEL. For the compositional modeling of BPEL, the authors present a Chu spaces process algebra. This algebra allows faults to be thrown at any point of execution and take link-based synchronization into consideration. The paper gives the abstract syntax of BPEL-CF, the semantic algebra, and the valuation functions for computing the Chu spaces denotations of BPEL-CF programs.
Chapter Preview

Two kinds of related work need to be discussed: formal semantics of WS-BPEL and the study of Chu spaces process algebra.

Much research has been done on the formulating of WS-BPEL (or earlier versions) semantics. The main objectives of giving a formal semantics of WS-BPEL are twofold: to clarify the informal WS-BPEL specifications and to verify WS-BPEL processes. Because of the large number of publications, we will not (and cannot) give a full survey in this section (not so recent surveys can be found in Morimoto, 2008; van Breugel & Koshkina, 2006). We apologize to those authors whose excellent results are not mentioned here. According to the formalisms being used, these publications are categorized into three groups: automata (Fu, 2004; Kovács, Gönczy, & Varró, 2008; Nakajima, 2006; Pu et al., 2005), Petri nets (Lohmann, 2007a; Ouyang et al., 2007; Schlingloff, Martens, & Schmidt, 2005; Yang, Tan, Xiao, Liu, & Yu, 2006) and process algebras (Ferrara, 2004; Foster, 2006; Lapadula, Pugliese, & Tiezzi, 2007, 2008; Lucchi & Mazzara, 2007).

Two important factors in the formal semantics of WS-BPEL are (1) whether it supports the interleaving semantics or true concurrency; (2) whether it supports process-algebraic verification.

Complete Chapter List

Search this Book: