CMU-CS-98-117 Computer Science Department School of Computer Science, Carnegie Mellon University
Proving Correctness of a Controller Algorithms 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
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
| |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |