Model Checking Software Systems: A Case Study.

Model 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, phi to be verifIed. We check phi 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 clients 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 McMillans SMV model checker on our most complicated protocol, SMV took less than 1 second to check over 43,600 reachable states.