A case study in model checking software systems

AbstractModel checking is a proven successful technology for verifying hardware. It works, however, on only finite state machines, and most software systems have infinitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, θ, to be verified. We check θ on an abstracted, but finite, model of S.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 s to check over 43600 reachable states