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.
TopTwo 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.