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


Related Tutorials and Papers


Return to the Formal Methods Program home page

Return to the Computer Science Laboratory home page