SRI International Computer Science Laboratory
Specification, Proof Checking, and Model Checking for
Protocols and Distributed Systems with PVS
John Rushby
Tutorial Notes for FORTE/PSTV '97, Osaka, Japan, November 1997
Abstract
This tutorial uses a simple example to demonstrate
some of the techniques and issues in the formal specification and
analysis of protocols. A simple cache-coherence protocol is formally
specified as a transition relation in PVS and a desired property of
the protocol is proposed. The specification is then ``downscaled'' to
create a finite-state instance with just two caches, and the property
is examined using model checking. An attempt is then made to
establish the property for the full protocol using theorem proving,
but it is discovered that the property is not inductive. A
strengthened invariant is then proposed, checked by model checking in
the downscaled instance, and then established by theorem proving.
Finally, an alternative approach is illustrated in which theorem
proving is used to justify a property-preserving abstraction to finite
state, which is then analyzed by model checking.
The tutorial is not intended as an introduction to PVS, but as an
illustration of some topics in its application to protocols and as an
introduction to the use of theorem proving and model checking
techniques in combination.
This tutorial was developed in PVS version 2.2. In version 2.3 the
model checking theories have been incorporated into the prelude, and the
proofs of cache_array.invariant and refinement.next_simulation needed
adjustment because of other changes. Make sure you get the dump file
corresponding to the system you are using.
dvi or
postscript;
slides and
4-up slides (both
gzipped postscript)
PVS 2.3 dump file
PVS 2.2 dump file
Return to the Computer Science Laboratory home page