Durham Research Online
Deposited in DRO:
23 November 2009
Version of attached file:
Published
Peer-review status of attached file:
Peer-reviewed
Citation for published item:
Luo, C. and Qin, S. and Qiu, Z. (2008) ’Verifying BPEL-like programs with Hoare logic.’, Frontiers of
computer science in China., 2 (4). pp. 344-356.
Further information on publisher’s website:
http://dx.doi.org/10.1007/s11704-008-0039-2
Publisher’s copyright statement:
The original publication is available at www.springerlink.com
Use policy
The full-text may be used and/or reproduced, and given to third parties in any format or medium, without prior permission or
charge, for personal research or study, educational, or not-for-profit purposes provided that:
• a full bibliographic reference is made to the original source
• a link is made to the metadata record in DRO
• the full-text is not changed in any way
The full-text must not be sold in any format or medium without the formal permission of the copyright holders.
Please consult the full DRO policy for further details.
Durham University Library, Stockton Road, Durham DH1 3LY, United Kingdom
Tel : +44 (0)191 334 3042 — Fax : +44 (0)191 334 2971
http://dro.dur.ac.uk

Durham Research Online

Deposited in DRO:
11 December 2009

Peer-review status:
Peer-reviewed

Publication status:
Accepted for publication version

Citation for published item:
Luo, C. and Qin, S. and Qiu, Z. (2008) 'Verifying BPEL-like programs with Hoare logic.',
Frontiers of computer science in China., 2 (4). pp. 344-356.

Further information on publishers website:
http://dx.doi.org/10.1007/s11704-008-0039-2

Publishers copyright statement:
The original publication is available at www.springerlink.com













Use policy

The full-text may be used and/or reproduced, and given to third parties in any format or medium, without prior
permission or charge, for personal research or study, educational, or not-for-profit purposes provided that :

 a full bibliographic reference is made to the original source
 a link is made to the metadata record in DRO
 the full-text is not changed in any way

The full-text must not be sold in any format or medium without the formal permission of the copyright holders.

Please consult the full DRO policy for further details.

Durham University Library, Stockton Road, Durham DH1 3LY, United Kingdom
Tel : +44 (0)191 334 2975 | Fax : +44 (0)191 334 2971
http://dro.dur.ac.uk

Front. Comput. Sci. China, 2008, 2(3)
DOI 10.1007/s11467-008-0000-0
Frontiers of Computer Science in China
Verifying BPEL-like Programs with Hoare Logic
Chenguang LUO1, Shengchao QIN1, Zongyan QIU2
1 Department of Computer Science, Durham University, Durham DH1 3LE, United Kingdom
2 LMAM and Department of Informatics, School of Math. Sciences, Peking University, Beijing 100871, China
c© Higher Education Press and Springer-Verlag 2008
Abstract The WS-BPEL language has recently become
a de facto standard for modeling Web-based business pro-
cesses. One of its essential features is the fully programmable
compensation mechanism. To understand it better, many
recent works have mainly focused on formal semantic models
for WS-BPEL. In this paper, we make one step forward by
investigating the verification problem for business processes
written in BPEL-like languages. We propose a set of proof
rules in Hoare-logic style as an axiomatic verification system
for a BPEL-like core language containing key features such
as data states, fault and compensation handling. We also
propose a big-step operational semantics which incorporates
all these key features. Our verification rules are proven sound
with respect to this underlying semantics. The application
of the verification rules is illustrated via the proof search
process for a nontrivial example.
Keywords WS-BPEL, compensation mechanism, opera-
tional semantics, axiomatic verification system, soundness
1 Introduction
The Internet is now developing at a high speed supported
by the web technology. As a result, many web-based ap-
plications, such as Web services, begin to flourish and play
a more and more significant role in various application ar-
eas. Web services boost a new approach to the construction
of business processes where many basic functions are encap-
sulated and provided as individual services on the web, which
later may be composed to form complex services according
Received 07.2008; accepted 09.2008
E-mail: {chenguang.luo, shengchao.qin}@dur.ac.uk, zyqiu@pku.edu.cn
to diverse clients’ demands. To cater for the description of
Web service composition, researchers and industrial practi-
tioners have proposed several Web service orchestration lan-
guages such as XLANG [1], WSFL [2], StAC [3], and WS-
BPEL [4, 5].
Among these orchestration languages, WS-BPEL has now
become a de facto standard. One important feature of WS-
BPEL, as well as some other similar languages, is its mech-
anism for supporting long run transactions (LRTs). In any
single step of an LRT, a fault may occur and appropriate com-
pensation actions may be required. To address such demand,
WS-BPEL provides a set of scope-based fault handling and
compensation mechanisms to deal with faults and potential
undoing of some already completed business activities. The
compensation mechanisms are fully programmable, and thus
allow users to define any application-specific compensation
rules. Nevertheless, these mechanisms, despite very flexible
and powerful, also bring intricacies into the WS-BPEL lan-
guage specification. As a result, it becomes a challenging
issue to formalize and reason about WS-BPEL processes.
Many recent works focused mostly on the formal seman-
tics for WS-BPEL, e.g. [6–10]. These pioneering works are
very important for reducing possible ambiguity in the lan-
guage specification and also for better understanding of the
language. In this paper we will target at an orthogonal but
equally important problem, the partial correctness of WS-
BPEL processes. To make the presentation simple, we shall
focus on a subset of WS-BPEL. However, our core language
will take into account most of the important language features
of WS-BPEL, including data state, fault handling and com-
pensation mechanism. We will design a concise yet novel
operational semantics for our language, and propose a Hoare
logic style verification system on top of it, which will be
proven sound with respect to the underlying semantics. Due

2
Frontiers of Computer Science in China Instruction for authors
to the complexity of web-based business processes, the cor-
rectness of such programs remains as a challenge. Our veri-
fication system for BPEL-like language makes one step for-
ward towards tackling this challenging problem. To the best
of our knowledge, this is the first axiomatic verification sys-
tem for a language with data states, scope-based fault and
compensation handling mechanisms. The main contributions
of this paper can be summarized as follows:
• We propose a concise yet novel operational semantics
for a BPEL-like core language. Although there are some
semantic works with similar topics, our semantics is in-
teresting in that it integrates features like scopes, data
states, fault handling and compensation in a very simple
way.
• We design an assertion language for specifying certain
safety properties for BPEL-like processes, and also pro-
pose a set of axioms and inference rules in Hoare logic
style to form an axiomatic verification system for the
language. The pre- and postconditions are formulas ex-
pressed in our assertion language.
• We state and prove the soundness of our axiomatic ver-
ification system with respect to the semantics. That is,
provable specifications are all semantically valid. A non-
trivial example is presented to illustrate the application
of the verification rules.
The remainder of this paper is organized as follows. Sec
introduces our language BPEL∗ which is a core subset of
WS-BPEL. A new operational semantics for BPEL∗ is then
presented in Sec . Sec 2 is devoted to the Hoare logic style
verification system for BPEL∗. Sec 3 deals with the sound-
ness of our verification system, while Sec 3 gives a nontrivial
example proof using our verification system. Related work
and concluding remarks follow afterwards.
2 The BPEL∗ Language
To concentrate on the main aim of this study, we take into ac-
count a core subset of the WS-BPEL language, called BPEL∗,
which comprises not only the important fault and compensa-
tion handling mechanisms but also data states of WS-BPEL
processes.
The abstract syntax of BPEL∗ is given in Figure 1. Note
that a program written in BPEL∗ is called a business process
(denoted as BP) which may contain an activity A and a fault
handler F. We may sometimes use the general term process
to refer to an activity A, a compensation handler C, or a fault
handler F. The set of all processes is denoted as P.
In Figure 1, x and y stand for variable names, e represents
arithmetic expressions, b is for boolean expressions, and n for
scope names. A denotes a general activity, while C and F are
for compensation and fault handlers, respectively. It is worth
noting that the compensation activity n can only appear in
these two constructs.
Generally a business process has an activity to perform its
BP ::= {| A : F |} (business process)
A ::= skip (do nothing)
| x := e (assignment)
| inv a x y (invoke)
| rec a y (receive)
| rep a x (reply)
| throw (throw a fault)
| A; A (sequence)
| if b then A else A (conditional)
| A ‖ A (flow)
| n : {A ? C : F} (scope)
C,F ::= n (compensation)
| . . . (similar as A)
Fig. 1 The Syntax of BPEL∗
normal work, and once an error occurs it uses the fault handler
to deal with it. As for a general activity, the skip does nothing
to a process, and an assignment simply overwrites a variable’s
value to user’s intention.
The inv, rec and rep constitute our abstract model of com-
munication with external Web services. The a here is an ab-
straction of call port of some Web service beyond the current
process we are interested in. In our work we have taken a
most general web model, where “a” is assumed to have some
arbitrary behavior as far as the current business process is con-
cerned, as it either returns an arbitrary value or fails. It is also
possible to take more specialized models, which is out the
consideration of this paper.
The throw throws a fault to prevent any other activity in
the current scope from being processed, until the end of the
business process — or it is captured somewhere by a fault
handler.
The A ‖ A is a simplification of activities’ parallel com-
position (flow). To focus more on the novel aspects of WS-
BPEL, including the fault and compensation handling, we put
some restrictions over this construct so that links between its
components (i.e. additional control-flow restrictions) are dis-
allowed in BPEL∗. We can do so because this issue is almost
orthogonal to our focus in this paper and it has already been
well investigated by researchers, e.g. [11, 12].
Inside a scope n : {A ? C : F}, A is the normal activity, C
is the compensation handler, and F is the fault handler. In
BPEL∗, we assume all names for variables defined in a busi-
ness process are distinct, so are the scope names. This is just
for simplicity and does not lose generality as we can easily
achieve this by a pre-processing step. Under such assump-
tions, we can refer to a variable or a scope simply by its name,
with no need of mentioning its enclosing context. We also
assume that the processes under consideration have been stat-
ically checked to meet certain basic well-formedness condi-
tions. For instance, the compensation activity  n will only

Front. Comput. Sci. China
3
occur in the immediate enclosing scope of the scope n.
3 Dynamic Semantics
In this section, we propose a big-step operational semantics
for BPEL∗. The semantics not only serves as a runtime model
for the language, but also acts as a reference semantics in
the soundness proof for our axiomatic verification system. In
what follows, we will define the runtime states used for the
semantics and then depict the semantic rules.
3.1 Runtime States
The nontrivial business processes need often to support long-
running transactions (LRTs), where the exceptional faults are
unavoidable, and as a result the partially completed tasks may
need to be revoked accordingly. This kind of processes are
hard to describe without language support. WS-BPEL deals
with this necessity with its scope and compensation mech-
anism, which can be invoked to reverse partially completed
transactions. Since a fault may happen from time to time,
the WS-BPEL specification advocates to keep records of state
snapshots for the successfully completed scopes, as the asso-
ciated compensation handlers may refer to such completion
states when the compensation is invoked. Our semantics will
record those successfully completed scope snapshots in the
runtime state, similar to the way used in Qiu et al. [6] for
recording compensation closures. To facilitate the handling
of faults, we also instrument the runtime state with a boolean
value to indicate whether the current state is a normal state or
a faulty state. The formal notations we use are as follows:
f ∈ Status =df {fail, norm}
s ∈ Val =df Var ⇀ Value
α, [δ, . . . , δ] ∈ CPCtx =df seq CPCl
δ, 〈n, s, α〉 ∈ CPCl =df ScopeN × Val × CPCtx
σ, (f, s, α) ∈ Σ =df Status × Val × CPCtx
In the semantic model, a runtime state σ = (f, s, α) is com-
posed of three elements, where f indicates whether the cur-
rent state is normal (f = norm) or of a fault (f = fail), and the
s records current snapshot for the values of all variables in
the process. The third element α is the compensation context
used to record the state snapshots and relative compensation
information for successfully completed scopes.
When a compensation activity n runs, the code to be ex-
ecuted (i.e. the compensation handler defined in scope n) is
statically determined. However, the behavior of the compen-
sation will depend on not only the scope snapshot of n, but
also the dynamic execution of the normal activity in scope n
that yields the state snapshot. This is due to the fact that (1)
the current compensation may invoke compensation handlers
from the immediate sub-scopes of n, so its behavior will de-
pend on whether or not each of the sub-scopes has completed
successfully (thus the associative compensation handler has
been installed) and (2) such information is determined dy-
namically during the execution of the normal activity of scope
n. To record such information along with the scope snapshot,
we define the compensation context α as a (possibly empty)
sequence of compensation closures [δ1, δ2, . . . , δn], whereby
a compensation closure δi = 〈n, s, α1〉 is a nested structure
which records the state snapshot s for scope n (i.e., the data
state at the end of the normal execution of scope n). The third
element α1 is the compensation context accumulated during
the execution of the normal activity of scope n. It includes
all the compensation closures for those normally completed
immediately-enclosed sub-scopes. When the compensation
handler of n is invoked, both the scope snapshot s and the en-
closed context α1 are restored for the compensation activity.
We do not record the handlers in the context as such in-
formation can be statically determined for a given business
process. Instead, we assume the availability of a mapping to
fetch the corresponding handlers:
C : ScopeN → P
where ScopeN is the set of scope names. For a valid scope
name n ∈ dom(C), C(n) ∈ P is the compensation handler de-
fined in scope n.
We will make use of standard sequence operators given
below (where α1 = [δ1, . . . , δm] and α2 = [δ′1, . . . , δ′n]):
δ0 · α1 = [δ0, δ1, . . . , δm]
hd(α1) = δ1
tl(α1) = [δ2, . . . , δm]
α1aα2 = [δ1, . . . , δm, δ′1, . . . , δ′n]
We define a membership relation as follows:
δ∈α =df



false if α = [ ]
true if hd(α) = δ
δ∈tl(α) else
δ /∈α =df ¬(δ∈α)
Based on it we can define the following analogous relation:
n∈α =df ∃s, α1 • 〈n, s, α1〉 ∈ α
n/∈α =df ¬(n∈α)
where n is a scope name and α is a compensation context.
Informally, n∈α indicates that the compensation handler for
the scope n has been installed (and hence n’s scope snapshot
appears in α).
3.2 Operational Semantics
In this subsection, we present the semantic rules for the pro-
cesses in BPEL∗. The big-step operational semantics for
BPEL∗ is defined by a set of rules of the form
〈A, σ〉 σ′
where A is a process, while σ and σ′ denote the initial and
final states, respectively.

4
Frontiers of Computer Science in China Instruction for authors
When a fault has occurred, the process to be executed will
do nothing but propagate the fault. The rule below describes
this scenario:
σ = (fail, s, α)
〈A, σ〉 σ
The following rules define the behavior of skip, assign-
ment, and throw activities from normal states:
〈skip, (norm, s, α)〉 (norm, s, α)
〈x := e, (norm, s, α)〉 (norm, s ⊕ {x7→s(e)}, α)
〈throw, (norm, s, α)〉 (fail, s, α)
where s ⊕ s′ is a state formed by s and s′:
(s ⊕ s′)(x) =df
{
s′(x) when x ∈ dom s′
s(x) otherwise
With s(e) to denote the value of expression e under state s,
the skip and assignment are analogous to normal imperative
language. The throw here changes the process faulty state to
fail immediately, resulting in its propagation to all following
activities until the end of the enclosing scope or the whole
business process, where it will be dealt with by the fault han-
dler.
When synchronized communication activity inv a x y suc-
ceeds, the value received from a, the other end of communica-
tion, is assigned to y; while failed communication also makes
the process fail.
〈inv a x y, (norm, s, α)〉 (norm, s ⊕ {y 7→ν}, α)
〈inv a x y, (norm, s, α)〉 (fail, s, α)
where ν is the value achieved through the communication.
The rules for the one-way communications rec a y and
rep a x are as follows:
〈rec a y, (norm, s, α)〉 (norm, s ⊕ {y 7→ν}, α)
〈rec a y, (norm, s, α)〉 (fail, s, α)
〈rep a x, (f, s, α)〉 (f, s, α)
Note that the one-way communications provide an invocation
mechanism for external Web services. The rec a y is used to
retrieve parameters from other Web services (a). Its effect is
to update variable y using the value received from the external
Web service. On the contrary, the rep a x replies to other
external Web services (a) with the value of x. Thus its effect
is just like a skip to the current process.
Rules for sequence and conditional activities are routine:
〈A1, (norm, s, α)〉 (f1, s1, α1)
〈A2, (f1, s1, α1)〉 (f2, s2, α2)
〈A1; A2, (norm, s, α)〉 (f2, s2, α2)
s(b) = true 〈A1, (norm, s, α)〉 (f1, s1, α1)
〈if b then A1 else A2, (norm, s, α)〉 (f1, s1, α1)
s(b) = false 〈A2, (norm, s, α)〉 (f1, s1, α1)
〈if b then A1 else A2, (norm, s, α)〉 (f1, s1, α1)
The rule for the parallel composition is as follows:
(s1, s2) = split(s,Var(A1),Var(A2))
〈A1, (norm, s1, [ ])〉 (f1, s′1, α1)
〈A2, (norm, s2, [ ])〉 (f2, s′2, α2)
f ′ = f1∧f2 s′ = s′1∪s′2 α′ = interleave(α1, α2)aα
〈A1 ‖ A2, (norm, s, α)〉 (f ′, s′, α′)
where the splitting of variable mappings is based on the sep-
aration of variable names:
split(s,Var(A1),Var(A2)) =df
({x1 7→ e1 | x1 ∈ Var(A1)} ∧ x1 7→e1 ∈ s,
{x2 7→ e2 | x2 ∈ Var(A2) ∧ x2 7→e2 ∈ s}).
in which Var(A1) ∩ Var(A2) = ∅. And for f1 and f2, f1∧f2 is
defined as
f1 ∧ f2 =df
{
norm, if f1 = norm and f2 = norm;
fail, otherwise.
The initial sub-states s1 and s2 are obtained from the overall
state s via a splitting operation whose definition is straight-
forward given that A1 and A2 do not share variables, i.e.,
Var(A1) ∩ Var(A2) = ∅. The function interleave(α1, α2) re-
turns a merged sequence of α1 and α2 by arbitrarily interleav-
ing elements of α1 and α2:
interleave(α1, α2) =df [δ1, δ2, . . . , δm+n]
where we denote α1 = [δ1,1, δ1,2, . . . , δ1,m] and α2 =
[δ2,1, δ2,2, . . . , δ2,n], and then the following holds: δi ∈
α1aα2, i = 1, 2, . . . ,m + n; ∀ 1 ≤ i < j ≤ m + n, if δi,
δj ∈ α1, δi = δ1,s and δj = δ1,t, then s < t; and the same
condition for α2.
The execution of a scope n : {A ? C : F} may result in two
different situations: the execution of A may complete suc-
cessfully or raise a fault. For the former, the compensation
handler will be installed by adding the compensation closure
into the compensation context. For the latter, the fault handler
is invoked instead.
〈A, (norm, s, [ ])〉 (norm, s1, α1) s′ = s1⌋V (n)
〈n : {A ? C : F}, (norm, s, α)〉 (norm, s1, 〈n, s′, α1〉 · α)
〈A, (norm, s, [ ])〉 (fail, s1, α1)
〈F, (norm, s1, α1)〉 (f2, s2, α2)
〈n : {A ? C : F}, (norm, s, α)〉 (f2, s2, α2)
Here V (n) denotes the set of local variables of scope n, and
s1⌋V (n) takes the part of state local to n, which is the snapshot
of scope n when it completes execution.
Note that the scope is the only part in the model to deal
with faults. Once a fault is propagated from an activity A
to its enclosing scope, it will be caught by the relevant fault
handler F. If the fault handler of the immediately enclosing
scope of A throws the fault again rather than completes the
handling, the fault continues its propagation to the next fault

Front. Comput. Sci. China
5
handler, or meets the end of the process. This is elaborated in
the rules defined above.
Next comes the definition of compensation. According to
the WS-BPEL Specification [4], our compensation looks for
the installed compensation closure of corresponding scope,
removes it from the compensation context and runs its han-
dler. If the closure is not installed, the invocation behaves like
a skip. Since we have actually accumulated the compensation
contexts, it turns out simple to execute the handler as below:
n /∈ α
〈n, (norm, s, α)〉 (norm, s, α)
σ = (norm, s, α1a[〈n, s′, β〉]aα2)
〈C(n), (norm, s ⊕ s′, β)〉 (f1, s1, γ)
〈n, σ〉 (f1, s1, α1aα2)
Note that n /∈ α, defined in last section, means that the com-
pensation handler for n is not installed (hence the closure for
n does not appear in α).
The rules for the whole business process are as follows:
〈A, σ〉 (norm, s1, α1)
〈{| A : F |}, σ〉 (norm, s1, α1)
〈A, σ〉 (fail, s1, α1)
〈F, (norm, s1, α1)〉 (f2, s2, α2)
〈{| A : F |}, σ〉 (f2, s2, α2)
There is no top-level compensation handler in the business
process because no one could invoke it if there were any.
4 An Axiomatic System for BPEL∗
As a first step to support mechanized verification for BPEL∗
processes, we propose in this section a set of inference rules
in the style of a Floyd-Hoare logic.
4.1 Assertion Language
To specify properties for BPEL∗ processes, apart from the
usual logical operations, we shall make use of some logical
constructs that are specific for compensation related reason-
ing. The syntax for the assertion language Assn is:
P ∈ Assn
P ::= true | false | normal | x⊙∼e | ∼P | Pǫ | P⌋V |
P+n | P−n | P↾n | P∗n | P||P | P⋆P | P∗P |
¬P | P∧P | P∨P | P⇒P
Note that x, e and n denote a variable name, an expression
and a scope name, respectively. The ⊙∼ denotes a relational
operator in {=, <,>,≤,≥}.
In the axiomatic system, each assertion is viewed as a set
of states that satisfy the assertion. The semantics for all asser-
tions is given in Figure 2.
Among all assertion constructs, true and false are modeled
as the whole and empty sets of states, respectively. Semantics
|[true]| = Σ
|[false]| = ∅
|[x]|σ = σ.2(x)
|[normal]| = {σ | σ.1 = norm}
|[e]|σ = σ.2(e) which is the evaluation result of
e under state σ
|[x⊙∼e]| = {σ | |[x]|σ⊙∼|[e]|σ},where ⊙∼ has the
semantics of the relational operator
|[∼P]| = {(¬σ.1, σ.2, σ.3) | σ ∈ |[P]|}
|[Pǫ]| = {(σ.1, σ.2, [ ]) | σ ∈ P}
|[P⌋V]| = {(σ.1, σ.2⌋V, σ.3) | σ∈|[P]|}
|[P+n]| = {(σ.1, σ.2, 〈n, σ.2⌋V (n), σ.3〉) | σ ∈ |[P]|}
|[P−n]| = {(σ.1, σ.2, α) | σ ∈ |[P]| ∧ α =
before(n, σ.3)aafter(n, σ.3)}
|[P↾n]| = {σ | σ∈|[P]| ∧ n∈σ.3}
|[P∗n]| = {firstof(n, σ) | σ∈|[P]| ∧ n∈σ.3}
|[P||Q]| = {(σ.1 ∧ σ′.1, σ.2 ∪ σ′.2, α) | σ∈|[P]|∧
σ′∈|[Q]| ∧ α=interleave(σ.3, σ′.3)}
|[P⋆Q]| = {(σ1.1, σ1.2, σ1.3aσ2.3) | σ1∈|[P]|∧
σ2∈|[Q]|}
|[P∗Q]| = {(σ1.1, σ1.2, σ2.3) | σ1∈|[P]| ∧ σ2∈|[Q]|}
|[¬P]| = Σ \ |[P]|
|[P ∧ Q]| = |[P]| ∩ |[Q]|
|[P ∨ Q]| = |[P]| ∪ |[Q]|
|[P ⇒ Q]| = |[¬P ∨ Q]|
Fig. 2 Semantics for Assertions
for normal contains all states without fault. Assertion x⊙∼e
can be in forms x<e, x=e, x>e and so forth, to model the
relationship between variable x and expression e.
To facilitate the description, we use here (and below) σ.i
to denote the i-th element of tuple σ. For instance, given
σ = (f, s, α), we will have σ.1 = f, σ.2 = s and σ.3 = α. In
the definition, n∈σ.3, defined in last section, denotes that the
compensation handler for scope n is installed in σ. We also
use three operations to extract information w.r.t. scope n from
compensation context α:
firstof(n, σ) =df (norm, σ.2⊕ s, β)
if σ.3 = α1a[〈n, s, β〉]aα2 ∧ n /∈ α1
before(n, α)=df
{
α, if n /∈ α
α1, if α=α1a[〈n, s, β〉]aα2 ∧ n/∈α1
after(n, α) =df
{
[ ], if n /∈ α
α2, if α=α1a[〈n, s, β〉]aα2 ∧ n/∈α1
Operation firstof(n, σ) extracts from α = σ.3 the first state
snapshot for n, and merges it with σ.2. In the case n /∈ σ.3,
firstof(n, σ) is undefined. before(n, α) returns the largest pre-
fix of α which contains no closure for scope n, and after(n, α)
returns the sub-sequence of α after the first closure for scope
n, or the empty sequence when there is no such closure in α.
Among the semantics for the assertions, some relating to
flow, scope, and compensation are worth illustration.

6
Frontiers of Computer Science in China Instruction for authors
The assertions P⌋V and P||Q are used in verification of flow
constructs. In the first one, V is a set of variables and P⌋V re-
stricts the domain of variable mapping σ.2 (where σ ∈ |[P]|) to
V. For example, (x>0 ∧ y≤0)⌋{x} = x>0. The second one,
P||Q, enumerates all possible interleaving cases of compensa-
tion contexts of states in |[P]| and |[Q]|, respectively.
The following assertions mainly concern scope and com-
pensation. ∼P reverses all the faulty states in each σ ∈ |[P]|
(from norm to fail and vice versa). This corresponds to the
verification of throw activity and fault handler which change
the process faulty state. Pǫ reserves the first and second com-
ponents of states but empties their compensation contexts.
This is useful for verifying scopes whose inner activity A be-
gins with empty compensation context.
Assertion P+n extracts each state σ from set |[P ]|, sets its
compensation context to the closure 〈n, σ.2⌋V (n), σ.3〉, and
forms a new set with all of these states.
As its form suggests, P−n performs an “elimination” of
scope name n “from” the elements in |[P]|. It extracts first
the compensation context α from each state of |[P]|, then finds
the first compensation closure with name n, and removes it to
form a new context α. If there is no such closure found, then
α will be the original context. The semantics of P−n is the
set of states with these newly formed α.
What P↾n does is, informally, to “restrict” |[P]| to the set of
states in which the compensation context contains a closure
with name n, P∗n “locates” the first occurrence of the closure
with name n in each state in |[P]|, and forms a set of states
from these closures.
P⋆Q and P∗Q are for compensation contexts concatena-
tion and replacement between assertions, respectively. The
first appends the compensation contexts within Q’s model to
those of P’s, to accumulate new compensation closure based
on old ones, according to scope’s behavior. The second dis-
cards directly the compensation contexts of the states in P’s
semantics, because of the manner of compensation handlers.
An assertion is modeled as a set containing all the states
which satisfy it. Thus we define
σ |= P =df σ ∈ |[P]|.
A specification in our system takes the ordinary form
{P} A {Q}, where P,Q ∈ Assn and A ∈ P is an activity.
One thing notable is that a business process may commu-
nicate via activities inv, rec and rep with external processes,
which are essentially other Web services within the same ap-
plication or from third party. As a result, whether a business
process behaves in a desired way might depend on the ex-
ternal processes being interacted with. Hence, a business pro-
cess is more like an open system which makes the verification
problem rather challenging. Our proposal is to verify each
business process separately according to certain dependency
order in the first step. We assume that specifications for com-
munication activities are available in the verification of one
business process. When all relevant business processes have
been verified separately, we can then check the consistency of
all the assumptions made on communication activities. In this
paper, we focus only on the verification of individual business
processes.
Remembering that in the operational semantics for com-
munications with external Web services, we have addressed
that their behaviors can be arbitrary, either to deliver a value
or to fail. However, to verify a business process involving
communications more precisely, we need to put more restric-
tions over semantics of the communications. These restric-
tions take the form of a set of specifications {P} c {Q}, where
each c is any one of inv a x y, rec a y, or rep a x, represent-
ing a communication that might be executed by the process
with the environment. We use T to denote a set of such spec-
ifications and use it as a context of the verification rules. For
example, for a specification {P} inv a x y {Q} ∈ T , the pre-
condition P acts as an assertion imposed on the current pro-
cess to ensure that information sent out (the value of x) sat-
isfies the requirement of the environment, while Q acts as an
assumption made on the environment: the result sent back
by the environment (final value of y) satisfies the constraint
described by Q, with a possible substitution of the communi-
cation channel and variable names.
The proof rules in our verification system are of the form
C, T ⊢ {P} A {Q}, where C, defined earlier, is the mapping
from scope names to associated compensation handlers, and
T is the set of specifications defined above. We shall now
present the syntax-directed proof rules in our logic.
4.2 Consequence Rule
The only structural rule in our axiomatic system is the con-
sequence rule for precondition weakening and postcondition
strengthening:
P ⇒ P′ C, T ⊢ {P′} A {Q′} Q′ ⇒ Q
C, T ⊢ {P} A {Q} (conseq)
4.3 BPEL∗-specific Rules
The rules for skip and assignment are simple:
C, T ⊢ {P} skip {P} (skip)
C, T ⊢ {normal ∧ P [e/x]} x := e {P} (assign)
The rule for throw is clear too:
C, T ⊢ {P} throw {¬normal∧(P∨∼P)} (throw)
Here we do not need to care whether the pre-condition is nor-
mal, because the type of fault is not in the range of our current
consideration.
For the basic communication activities, the rules need to
use their assumed specifications in T . For the convenience
of description, we assume the variable names in the pre-
and postconditions are correspondent with those used in the
invocations. Meanwhile, as is stated in former section, in
the verification of the process, a triple {P} A {Q} in T can

Front. Comput. Sci. China
7
also be used to verify a triple whose pre- and postcondition
have the same denotation of compensation contexts, such as
{P⋆R} A {Q⋆R}. And in this situation it must be guaranteed
that the denotations of compensation contexts in both pre- and
postcondition are the same.
If the environment can be modeled as a subset of normal,
then rec sets the variable’s value to what the specification de-
notes. Or it just propagates the fault.
{normal} rec a v {Q} ∈ T
¬normal ⇒ Q [v/y]
C, T ⊢ {true} rec a y {Q [v/y]} (rec)
where Q [v/y] is an assertion formed by substituting each
occurrence of v in Q by y, for filling the gap between the
specification in T and the current process. Because of rep’s
analogous behavior to skip, its rule is also the same.
C, T ⊢ {P} rep a x {P} (rep)
The semantics of two-way invocation is simple:
{P} inv a u v {Q} ∈ T
C, T ⊢ {P} inv a x y {Q [u, v/x, y]} (inv)
Note that these rules depend on T – the set of specifications
assumed on communication activities.
The rules for control structures are as follows.
¬normal ∧ P ⇒ Q
C, T ⊢ {normal ∧ P} A {R}
C, T ⊢ {R} B {Q}
C, T ⊢ {P} A; B {Q} (seq)
¬normal ∧ P ⇒ Q
C, T ⊢ {normal ∧ P ∧ b} A {Q}
C, T ⊢ {normal ∧ P ∧ ¬b} B {Q}
C, T ⊢ {P} if b then A else B {Q} (if)
where b is a boolean expression of the form x⊙∼e.
Since we assume that the different parallel flows share no
variables, the rule for the parallel structures is given as
¬normal ∧ P ⇒ (Q1||Q2)⋆P
C, T ⊢ {Pǫ⌋V1} A {Q1}
C, T ⊢ {Pǫ⌋V2} B {Q2}
C, T ⊢ {P} A||B {(Q1||Q2)⋆P}
(flow)
where V1 and V2 are disjoint variable sets and A and B only
modify variables in V1 and V2, respectively.
Now we present the two most significant rules, which re-
veal the essential features of our language. The rule for scopes
is as follows:
¬normal ∧ P ⇒ Q
C, T ⊢ {normal ∧ Pǫ} A {R}
(normal ∧ R)+n⋆P ⇒ Q
C, T ⊢ {∼(¬normal ∧ R)} F {Q}
C, T ⊢ {P} n : {A ? C : F} {Q} (scope)
Note that the rule (scope) captures two cases. One stands for
the scenario where a fault occurs in A. In that case the control
transfers to the fault handler, and the compensation handler
for scope n is not installed. The other is for the normal com-
pletion of A and the concatenation of this scope’s compensa-
tion context to the process state.
Then the most intricate rule in our system, the named com-
pensation, comes as follows:
¬normal ∧ P ⇒ Q
¬P↾n ∧ P ⇒ Q
C, T ⊢ {(P↾n)∗n} C(n) {R}
R∗P−n ⇒ Q
C, T ⊢ {P} n {Q} (compensate)
In this rule, the behavior of a named compensation is depicted
with the relevant compensation handler. If the pre-condition
does not entail a scope name n, the post-condition must be
automatically satisfied. Otherwise, the snapshots’ set (as the
pre-condition for the compensation handler) is extracted and
the post-condition is a combination of the fault and variable
mapping states after the handler’s execution, and the compen-
sation context with the elimination of the first compensation
closure named n.
At last is the rule for the whole business process:
C, T ⊢ {P} A {R}
(normal ∧ R) ⇒ Q
C, T ⊢ {∼(¬normal ∧ R)} F {Q}
C, T ⊢ {P} {| A : F |} {Q} (bp)
5 Soundness
This section is devoted to the soundness of our verification
system. We will first give two definitions and then formalize
the soundness theorem and its proof.
Definition 1 (Validity). We denote that a triple {P} A {Q}
is valid under C, T, i.e. C, T |= {P} A {Q}, if for all σ ∈ Σ, if
σ |= P and 〈A, σ〉 σ′ for some σ′, then σ′ |= Q.
Definition 2 (Soundness). Our verification system for
BPEL∗ is sound if all provable specifications are indeed valid,
that is, if C, T ⊢ {P} A {Q}, then C, T |= {P} A {Q}.
The theorem for soundness can be stated as below:
Theorem 1. The Hoare logic for BPEL∗ presented in this
paper is sound.
As is indicated by Definition 2 above, we need to show
that, for any P,A,Q, if C, T ⊢ {P} A {Q}, then C, T |=
{P} A {Q}. The proof can be accomplished by structural in-
duction over A.

8
Frontiers of Computer Science in China Instruction for authors
Proof. The verification of C, T ⊢ {P} A {Q} (denoted as t)
can be a process such as
(some premises)
.
.
.
··· · · ·
(some other premises)
.
.
.
···
C, T ⊢ {P} A {Q}
From the perspective of backwards reasoning, a rule r should
be utilized on t according to A’s structure, and from this rule
some other premises need to be verified with similar back-
ward verifications until all the premises are axioms or known
facts. As an illustration, if A is C, T ⊢ {P} {| A1 : F1 |} {Q},
then we must verify C, T ⊢ {P} A {R}, (normal ∧ R) ⇒ Q
and C, T ⊢ {∼(¬normal ∧ R)} F {Q}, according to the (bp)
rule. Hence the last rule r used to verify t depends on the
structure of the activity A. Therefore, the following cases are
organized according to the structure of A, which is equivalent
to r to some extent.
• Case (skip). The last rule r for this is (skip):
C, T ⊢ {P} skip {P}
Since 〈skip, σ〉 σ, it is easy to see that rule (skip) is
sound in our system.
• Case (x := e). The corresponding rule is (assign):
C, T ⊢ {normal ∧ P[e/x]} x := e {P}
The proof for rule (assign) simply follows the canonical
Hoare logic’s proof using the Substitution Theorem and
thus is omitted here.
• Case (throw). The last rule to apply is (throw):
C, T ⊢ {P} throw {¬normal ∧ (P ∨ ∼P)}
Take any σ such that σ |= P. If σ.1 = fail, then we
have 〈throw, σ〉 σ and σ |= ¬normal ∧ P. Other-
wise, if σ.1 = norm, then we have 〈throw, σ〉 σ′
where σ′ = (fail, σ.2, σ.3), and σ′ |= ¬normal∧ ∼P. So
we get C, T |= {P} throw {¬normal ∧ (P ∨ ∼P)}.
• Case (rec a y).
{normal} rec a v {Q} ∈ T
¬normal ⇒ Q [v/y]
C, T ⊢ {true} rec a y {Q [v/y]}
For the proof of the rule (rec), if σ |= normal, then
since {normal} rec a v {Q} is already known for the
communication, the model of postcondition Q [v/y]
should contain the final state transited from σ (ei-
ther (norm, σ.2⊕ {y 7→ν}, σ.3) or (fail, σ.2, σ.3), ac-
cording to the communication’s behavior). Other-
wise if σ |= ¬normal, then from the semantics for
¬normal ⇒ Q [v/y] we know σ |= Q [v/y]. Therefore
we conclude in this case.
• Case (rep a x).
C, T ⊢ {P} rep a x {P}
Since the communication of reply does not change the
process status, rule (rep) shares the same proof of skip’s.
• Case (inv a x y).
{P} inv a u v {Q} ∈ T
C, T ⊢ {P} inv a x y {Q [u, v/x, y]}
The proof can be completed in the similar way as that of
rec a y.
• Case (A; B). The rule applied in this case is (seq):
¬normal ∧ P ⇒ Q
C, T ⊢ {normal ∧ P} A {R}
C, T ⊢ {R} B {Q}
C, T ⊢ {P} A; B {Q}
The proof for rule (seq) is classical, except that the faulty
state is taken into consideration first. That is, for any
state σ |= P, if σ.1 = fail, then σ |= ¬normal ∧ P and
thus σ |= Q. If not, then take σ∗ as 〈A, σ〉 σ∗, we
have σ∗ |= R. And from 〈B, σ∗〉 σ′ and the inductive
assumption, it holds that σ′ |= Q.
• Case (if b then A else B). In this case the condition rule
(if ) is applied:
¬normal ∧ P ⇒ Q
C, T ⊢ {normal ∧ P ∧ b} A {Q}
C, T ⊢ {normal ∧ P ∧ ¬b} B {Q}
C, T ⊢ {P} if b then A else B {Q}
The proof of the condition rule is also similar as the
classical one. Except for the abnormal state, consider
any σ where σ.1 = norm. Then no matter whether
σ |= normal ∧ P ∧ b or σ |= normal ∧ P ∧ ¬b, for some
σ′ and σ∗ that 〈A, σ〉 σ′ in the first case and
〈B, σ〉 σ∗ in the second, we always get σ′ |= Q and
σ∗ |= Q from inductive assumption.
• Case (A ‖ B). The last rule used is (flow):
¬normal ∧ P ⇒ (Q1||Q2)⋆P
C, T ⊢ {Pǫ⌋V1} A {Q1}
C, T ⊢ {Pǫ⌋V2} B {Q2}
C, T ⊢ {P} A||B {(Q1||Q2)⋆P}
Take any σ |= normal ∧ P (the case for σ.1 = fail is
like other rules), from the premises and the inductive
assumption we know that 〈A, (σ.1, σ.2⌋s1 , [ ])〉 σ′1
and 〈B, (σ.1, σ.2⌋s2 , [ ])〉 σ′2, for some σ′1 |= Q1,
σ′2 |= Q2. Hence (σ′1.1 ∧ σ′2.1, σ′1.2 ∪ σ′2.2, interleave
(σ′1.3, σ′2.3)aσ.3) |= (Q1||Q2)⋆P, and thus we conclude
in this case.

Front. Comput. Sci. China
9
• Case (n : {A ? C : F}). Rule (scope) is the last rule ap-
plied in the proof for C, T ⊢ {P} n : {A ? C : F} {Q}:
¬normal ∧ P ⇒ Q
C, T ⊢ {normal ∧ Pǫ} A {R}
(normal ∧ R)+n⋆P ⇒ Q
C, T ⊢ {∼(¬normal ∧ R)} F {Q}
C, T ⊢ {P} n : {A ? C : F} {Q}
The following cases are discussed for all σ |= P.
– If σ.1 = fail, from inductive assumption and
the premise ¬normal ∧ P ⇒ Q, we have σ |=
¬normal ∧ P, and thus σ |= Q.
– If σ.1 = norm, then take σǫ = (σ.1, σ.2, [ ]), and
hence we have σ |= normal ∧ Pǫ. With induc-
tive assumption and the premise, denoting σ′ǫ as
〈A, σǫ〉 σ′ǫ, then σ′ǫ |= R is achieved.
∗ If σ′ǫ.1 = norm, then σ′ǫ |= normal ∧ R, and
σ′+n = (σ′ǫ.1, σ′ǫ.2, 〈n, σ′ǫ.2⌋V (n), σ′ǫ.3〉) |=
(normal ∧ R)+n, and still σ′ = (σ′+n.1,
σ′+n.2, σ′+n.3 · σ.3) |= (normal ∧ R)+n⋆P.
We get σ′ |= Q from the last implication.
∗ If σ′ǫ.1 = fail, then σ′F |= ∼(¬normal ∧ R)
where σ′F = (norm, σ′ǫ.2, σ′ǫ.3). From the
inductive assumption and the semantics
〈F, σ′F〉 σ′ for some σ′, we have σ′ |= Q.
This completes our proof for scope.
• Case (n):
¬normal ∧ P ⇒ Q
¬P↾n ∧ P ⇒ Q
C, T ⊢ {(P↾n)∗n} C(n) {R}
R∗P−n ⇒ Q
C, T ⊢ {P} n {Q}
For the rule of compensation, consider any σ |= P in the
following cases.
– If σ.1 = fail, then directly we have σ |= Q.
– If σ.1 6= fail and there are no compensation clo-
sures named n in σ’s compensation context, then
σ |= ¬P↾n ∧ P by definition, and thus σ |= Q
which conforms to the operational semantics.
– Otherwise, we need to run the compensation han-
dler named n. Denote σn = firstof(n, σ), and we
have σn |= (P↾n)∗n and hence 〈C(n), σn〉 σ′n
for some σ′n, while σ′n |= R. Then take
σ = (f, σ, α1a[〈n, σ∗, β〉]aα2), and we have
σ′ = (σ′n.1, σ′n.2, α1aα2) |= R∗P−n, and thus
σ′ |= Q. From all discussion above, we conclude
this case.
• Case ({| A : F |}). The last rule applied in the proof for
the whole business process will be the rule (bp):
C, T ⊢ {P} A {R}
(normal ∧ R) ⇒ Q
C, T ⊢ {∼(¬normal ∧ R)} F {Q}
C, T ⊢ {P} {| A : F |} {Q}
It is similar as the scope rule with compensation handler
eliminated. For any σ |= P and 〈A, σ〉 σ′ for some σ′
there are the following two cases:
– σ′.1 = norm. From (normal ∧ R) ⇒ Q, we know
that σ′ |= Q.
– σ′.1 = fail. If 〈F, (norm, σ′.2, σ′.3)〉 σ∗ for
some σ∗, then we have σ∗ |= Q from the premise
C, T ⊢ {∼(¬normal ∧ R)} F {Q}.
• Besides the aforesaid A’s possible structures directly re-
lated to rules, sometimes we may be not able to verify
C, T ⊢ {P} A {Q} with an existing rule but can verify
C, T ⊢ {P′} A {Q′} where P′ is weaker than P and/or Q′
is stronger than Q. Thus the structural rule (conseq) is
employed in such cases:
P ⇒ P′ C, T ⊢ {P′} A {Q′} Q′ ⇒ Q
C, T ⊢ {P} A {Q}
For all σ |= P and 〈A, σ〉 σ′ for some σ′, we have
σ |= P′ from P ⇒ P′ and also 〈A, σ〉 σ∗ for some
σ∗ |= Q′. Then from Q′ ⇒ Q we get σ∗ |= Q. Hence
σ∗ is the σ′ we need and the proof for this rule is com-
pleted.
Above are all the cases of our structural induction, and
each of them is proven to be sound. Hence this completes
our proof for the soundness. 2
6 Example
In this section a purchase example is exhibited to illustrate
the verification of a real business process, which is a modified
version of that in [13].
The general flow of the example is as follows. First the
process receives the price for each single item (stored in vari-
able p) and the class of the customer from other service with
communication (into variable y). Then it decides the discount
ratio according to the customer class, and receives the amount
of items to store in t. After having all the items purchased, it
computes the shipping fare according to the value of t. At last
the real average price (including shipping cost) for each item
is calculated and replied, which may incur fault and hence call
for compensation.
This business process, denoted as BP, is written in BPEL∗
below.
{|
n1 : {rec a p; q := p ? p := −p : skip};
rec b y;
if y = 1 then
n2 : {p := p× 0.5 ? p := p× 2 : skip}
else
n3 : {p := p× 0.8 ? p := p× 1.25 : skip};
n4 : {rec c t; p := p× t ? p := p/t : skip};
if t > 500 then
n5 : {p := p + 500 ? p := p− 500 : skip}

10
Frontiers of Computer Science in China Instruction for authors
else
n6 : {p := p + t ? p := p− t : skip };
if t > 0 then p := p/t; rep d p else throw
: n6; n5; n4; n3; n2; n1
|}
The specification for us to verify is {normal} BP {Q}
where Q is p=q/2+500/t ∨ p=0.8q+500/t∨ p=q/2+1∨
p=0.8q+1 ∨ p=−q. The first four parts of the disjunctions in
Q present the different situations of discount ratio and ship-
ping fare, while the last p=− q is the case where a fault is
compensated. This specification states that, if BP starts in
a normal state and terminates at last, it should establish the
postcondition Q, provided that the specifications of the com-
munication activities are as follows:
{normal} rec a y {normal ∧ y>0}
{normal} rec b y {normal ∧ (y=1 ∨ y=2)}
{normal} rec c y {normal ∧ y 6=0}
Here we give an outline of the verification for BP with
the backwards searching strategy. First, for the whole busi-
ness process, we use the rule of bp to get three subgoals
G1, G2, G3 for further verification:
G1 : C, T ⊢ {normal} A {R}
G2 : (normal ∧ R) ⇒ Q
G3 : C, T ⊢ {∼(¬normal ∧ R)} F {Q}
where A stands for the codes before the last : in the pro-
cess, Q is the postcondition we want to verify, F represents
the six compensations (n6; n5; n4; n3; n2; n1), and
R should be both strong enough to derive Q and still suffi-
ciently weak as F’s precondition to get Q. A possible R can
be the assertion below:
(normal ∧ (p=q/2+500/t ∨ p=0.8q+500/t∨
p=q/2+1 ∨ p=0.8q+1)) ∨ (¬normal∧ ∼ P6)
where P6 is
normal∧
((t ≤ 500 ⇒ ((y=1 ⇒ p=0.5qt+ t)∧
(y 6=1 ⇒ p=0.8qt + t))+n5∧
t > 500 ⇒ ((y=1 ⇒ p=0.5qt+ 500)∧
(y 6=1 ⇒ p=0.8qt + 500))+n6)⋆ P5)
where P5 stands for the set of states for compensation ac-
cumulated in the previous execution of the process, from a
semantics perspective (and so are the other assertions to be
depicted below); its definition is
normal∧(((y=1 ⇒ p=0.5qt)∧(y 6=1 ⇒ p=0.8qt))+n4⋆ P4)
where P4 is
normal ∧ (((y=1 ⇒ (p=0.5q)+n2)∧
(y 6=1 ⇒ (p=0.8q)+n3))⋆ P2)
where P2 is
(normal ∧ p=q)+n1⋆ normal
and the semantics and the derivations of these assertions will
be introduced in the following descriptions. With them as
bridges we will try to verify the three subgoals separately.
For the first subgoal G1, it can still be divided into six sub-
goals, since A is a sequence made up of six other activities,
including two scopes, one basic communication activity and
three conditional judgments. We will denote these activities
as A1,A2, . . . ,A6 according to their original orders in BP, and
call these six subgoals G1,i, i = 1, 2, . . . , 6, defined as below:
G1,i : C, T ⊢ {Pi} Ai {Pi+1}
where i = 1, 2, . . . , 6,P1 = normal and P7 = R. (Note that
the P2, . . . ,P5 are what have been described above.) We will
demonstrate the verification of each subgoal.
For G1,1, since A1 is the scope n1 and the precondition
is normal, we will use the scope rule to divide it further into
three subgoals:
G1,1,1 : {normalǫ} rec a p; q := p {P1,1}
G1,1,2 : (normal ∧ P1,1)+n1⋆ normal ⇒ P2
G1,1,3 : {∼(¬normal ∧ P1,1)} skip {P2}
For the first subgoal, the rules seq, rec and assign
are used, to get that P1,1 is normal ∧ p=q. With this
result and the second subgoal the strongest P2 is de-
rived as (normal ∧ p=q)+n1⋆ normal. For the third sub-
goal, since ¬normal ∧ P1,1 = false, it holds automatically.
Then G1,1 is verified with the postcondition P2, that is,
(normal ∧ p=q)+n1⋆ normal.
Next we will examine G1,2. Here the rule of rec is applied
to P2 and rec b y, with the result of postcondition P3 which is
(y=1 ∨ y=2) ∧ P2.
Subgoal G1,3 concerns the first if construct of the process,
and its verification is an application of rule if with the result
of two other subgoals
G1,3,1 : C, T ⊢ {normal ∧ P3 ∧ y=1} A1,3 {P4}
G1,3,2 : C, T ⊢ {normal ∧ P3 ∧ ¬y=1} B1,3 {P4}
where A1,3 and B1,3 are scopes n2 and n3, respectively. They
can be verified similarly as n1 (using rules scope and assign),
and we get the postcondition P4:
normal ∧ q=X∧
((y=1 ⇒ (p=0.5q)+n2∧
y 6=1 ⇒ (p=0.8q)+n3)⋆ P2)
G1,4 is to verify the Hoare triple for scope n4. Fol-
lowing similar way of G1,1 it can be verified with P5 as
normal ∧ (((y=1 ⇒ p=0.5qt) ∧ (y 6=1 ⇒ p=0.8qt))+n4⋆ P4).
G1,5 again seeks the verification of the second if construct.
With the approach like that of G1,3 (splitting it into two sub-
goals) we can achieve P6:
normal∧
((t ≤ 500 ⇒ ((y=1 ⇒ p=0.5qt+ t)∧
(y 6=1 ⇒ p=0.8qt + t))+n5∧
t > 500 ⇒ ((y=1 ⇒ p=0.5qt+ 500)∧
(y 6=1 ⇒ p=0.8qt + 500))+n6)⋆ P5)

Front. Comput. Sci. China
11
The last subgoal, G1,6, is slightly different from the former
two if’s. It is also first divided into two subgoals:
G1,6,1 : C, T ⊢ {normal ∧ P6 ∧ t>0} p := p/t; rep d p {R}
G1,6,2 : C, T ⊢ {normal ∧ P6 ∧ ¬t>0} throw {R}
in which the first subgoal’s verification is as the for-
mer ones, with the postcondition p=q/2+500/t∨
p=0.8q+500/t ∨ p=q/2+1 ∨ p=0.8q+1. (Note that
we omit the part for compensation and present a weaker
assertion here.) However, the second one uses the throw rule
to force a conjunction of ¬normal with the precondition.
Therefore the whole postcondition for A,R, is as follows:
(normal ∧ (p=q/2+500/t ∨ p=0.8q+500/t∨
p=q/2+1 ∨ p=0.8q+1)) ∨ (¬normal∧ ∼ P6)
It is clear that a conjunction of normal and this R automati-
cally implies Q, which is demanded in the subgoal G2. So the
remaining work is to verify the subgoal G3.
G3 equals to C, T ⊢ {t<0 ∧ P6} F {Q}, where F is the se-
quence of six compensations. Similarly, this can be divided
into six subgoals using the seq rule, and each subgoal is
solved equally with rule compensate. We will illustrate its
usage with the first two compensations for scopes n6 and n5,
and the others are the same as these two.
Since t<0 implies that t≤500, it can be deducted that the
compensation context for n6 must be installed, and thus we
have only two possible cases to consider (y=1; y 6=1). We now
take the first case as an example, in which the precondition of
these compensations can be reduced as
normal ∧ y=1 ∧ t≤500∧
(p=0.5qt+t)+n6⋆ (p=0.5qt)+n4⋆
(p=0.5q)+n2⋆ (p=q)+n1⋆ normal
where we denote the ⋆ as right-associative to prevent excess
parentheses. Using once the rule compensate we get
normal ∧ y=1 ∧ t≤500∧
(p=0.5qt)+n4⋆ (p=0.5q)+n2⋆
(p=q)+n1⋆ normal
to remove the compensation context of n6 from the states (on
the level of semantics).
Then for the subgoal concerning n5, since in this case it
is not installed in the compensation context (which can be
seen from the structure of the assertion), its effect, due to rule
compensate, is like a skip.
Therefore we use the rule four times more on ni,
i = 4 . . . 1 respectively, to verify each remaining subgoal and
gain the final assertion
normal ∧ y=1 ∧ t≤500 ∧ p=− q
which implies that p = −q, and hence Q. This completes the
whole process’ verification.
7 Related Work
The concept of compensation dates back to Sagas [14] and
nested transactions [15]. There are a few attempts to formal-
ize workflow languages [3,16–18], and still many of them are
about compensation.
On the semantics of such languages there are many in-
vestigations. Qiu and et al. [6] provided a formal opera-
tional semantics for a simplified version of BPEL4WS to
specify the execution path of a process with possible com-
pensation behavior. In that work, they adopted an abridgment
of BPEL4WS which was followed by a series of works with
similar objective. Then they provided a formal semantics for
fault handling, compensations, and parallel processes with re-
spect to the original informal description by the BPEL4WS
Specification [19], with a clarification to some of its elusive
parts. Meanwhile they proved the completeness of the de-
duction of their semantics. Besides their work, there are still
many others to formalize the semantics of these languages
from different perspectives. Bruni and et al. [20] presented
an operational semantics for a series of languages, which in-
cluded the compensation concept. Pu and et al. [7] also pre-
sented an abridged edition of WS-BPEL, discussed its oper-
ational semantics, and defined the equivalence between two
processes with its proposed n-bi-simulation. He and et al. [9]
focused on the process equivalence from the perspective of
an observation-oriented model and its algebraic laws. Zhu
and et al. [10] made a link among different semantics (op-
erational, denotational and algebraic) of the WS-BPEL lan-
guage with the approach of the unifying theories of program-
ming. Some of the semantics proposed in these works may
also be enhanced as suitable underlying semantics for our ver-
ification system, while our semantics is mainly distinguished
from theirs in that it incorporates variable mappings in both
program runtime states and compensation contexts, enabling
concrete variable valuations to be stored in the semantics.
Apart from the work on semantic models, researchers have
also tried to model and verify the WS-BPEL processes. Duan
and et al. [21] introduced a logic model to formally specify
the semantics of workflow and its composite tasks described
as WS-BPEL abstract processes, and made a deduction of the
weakest precondition for workflow. Another work by Duan
and et al. [22] put some restrictions to such model and found
an algorithm to proof the abstract processes’ correctness. Fu
and et al. [23] proposed some techniques and related tools
to analyze interactions of composite Web services written in
BPEL4WS. The BPEL4WS specifications [19] are first trans-
lated into an intermediate representation, and then verified use
SPIN [24]. Hamadi and Benatallah [17] transformed the for-
mal semantics of the WS-BPEL composition operators to an
expression of Petri nets, and hence allowed the verification
of properties and the detection of inconsistencies both within
and between services. Pu and et al. [25] adopted a similar
method by using model checker UPPAAL [26] to verify the
correctness of BPEL4WS program including temporal prop-
erties. However, none of these works have attempted in veri-
fying WS-BPEL-like fault handling and compensation as we

12
Frontiers of Computer Science in China Instruction for authors
have done in this paper.
8 Conclusions and Future Work
In this paper we proposed an axiomatic system to verify the
correctness of BPEL∗ processes. Here we have concentrated
on an important core subset of WS-BPEL, namely, BPEL∗.
This subset reflects the key features of the language appeal-
ing to us, say, fault states, variable mappings and compensa-
tion contexts; meanwhile it keeps our mechanism both pre-
cise and concise, rather than builds up a huge and compli-
cated system trying to cover all aspects of WS-BPEL. We
have formalized these features into program runtime states,
and created BPEL∗’s operational semantics with state transi-
tion rules, according to the OASIS Standard [4]. Based on
this, we have set up the assertions to abstract and express the
novel language features, leaving the Hoare triples for verifi-
cation and their semantics as a natural result. The verification
rules for BPEL∗ are also formalized after the underlying op-
erational semantics. With respect to such semantics, we have
proven the soundness of this system by structural induction
on BPEL∗’s constructs, and provided an example as an illus-
tration to the verification process of our system.
Our possible future works following this mainly include
two aspects. The first is to extend the logic to cover more lan-
guage features of WS-BPEL. As our original intention is to
propose a concise yet novel system to verify WS-BPEL’s fault
handling and compensation mechanism, we omitted some
language constructs which may cause the verification rule to
be uncontrollable under current model, say, partner links, all
compensation activities and while loops. These language fea-
tures may require further invention of verification techniques
such as invariants on compensation contexts, and are worth
being a natural subsequence of our further work. The second
aspect aims at mechanizing the verification system for prac-
tical use, which involves some kind of verification condition
generators to create the verification conditions, some reason-
ers to discharge the produced subgoals, and some verification
algorithm to integrate these together.
Acknowledgements We appreciate the precious comments from
the anonymous reviewers. This work is supported by UK EPSRC
project EP/E021948/1 and China NNSF project 60773161.
References
1. Thatte S. XLANG: web service for business process de-
sign. http://www.gotdotnet.com/team/xml_wsspecs/xlang-c/
default.htm, Microsoft, 2001
2. Leymann F. WSFL: web services flow language. http://www-
4.ibm.com/software/solutions/webservices/pdf/WSFL.pdf,
IBM, 2001
3. Butler M, Ferreira C. An operational semantics for stac, a lan-
guage for modelling long-running business transactions. In:
Proceedings of Sixth International Conference on Coordina-
tion Models and Languages, LNCS 2949, 2004, 87–104
4. Alves A, Arkin A, Askary S, et al. Web services business pro-
cess execution language version 2.0. http://docs.oasis-open.
org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html, OASIS Standard,
2007
5. Barreto C, Bullard V, Erl T, et al. Web services business pro-
cess execution language version 2.0 primer. http://docs. oasis-
open.org/wsbpel/2.0/Primer/wsbpel-v2.0-Primer.html, OASIS
Standard, 2007
6. Qiu Z, Wang S, Pu G, et al. Semantics of bpel4ws-like fault
and compensation handling. In: Proceedings of International
Symposium of Formal Methods Europe, LNCS 3582, 2005,
350–365
7. Pu G, Zhu H, Qiu Z, et al. Theoretical foundation of
scope-based compensable flow language for web service. In:
Proceedings of International Conference on Formal Methods
for Open Object-Based Distributed Systems (FMOODS’06),
LNCS 4037, 2006, 251–266
8. Qiu Z, Zhao X, Cai C, et al. Towards the theoretical foundation
of choreography. In: Proceedings of Sixteenth International
World Wide Web Conference (WWW 2007), 2007, 973–982
9. He J, Zhu H, Pu G. A model for bpel-like languages. Frontiers
of Computer Science in China, 2007, 1(1):9–19
10. Zhu H, He J, Li J, et al. Algebraic approach to linking the
semantics of web services. In: Proceedings of Fifth IEEE In-
ternational Conference on Software Engineering and Formal
Methods, 2007, 315–328
11. Xu Q, de Roever W, He J. The rely-guarantee method for veri-
fying shared variable concurrent programs. Formal Aspects of
Computing, 1997, 9(2):149–174
12. Zhu H. Linking the semantics of a multithreaded discrete event
simulation language. PhD thesis, London South Bank Univer-
sity, 2005
13. Fowler M, Scott K. UML distilled : a brief guide to the stan-
dard object modeling language. Addison-Wesley, 2000
14. Garcia-Molina H, Salem K. Sagas. In: Proceedings of the
Association for Computing Machinery Special Interest Group
on Management of Data 1987 Annual Conference, 1987, 249–
259
15. Moss J. Nested Transactions: An Approach to Reliable Dis-
tributed Computing. PhD thesis, Massachusetts Institute of
Technology, 1981
16. Aalst W, Dumas M, Hofstede A, et al. Analysis of web services
composition languages: The case of bpel4ws. In: Proceedings
of the 22nd International Conference on Conceptual Modeling,
2003, 200–215
17. Hamadi R, Benatallah B. A petri net-based model for web
service composition. In: Proceedings of the 14th Australasian
Database Conference, 2003, 191–200
18. Brogi A, Canal C, Pimentel E, et al. Formalizing web ser-
vice choreographies. Electronic Notes of Theoretical Com-
puter Science, 2004, 105:73–94
19. Andrews T, Curbera F, Dholakia H, et al. Business process exe-
cution language for web services 1.1. http://download.boulder.
ibm.com/ibmdl/pub/software/dw/specs/ws-bpel/ws-bpel.pdf,
2003
20. Bruni R, Melgratti H, Montanari U. Theoretical foundations
for compensations in flow composition languages. In: Pro-
ceedings of the 32nd ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, 2005, 209–220

Front. Comput. Sci. China
13
21. Duan Z, Bernstein A, Lewis P, et al. Semantics based verifica-
tion and synthesis of bpel4ws abstract processes. In: Proceed-
ings of IEEE International Conference on Web Services, 2004,
734–737
22. Duan Z, Bernstein A, Lewis P, et al. A model for abstract pro-
cess specification, verification and composition. In: Proceed-
ings of the 2nd International Conference on Service Oriented
Computing, 2004, 232–241
23. Fu X, Bultan T, Su J. Analysis of interacting bpel web services.
In: Proceedings of Thirteenth International World Wide Web
Conference (WWW 2004), 2004, 621–630
24. Holzmann G. The Spin Model Checker — Primer and Refer-
ence Manual. Addison-Wesley, 2003
25. Pu G, Zhao X, Wang S, et al. Towards the semantics and verifi-
cation of bpel4ws. In: Proceedings of the International Work-
shop on Web Languages and Formal Methods (WLFM 2005),
2005
26. Bengtsson J, Larsen K, Larsson F, et al. Uppaal — a tool suite
for automatic verification of real-time systems. In: Proceed-
ings of the DIMACS/SYCON Workshop on Hybrid Systems
III : Verification and Control, 1996, 232–243