A Case Study in Model Checking Software Systems
Authors:Jeannette M. Wing and Mandan Vaziri-Farahani
Click here for the
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 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.