SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Specification, Proof Checking, and Model Checking for Protocols and Distributed Systems with PVS
 by Dr. John Rushby.

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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy