Information Technology Reference
In-Depth Information
and { in case of the Byzantine protocol verication { do not represent relevant
protocol data.
Example 1. Suppose that channels c
;
d range over the natural numbers. We wish
to prove that process system
SYSTEM =( P k
fjcjg
Q )
P = c !0
!
STOP
u
c !1
!
STOP
Q = c ? x
!
( if ( x
<
10) then ( d !0
!
STOP ) else ( d !10
!
STOP ))
always produces event d
:
0. Formally, this property p can be expressed as
( d
v T denoting the trace renement rela-
tion. Since the condition in Q only depends on the two situations x
:
0
!
STOP )
v T
SYSTEM
nfj
c
jg
,
<
10 and
x
10, it suces to analyse the abstracted process system
SYSTEM 0 =( P 0 k
fjc 0 jg
Q 0 )
P 0 = c 0 !0
!
STOP
Q 0 = c 0 ? x
( if ( x == 0) then ( d 0 !0
STOP ) else ( d 0 !10
!
!
!
STOP ))
where channels c 0 ;
d 0 are dened with the nite alphabet
f
;
g
0
10
instead of the
A ( p ) now diers from the original p :
innite set N . The abstracted property
A ( p ) would be dened as ( d 0 :
SYSTEM 0 nfj
c 0 jg
0
!
STOP )
v T
, referring to
abstracted channels c 0 ;
d 0 .
t
This type of abstraction is called abstraction through data independence and has
been formally investigated by Lazic and Roscoe [16,24]. It is much more powerful
with respect to the construction of valid abstractions with considerably reduced
state spaces. For our verication suite, abstraction through data independence
was used to extend the verication strategy by further simplifying the CSP
processes constructed before according to the abstraction through renement
principle (details can be found in Buth et.al. [5,6] and Peleska et.al. [27]).
{ For the verication of deadlock and livelock freedom, the channels c used by
OCCAM processes and on the rst CSP abstraction level were abstracted to
single-event channels c 0 if the data communicated along c did not influence
communication decisions. If the data communicated along c could lead to
n dierent communication decisions, the set
f
;:::;
g
1
n
was used for the
alphabet of c 0 .
{ For the Byzantine protocol verication, it could be shown that the range of
data to be passed along the protocol channels for comparison in the voting
procedure could be reduced to a set of 7 elements.
3.3
Compositional Reasoning and Use of Generic Theories
Even after the application of the abstraction methods described above, it would
have been infeasible to verify the correctness properties in one step simply by
 
Search WWH ::




Custom Search