Model Checking Cache Coherence Protocols for Distributed File Systems

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 conf...

Full description

Saved in:
Bibliographic Details
Main Author: Vaziri-Farahani, Mandana
Format: Report
Language:English
Subjects:
COHERENCE
COMPUTATIONS
COMPUTER PROGRAM VERIFICATION
Computer Programming and Software
COMPUTER PROGRAMS
CTL(COMPUTATIONAL TREE LOGIC)
DEBUGGING(COMPUTERS)
DISTRIBUTED DATA PROCESSING
ERROR ANALYSIS
FSM(FINITE STATE MACHINE)
LOGIC
MACHINES
MODEL CHECKING
SYSTEMS APPROACH
TREES
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.