Paper Info
Title
Proving Correctness of a Controller Algorithm for the RAID Level 5 System
Abstract
Abstract Most RAID controllers implemented in industry are complicated and di cult to reason about. This com-plexity has led to software and hardware systems that are di cult 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 [1]. 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 di cult due to the concurrency of operations on the disks. This is the reason why it would be useful to provide designers with an automated veri cation tool tailored speci cally for the RAID pro-totyping system. As a rst step towards building such a tool, our approach consists of studying several controller algo-rithms manually, to determine the key properties that need to be veri ed. This paper presents the modeling and veri cation of a controller algorithm for the RAID Level 5 System [5]. We model the system using I/O automata [6], give an external requirements speci cation, and prove that the model implements its speci cation. We use a key invariant to nd an error in a controller algorithm for the RAID Level 6 System [5].
Year
DOI
Venue
1998
10.1109/FTCS.1998.689451
FTCS
Keywords
Field
DocType
controller algorithm,raid level,proving correctness,automata theory,requirements specification,software systems,prototypes,hardware,verification,automatic control,algorithms,requirements,computer architecture,automata,invariance,algorithm design and analysis,control
Control theory,Automata theory,Concurrency,Computer science,Correctness,Algorithm,Standard RAID levels,RAID,Software requirements specification,Embedded system,Debugging
Conference
ISSN
ISBN
Citations 
0731-3071
0-8186-8470-4
0
PageRank 
References 
Authors
0.34
2
3
Name
Order
Citations
PageRank
mandana vazirifarahani100.34
Nancy A. Lynch2101701838.61
Jeannette M. Wing36429874.60