Proving Correctness of a Controller Algorithm for the RAID Level 5 System

Most RAID controllers implemented in industry are complicated and di cult to reason about. This complexity 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 prototyping system. As a rst step towards building such a tool, our approach consists of studying several controller algorithms manually, to determine the key properties that need to be veri ed. This paper presents the modeling and veri cation of a contro...

• Type: Conference
• Year: 1998
• Where: FTCS
• Authors: Mandana Vaziri, Nancy A. Lynch, Jeannette M. Wing
• Keywords: Controller Algorithm, Di Cult, FTCS 1998, Generic Controller Algorithm