Appears in Proceedings of 3rd ACM SIGSOFT Symposium on the Foundations of Software Engineering, October 1995.
The full text of this paper is here (in PostScript).
Following this approach we verified three cache coherence protocols used in distributed file systems. These protocols have to satisfy this property: ``If a client believes that a cached file is valid then the authorized server believes that the client's copy is valid.'' In our finite model of the system, we need only represent the ``beliefs'' that a client and a server have about a cached file; we can abstract from the caches, the files' contents, and even the files themselves. Moreover, by successive application of the generalization rule from predicate logic, we need only consider a model with at most two clients, one server, and one file. We used McMillan's SMV model checker; on our most complicated protocol, SMV took less than 1 second to check over 43,600 reachable states.