Accession Number : ADA296389

Title :   Model Checking Cache Coherence Protocols for Distributed File Systems.

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

Personal Author(s) : Vaziri-Farahani, Mandana

PDF Url : ADA296389

Report Date : 18 MAY 1995

Pagination or Media Count : 31

Abstract : Debugging complex software systems is a major problem. Proving properties of software systems can be thought of as a debugging tool. If a system S must satisfy property P but we can prove that it does not, then S has bugs in it. On the other hand, if S is proved to satisfy P then this is just a confirmation that a certain aspect of S is correct. We can prove properties of software systems at any stage of development. If we do these proofs early in the design stage, we can prevent errors from propagating to later development stages and therefore save time, money, and human effort. The traditional approach to proving properties of software systems is theorem proving. This approach has several pragmatic drawbacks. The size of the programs that we can prove correct is not very large. Theorem proving must be done by highly skilled experts in the field. Our approach to proving properties of software systems is model checking, which consists of proving the property by automatically checking every state in the system. Model checking is a technique successfully used in hardware verification. The model checking tool we use is SMV, which takes as input a finite state machine (FSM) and a property P expressed in Computation Tree Logic (CTL) and outputs true if the FSM satisfies P or false otherwise. If the outcome is false then SMV also outputs a counterexample. Because software systems are not, in general, finite state machines, model checking seems to be inadequate at first glance. However, we can overcome this problem by abstracting the system and checking a finite model of it. We use this method to check cache coherence protocols for distributed systems.

Descriptors :   *SYSTEMS APPROACH, *COMPUTER FILES, *COMPUTER PROGRAM VERIFICATION, *DEBUGGING(COMPUTERS), COMPUTER PROGRAMS, COMPUTATIONS, DISTRIBUTED DATA PROCESSING, MODELS, COHERENCE, TREES, ERROR ANALYSIS, MACHINES, LOGIC.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE