Loading...
Please wait, while we are loading the content...
Similar Documents
Verification of the ftcayuga fault-tolerant microprocessor system. volume 1: a case study in theorem prover-based verification
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Srivas, Mandayam Bickford, Mark |
| Copyright Year | 1991 |
| Description | The design and formal verification of a hardware system for a task that is an important component of a fault tolerant computer architecture for flight control systems is presented. The hardware system implements an algorithm for obtaining interactive consistancy (byzantine agreement) among four microprocessors as a special instruction on the processors. The property verified insures that an execution of the special instruction by the processors correctly accomplishes interactive consistency, provided certain preconditions hold. An assumption is made that the processors execute synchronously. For verification, the authors used a computer aided design hardware design verification tool, Spectool, and the theorem prover, Clio. A major contribution of the work is the demonstration of a significant fault tolerant hardware design that is mechanically verified by a theorem prover. |
| File Size | 2984761 |
| Page Count | 66 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19910020464 |
| Archival Resource Key | ark:/13960/t9x110x7v |
| Language | English |
| Publisher Date | 1991-07-01 |
| Access Restriction | Open |
| Subject Keyword | Fault Tolerance Theorems Algorithms Microprocessors Consistency Proving Synchronism Architecture Computers Flight Control Computer Aided Design Program Verification Computers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |
