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.

• cache-pvs2.2.dmp
• cache-pvs2.3.dmp
• forte97.dvi
• forte97.ps
• slides-4up.ps
• slides.ps