Information Technology Reference
In-Depth Information
To equip a program with compensation mechanism, it is necessary to characterise
the cases when the control has to be passed to the compensation components.
Following the line adopted by the fault handling model, we introduce a new
logical variable
forward
to describe the status of control flow of the execution
of a program:
-
forward
=
true
indicates successful termination of the execution of the
forward activity of a program. In this case, its successor will carry on with
the initial state set up by the program.
-
forward
=
false
indicates it is required to undo the effect caused by the
execution of the forward activity. In this case, the installed compensation
module will be invoked.
As a result, when a program
Q
is asked to start in a state where
forward
=
false
, it has to meet the following healthiness condition:
Definition 3.4
(Healthiness Condition)
(
Req
2
)
Q
=
II
Q
This condition can be identified by the following mapping
¬
forward
H
2
(
Q
)=
df
II
¬
forward
Q
in the sense that a program satisfies
Req
2
iff it is a fixed point of
H
2
Theorem 3.2
H
2
◦H
1
=
H
1
◦H
2
where
◦
denotes functional composition.
Proof.
From the fact that
H
1
(
H
2
(
Q
)) =
II
eflag
∨¬
foward
Q
=
H
2
(
H
1
(
Q
))
Define
H
=
df
H
1
◦H
2
Theorem 3.3
A design satisfies both
Req
1
and
Req
2
iff it is a fixed point of
H
.
Like the mapping
H
1
,
H
is also a homomorphism.
Theorem 3.4
(1)
H
(
P
Q
)=
H
(
P
)
H
(
Q
)
(2)
H
(
P
b
Q
)=
H
(
P
)
b
H
(
Q
)
(3)
(
Q
)
Definition 3.5
(Design Matrix for exception and rollback)
Define
H
(
P
;
H
(
Q
)) =
H
(
P
);
H
⎛
⎞
D
1
D
2
D
3
⎝
⎠
=
df
H
((
D
1
;
succ
)
⊕
(
D
2
;
error
)
⊕
(
D
3
;
rollback
))
Search WWH ::
Custom Search