Information Technology Reference
In-Depth Information
failures-divergence renement relation is well-dened between CSP processes and
FTC OCCAM processes as well. Next observe the following facts:
{
Deadlock freedom is preserved under failures renement.
{
If
Q
is free of livelocks and
Q
0
is livelock-free and a trace
renement of
Q
,then
Q
0
nf
nf
c
1
;
c
2
;:::;
c
n
g
is free of livelocks, too
3
.
c
1
;
c
2
;:::;
c
n
g
{
If
Q
=(
Q
1
k::: k
Q
k
) species the Byzantine agreement protocol between
and
Q
0
=(
Q
1
k::: k
Q
k
processes
Q
i
) is free of deadlocks and livelocks and
the
Q
i
are trace renements of the
Q
i
,then
Q
0
is a correct implementation
of the protocol as well
4
.
These considerations motivate the following global verication strategy:
{
To establish deadlock freedom, nd an abstract deadlock-free CSP process
system which is rened in the failures model by the OCCAM process system
consisting of the FML and AVI running in parallel.
{
To establish livelock freedom, nd an abstract CSP process
Q
with the same
interface channels
as
the OCCAM system
P
consisting of the AVI running in parallel with the
FML and prove that (1)
Q
f
d
1
;
d
2
;:::;
d
`
g
and internal channels
f
c
1
;
c
2
;:::;
c
n
g
nf
c
1
;
c
2
;:::;
c
n
g
is free of livelocks and (2)
Q
is
rened by
P
in the trace model.
{
To prove correct implementation of the Byzantine protocol, specify the pro-
tocol as a CSP process
BYZAN
(this is a direct transcription of the semi-
formal protocol specication given in Lamport [13]), use the fact that the
FML has been shown to be free of deadlocks and livelocks and prove that
the FML is a trace renement of
BYZAN
.
3.2
Abstraction Methods
Purpose and Denition of Abstractions.
Abstraction methods were applied in
two situations:
{
To transform OCCAM code into CSP, so that formal analysis of correctness
properties could be performed on the level of a formal specication language
instead on programming language level,
{
To transform CSP specications into simpler ones which were still su-
ciently detailed to verify the correctness property under investigation, but
small enough to be analysed by model checking without running into state
explosion problems.
For our purposes, the abstraction principle can be formally dened as follows:
3
Livelock freedom for
Q
0
must be stipulated in order to exclude pathological diver-
gence cases such as
Q
0
=
Q
0
u Q
.
4
To prove this, one has to observe that the communication decisions of the proto-
col are deterministic for the correctly functioning communication partners, and the
communications are completely determined by the number
k
of processes and the
message contents communicated along the channels.
Search WWH ::
Custom Search