Computer Science Department
School of Computer Science, Carnegie Mellon University
Proving Correctness of a Controller Algorithms
Mandana Vaziri*, Nancy Lynch*, Jeannette M. Wing
This paper will appear in the Proceedings of the International Symposium on Fault-Tolerant Computing, 1998.
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