Accession Number : ADA309147
Title : A Case Study in Model Checking Software Systems.
Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Wing, Jeanette M. ; Vaziri-Farahani, Mandana
PDF Url : ADA309147
Report Date : APR 1996
Pagination or Media Count : 36
Abstract : 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.
Descriptors : *CASE STUDIES, *COMPUTER PROGRAM VERIFICATION, MODELS, MATHEMATICAL LOGIC, COHERENCE, THEOREMS.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE