Computer-Aided Verification
Many of the algorithm and system correctness proofs that have been
produced by the TDS Group
have been partially automated. Most of this work uses
theorem-proving, primarily using the Larch
Prover; some current work also involves model-checking. Among the
projects are:
-
The development of a
programming language
for I/O automata
which allows simple abstract descriptions of distributed systems,
in order to aid in system development, testing, and verification.
-
Jensen and
Vaziri
have been examining and developing techniques for the integration of
model-checking and theorem-proving methods for the
verification of concurrent systems.
Specifically, they have been studying the feasibility
of abstracting from an infinite state system
to a finite state system.
They have developed a property-preserving abstraction theorem
for the I/O automaton framework,
and are currently examining uses of this theorem
in the verification of concurrent read/write
and mutual exclusion algorithms.
- The development, by Jensen, of a verification
strategy in the Input/Output Automaton framework, that combines theorem
proving and model checking methods by the use of abstraction techniques.
General theorems stating conditions for property-preservation have been
developed and used in the verification of safety properties for important
distributed algorithms.
-
A verification, by Sogaard-Andersen, Garland,
Guttag,
Lynch, and Pogosyants,
of the equivalence of two specifications of fault-tolerant
at-most-once message communication services.
Both specifications are formalized as I/O automata.
One direction of the equivalence involves a forward simulation, and
the other a backward simulation.
Both directions are completely verified using the Larch Prover.
This work was presented at CAV93.
-
A S.M. thesis
by Mandana
Vaziri on the verification of protocols for Redundant Arrays of
Inexpensive Disk (RAID) systems.
-
A M. Eng. thesis by Ekrem Soylemez [4], giving a complete verification,
using the Larch Prover, of a time bound for a simple counter system.
The proof is based on a forward simulation.
This is interesting because the theorem-proving techniques are used to
prove a timing property.
The methods used are based on those presented by Lynch and Attiya in
JACM.
-
A M.S. thesis by Victor Luchangco, continuing the work by Soylemez
by using forward simulations to analyze some more complex algorithms.
These algorithms include the Fischer timing-based mutual exclusion
algorithm and the LeLann-Chang-Roberts leader election protocol.
The proof of the Fischer algorithm, including both the mutual
exclusion and time bound properties, has been automated using the
Larch Prover. Also, see FORTE94
paper.
-
A partial verification, using PVS, of the Generalized Railroad
Crossing implementation described by Heitmeyer and
Lynch.
This partial verification was carried out by Archer.
-
A partial verification, using Larch Prover, of the Randomized Digning
Philosophers Algorithm. This work is presented in a
paper PODC95
by Pogosyants and Segala.
-
A formal representation and machine-checked proof using the Larch Prover
for the Bounded Concurrent Timestamp (BCTS) algorithm of Dolev and
Shavit [1]. It is modified in Gawlick's M.S. thesis [2],
Gawlick-Lynch-Shavit [3] to take advantage of the power of atomic
snapshot shared memory.
This work was presented in a
FORTE96
by Petrov, Pogosyants, Garland, Luchangco, and Lynch.
[1] Danny Dolev and Nir Shavit. Bounded Concurrent Time-stamp Systems
are Constructible. In Proceedings of the Twenty-first Annual ACM
Symposium on Theory of Computing, pages 454--466, Seattle, Washington,
May 1989. To appear in SIAM Journal on Computing.
[2] Rainer Gawlick. Bounded Concurrent Time-stamping Made Simple.
Master's thesis, Department of Electrical Engineering and Computer
Science, Massachusetts Institute of Technology, June 1992.
[3] Rainer Gawlick, Nancy Lynch, and Nir Shavit. Councurrent
Time-stamping Made Simple. Full version submitted for
journal publication. Earlier version appears in Proceedings of the
First Israel Symposium on the Theory of Computing and Systems,
Springer-Verlag, pages 171-185, May 1992.
[4] Ekrem Soylemez. Automatic verification of the timing properties of
MMT automata. Master's thesis, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of
Technology, Cambridge, MA 02139, February 1994.
