Information Technology Reference
In-Depth Information
Denition 1.
Let P be an
OCCAM
or CSP process and p a property of P to be
veried. Let
A
(
p
)
a property dened on CSP
A
(
P
)
denote a CSP process and
; A
(
p
))
is called a valid abstraction for
(
P
level. Then the pair
(
A
(
P
)
;
p
)
,if
A
(
p
) always implies
Psatisesp.
A
(
P
)
satises
t
Abstraction Through Renement.
According to the fact that CSP renement can
be extended to OCCAM and due to the observation that the three correctness
properties under consideration can be expressed as renement properties, a rst
set of valid abstractions can be constructed according to the following rules:
{
To analyse deadlock freedom, property
p
is dened by an assertion of the
type \
P
renes
DF
in the failures model" (formally written as
DF
v
F
P
),
where
DF
is a given deadlock-free process with the same alphabet as
P
.The
abstracted property
A
(
p
) is identical to
p
,thatis
DF
v
F
. Abstraction
process
(
P
) must be chosen such that it is rened by the OCCAM process
system
P
in the failures model. Then, if
DF
A
(
P
)canbeproven,
deadlock freedom of
P
follows from the transitivity of renement.
{
To analyse livelock freedom,
v
F
A
A
(
P
) must be chosen such that it contains the
same interface channels
c
n
g
as
P
andisrenedby
P
in the trace model. Then, if livelock freedom of
A
f
d
1
;
d
2
;:::;
d
`
g
and internal channels
f
c
1
;
c
2
;:::;
can be proven, the same follows for
P
.
{
To analyse correct implementation of the Byzantine protocol (after having
veried deadlock and livelock freedom),
(
P
)
nf
c
1
;
c
2
;:::;
c
n
g
(
P
) must be chosen such that it is
rened by
P
in the trace model. Then, if it can be shown that
A
(
P
) renes
the protocol specication process
BYZAN
in the trace model,
P
is a correct
implementation of the protocol, too.
A
The abstraction principle described above is called
abstraction through re-
nement
(see Roscoe and Peleska et.al. [24,27] for further details on this topic):
concrete (OCCAM or CSP) process and abstract CSP process operate on the
same alphabet and are related by renement. Simplication of the abstrac-
tion process in comparison with the concrete process is only possible by hiding
irrelevant details and increasing nondeterminism through replacing conditions
if
condition
then
P
1
else
P
2
by internal choice
P
1
u
P
2
. This abstraction prin-
ciple has the advantage that it is transitive (since renement is) and distributes
through the CSP operators (since renement does), but it has a serious draw-
back: by increasing the degree of nondeterminism it is often the case that the
abstraction no longer fulls the required property, and the reason is not an im-
plementation error but the fact that too many relevant data-dependent decisions
in the implementation have been replaced by internal choice in the abstracted
process.
Abstraction Through Data Independence.
What is needed, is a more subtle ab-
straction method allowing us to reduce the channel alphabets and the data range
of local process variables if these do not contribute to communication decisions
Search WWH ::
Custom Search