Information Technology Reference
In-Depth Information
However, a simpler to write computational invariant is the following:
8i: CS
[
i
]=
)v
=
i
^8i; j:
(
B
[
i
]
^ CS
[
j
]) =
) x
[
i
]
1
^8i; j:
(
B
[
i
]
^ C
[
j
]) =
)
(
x
[
i
]
1
_ v 6
=
j _ x
[
i
]
x
[
j
])
Finding a Network Invariant
The interface between components concerns the
global variable
, the timing, and whether or not a component is in the critical
section. We can therefore nd a network invariant as a system with four states,
shown in Figure 2. The gure shows an abstraction of a network containing
v
v62 J
fg
true
true
fxg
x<
1
fxg
x>
1
fg
1
2
3
4
v
=0
v2J
fg
true
v
:= 0
Fig. 2.
Network Invariant for Fischer's Protocol. Not shown in the graph is a
self-loop at state 2, which sets
v
to an arbitrary index in
J
indices in a set
of indices. Here, the four states are abstractions of network
states with the following properties. We use
J
idle
[
i
] to denote the property
A
[
i
]
_
(
B
[
i
]
^ x
[
i
]
1)
_
(
C
[
i
]
^ v 6
=
i
) denoting processes that are not active in
competing for the critical section.
1:
8i: idle
[
i
]
2:
(
8i: idle
[
i
]
_ B
[
i
]
_
(
C
[
i
]
^ x
[
i
]
<
1))
^
(
8i; j:
(
B
[
i
]
^ C
[
j
]) =
) x
[
i
]
x
[
j
])
3:
8i: idle
[
i
]
_ C
[
i
]
4:
8i: idle
[
i
]
_ C
[
i
]
_
(
CS
[
i
])
^ v
=
i
)
Not shown in the graph is a self-loop at state 2, which sets
v
to an index in
J
.
6
Conclusion
In this paper, we have considered methods for verifying parameterized systems
using induction. We have considered the use of computational induction, and
of induction over the network structure. The main contribution has been to
give conditions under which there are guarantees for the existence of inductive
invariants of a simple form. For the case of computational induction, we have
Search WWH ::
Custom Search