Information Technology Reference
In-Depth Information
4
Compensable Programs
The ability to declare compensation logic alongside forware-working logic is
the underpinning of the application-controlled error-handling framework of WS-
BPEL. This section will provide a model for compensable programs which consist
of forward activity (for application task), backward activity (for compensation)
and exception handling component.
A compensable program will be identified as a healthy design with the al-
phabet containing the following variables to record the status of the holder of
compensation program and the values of program variables:
1.
x
and
x
: to stand for the initial value and the final value of variable
x
respectively.
2.
Cseq
: to keep the compensation programs installed so far.
3.
Cpens
: to record the named compensation programs. It is a mapping from
the scope names to their corresponding compensation programs.
4.1
Primitive Commands
The chaotic program
⊥
is defined as usual
⎛
⎝
⎞
⎠
true
true
true
beh
(
⊥
)=
df
The execution of
skip
terminates successfully, leaving both the contents of the
holder of compensation programs and the values of program variables and target
lables unchanged.
⎛
⎞
true
Identity
true
true
⎝
⎠
beh
(
skip
)=
df
where the binary relation
Identity
is defined by
(
v
=
v
)
(
Cpens
=
Cpens
)
(
Cseq
=
Cseq
)
Identity
=
df
∧
∧
The program
fail
stops the execution indicating the failure of the forward
activity.
⎛
⎝
⎞
⎠
true
true
true
beh
(
fail
)=
df
Identity
There is a class of programs which never end the execution with a meaningful
outcome. The assignment
x
:= 1
/
0 belongs to this category. We use the notation
Search WWH ::
Custom Search