udy in Component-Based Mechanical Verication
of Fault-Tolerant Programs
�
Sandeep S. Kulkarni
John Rushby
Natarajan Shankar
Department of Computer and
Computer Science Laboratory
Information Science
SRI International
The Ohio State University
Menlo Park CA 94025
Columbus Ohio 43210 USA
USA
Abstract
In this paper, we present a case study to demonstrate
that the decomposition of a fault-tolerant program into its
components is useful in its mechanical verication. More
specically, we discuss our experience in using the theo-
rem prover PVS to verify Dijkstras token ring program in a
component-based manner. We also demonstrate the advan-
tages of component based mechanical verication.
Keywords :
Component-based verication,
Fault-
tolerance, Program decomposition, Mechanical verica-
tion, Self-stabilization
1
Introduction
In this paper, we argue that the decomposition of a fault-
tolerant program into its components is benecial in its me-
chanical verication, and that such a decomposition admits
reuse of the proofs for other fault-tolerant programs as well
as the variations of the given fault-tolerant program.
Arora and Kulkarni [3] have shown that a fault-tolerant
program can be decomposed into a fault-intolerant program
and a set of tolerance-components, namely detectors and
correctors. Intuitively, a detector is a component that de-
tects whether a given predicate is true in the program state,
and it is used for ensuring that the program satises its safety
specication in the presence of faults. Likewise, a corrector
is a component that corrects the system to a state where
the given state predicate is true, and it is used for ensuring
that the program eventually recovers to a state from where
its specication is satised.
For example, a fail-safe program, which satises only its
safety specication in the presence of faults, can be decom-
posed into a fault-intolerant program and detector(s). Like-
wise, a self-stabilizing program, which guarantees recovery
1
Email:
kulkarni@cis.ohio-state.edu,
rushby@csl.sri.com,
shankar@csl.sri.com
Web:
http://www.cis.ohio-state.
edu/kulkarni
,
http://www.csl.sri.com/rushby
,
http://www.csl.sri.com/shankar
This work was partially supported by National Science Foundation grant
CCR-9509931 and by the Air Force Ofce of Scientic Research, Air Force
Materiel Command, USAF, under contract F49620-95-C0044.
The views and conclusions contained herein are those of the authors and
should not be interpreted as necessarily representing the ofcial policies
or endorsements, either expressed or implied, of the Air Force Ofce of
Scientic Research or the U.S. Government.
to a state from where its specication is satised, can be de-
composed into a fault-intolerant program and corrector(s).
Decomposition of a fault-tolerant program permits the
verication of a given property by focusing on the compo-
nent that is responsible for satisfying it. For example, if we
need to show that a program eventually recovers to a state
from where it satises its specication, we should focus on
its corrector components. Likewise, if we are interested in
showing that the program satises its specication in the ab-
sence of faults, we should focus on the corresponding fault-
intolerant program. Of course, we will have to show that
other components of the program do not interfere with the
component of interest. But this proof is typically simpler
than the proof required to show that the overall program
satises the given property. Moreover, if we change some
components used in that program, the proofs of other com-
ponents are not affected. Thus, it is possible for a small
change in the program to lead to a small change in the proof.
With the motivation of developing a systematic approach
for mechanical verication using program decomposition,
we are implementing the theory of detectors and correc-
tors into the theorem prover PVS [11]
2
. In this paper, we
present a proof of one of Dijkstras token ring program [5]
that has been proved using this theory. Previously, Qadeer
and Shankar [13] have veried this token ring program using
PVS. While their proof is impressive, it is very specic to
one program and, hence, much of their proof-technique can-
not be reused to prove other fault-tolerant programs. More-
over, since they focus on the entire program, instead of its
components, their proof is more complex than it needs to be.
We use this case-study to illustrate how the decomposition
of the program into its components can help in making the
proofs simple and reusable.
Being self-stabilizing, Dijkstras program can be decom-
posed into a fault-intolerant program and a corrector. The
fault-intolerant program circulates the token along an ini-
tialized ring in the absence of faults. On the other hand, if
faults perturb the program from its ideal states, the correc-
tor restores the fault-intolerant program back to some ideal
state, from where it continues to circulate the token. This
program is self-stabilizing in that even if the faults perturb
the program to an arbitrary state, the corrector restores it to
2
The URL
http://www.cis.ohio-state.edu/kulkarni/
pvs/
contains the PVS specication and proofs. an ideal state.
In Dijkstras token ring program, processes
�
�
,
�
�
,
are organized in a ring. Each process
maintains a counter
�
,
�
�
�
for some
�
�
. A non-zero process
has a token iff
�
differs from
�
�
�
��
, and process
�
has
a token iff
�
�
is the same as
�
�
. If process
has a token
then it passes it to process
�
�
��
�
�
�
by setting
�
to
�
�
�
��
, and if process
�
has a token then it passes it
to process
�
by incrementing
�
�
. For any
�
,
�
�
, the
program guarantees that in the absence of faults there will
be exactly one token that is being circulated in the ring. If
�
�
�
�
, the program guarantees that starting from any
arbitrary state, the program will reach a state where there is
exactly one token which is circulated along the ring.
To decompose Dijkstras program into a fault-intolerant
program and a corrector, we rst consider the following
question: If we are only interested in a token circulation
along an initialized ring, how can the token ring program
be simplied? The answer to this question identies the
fault-intolerant program. Next we ask the question about
fault-tolerance: what are the ideal states of the resulting
fault-intolerant program, and how can it be recovered to
these ideal states if the faults perturb it? The answer to this
question identies the corrector. Then, we show how the
fault-intolerant program and the corrector can be indepen-
dently veried in PVS and how they can be shown to be
interference-free.
The rest of the paper is organized as follows: In Section
2, we present Dijkstras token ring program and its decom-
position into a fault-intolerant program and a corrector. In
Section 3, we show how the token ring program is mod-
eled in PVS. In Section 4 and 5, we present the correctness
proof for the fault-intolerant program and the corrector re-
spectively. In Section 6, we show that the corrector and the
fault-intolerant program do not interfere with each other. Fi-
nally, in Section 7, we discuss the advantages of component-
based verication over non-component-based verication,
and present concluding remarks in Section 8.
2
The Token Ring Program and its
Decomposition
In this section, we rst present the decomposition of
Dijkstras token ring program into a fault-intolerant program
and a corrector. Then, we argue that they work in isolation
and that they do not interfere with each other. We use the
same arguments for mechanical verication in Sections 4, 5
and 6.
Fault-intolerant program.
If we are not interested in
fault-tolerance, a token ring program can be designed by
maintaining a variable
�
(in the range 0..(M-1), where
�
�
) as follows: Each non-zero process
checks
whether
�
is different from
�
�
�
��
. If this condition
is true then
�
is set to
�
�
�
��
. Process
�
checks whether
�
�
is the same as
�
�
. If this condition is true, process
�
increments
�
�
. Thus, the actions of the fault-intolerant
program are as follows:
�
�
�
�
�
��
�
�
�
�
�
��
�
�
�
�
�
�
�
�
�
�
�
The invariant of this program is
�
, where
�
(
�
�
�
�
�
�
(
�
�
�
�
�
�
�
�
�
�
��
�
))
The invariant
�
characterizes the states where there exists
a process
such that the
�
values of processes
�
�
�
��
are
equal to
�
, and the
�
values of processes
�
are equal to
�
�
�
��
�
. Thus, process
has the unique token, and
only the action at
is enabled in that state. The execution of
this action results in a state where process
�
�
��
�
�
�
has the token. Thus, starting from a state where
�
is true,
the fault-intolerant program circulates a unique token along
the ring.
Corrector.
If the faults perturb the
�
values maintained
at the processes, we need to recover the program to a state
where
�
holds in order to ensure that the token circulation
is re-established. This can be achieved by the corrector that
lets each non-zero process copy the
�
value of its predeces-
sor. Thus, the actions of the corrector are as follows:
�
�
�
�
�
��
�
�
�
�
�
��
Observe that if the corrector actions execute in isolation,
a state is reached where all
�
values are same, and at that
state
�
is true. Also, if the corrector executes in any state
where
�
is true,
�
continues to be true in the resulting state.
Note that although the actions of the fault-tolerant pro-
gram and that of the fault-intolerant program are the same,
when dealing with the fault-intolerant program we can as-
sume that the invariant
�
is true. In this sense, the fault-
intolerant program is simpler than the fault-tolerant pro-
gram. Of course, the actions of the corr