Accession Number : ADA294845

Title :   Model Checking Software Systems: A Case Study.

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Wing, Jeannette M. ; Vaziri-Farahani, Mandana

PDF Url : ADA294845

Report Date : 10 MAR 1995

Pagination or Media Count : 26

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, COMPUTER PROGRAMS, SOFTWARE ENGINEERING, DISTRIBUTED DATA PROCESSING, MODELS, COHERENCE, COMPUTER FILES.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE