NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Verification of the FtCayuga fault-tolerant microprocessor system. Volume 1: A case study in theorem prover-based verificationThe 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.
Document ID
19910020464
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Srivas, Mandayam (ORA Corp. Ithaca, NY, United States)
Bickford, Mark (ORA Corp. Ithaca, NY, United States)
Date Acquired
September 6, 2013
Publication Date
July 1, 1991
Subject Category
Computer Systems
Report/Patent Number
NAS 1.26:4381
NASA-CR-4381
Accession Number
91N29778
Funding Number(s)
CONTRACT_GRANT: NAS1-18972
PROJECT: RTOP 505-64-10-05
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available