CMU-CS-98-117
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-98-117

Proving Correctness of a Controller Algorithms
for the Raid Level 5 System

Mandana Vaziri*, Nancy Lynch*, Jeannette M. Wing

March 1998

This paper will appear in the Proceedings of the International Symposium on Fault-Tolerant Computing, 1998.

CMU-CS-98-117.ps
CMU-CS-98-117Cover.ps

Most RAID controllers implemented in industry are complicated and difficult to reason about. This complexity has led to software and hardware systems that are difficult to debug and hard to modify. To overcome this problem Courtright and Gibson have developed a rapid prototyping framework for RAID architectures which relies on a generic controller algorithm. The designer of a new architecture needs to specify parts of the generic controller algorithm and must justify the validity of the controller algorithm obtained. However the latter task may be difficult due to the concurrency of operations on the disks. This is the reason why it would be useful to provide designers with an automated verification tool tailored specifically for the RAID prototyping system.

As a first step towards building such a tool, our approach consists of studying several controller algorithms manually, to determine the key properties that need to be verified.

This paper presents the modeling and verification of a controller algorithm for the RAID Level 5 System. We model the system using I/O automata, give an external requirements specification, and prove that the model implements its specification. We use a key invariant to find an error in a controller algorithm for the RAID Level 6 System.

Keywords: Formal methods, RAID systems, formal specification, verification, correctness proofs, I/O automata


14 pages

*Laboratory for Computer Science, MIT, 545 Technology Square, Cambridge, MA 02139

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu