NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Investigation, Development, and Evaluation of Performance Proving for Fault-tolerant ComputersA number of methodologies for verifying systems and computer based tools that assist users in verifying their systems were developed. These tools were applied to verify in part the SIFT ultrareliable aircraft computer. Topics covered included: STP theorem prover; design verification of SIFT; high level language code verification; assembly language level verification; numerical algorithm verification; verification of flight control programs; and verification of hardware logic.
Document ID
19840017239
Acquisition Source
Legacy CDMS
Document Type
Other - Collected Works
Authors
Levitt, K. N. (SRI International Corp. Menlo Park, CA, United States)
Schwartz, R. (SRI International Corp. Menlo Park, CA, United States)
Hare, D. (SRI International Corp. Menlo Park, CA, United States)
Moore, J. S. (SRI International Corp. Menlo Park, CA, United States)
Melliar-Smith, P. M. (SRI International Corp. Menlo Park, CA, United States)
Shostak, R. E. (SRI International Corp. Menlo Park, CA, United States)
Boyer, R. S. (SRI International Corp. Menlo Park, CA, United States)
Green, M. W. (SRI International Corp. Menlo Park, CA, United States)
Elliott, W. D. (SRI International Corp. Menlo Park, CA, United States)
Date Acquired
September 4, 2013
Publication Date
August 1, 1983
Subject Category
Computer Operations And Hardware
Report/Patent Number
NASA-CR-166008
NAS 1.26:166008
Report Number: NASA-CR-166008
Report Number: NAS 1.26:166008
Accession Number
84N25307
Funding Number(s)
CONTRACT_GRANT: NAS1-15528
PROJECT: SRI PROJ. 7821
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

IDRelationTitle19840017240WorkSTP: A Mechanized Logic for Specification and Verification19840017241WorkSpecifying and Verifying Ultra-reliability and Fault-tolerance Properties19840017242WorkThe Hierarchical Specification and Mechanical Verification of the SIFT Design19840017243WorkOverview of Code Verification19840017244WorkA Summary of HDM19840017245WorkAutomatic Construction of Verification Generators from Hoare Logics19840017246WorkThe PASCAL-HDM Verification System19840017247WorkHDM/PASCAL Verification System User's Manual19840017248WorkThe SIFT Code Specification19840017249WorkThe Proof of the SIFT Implementation19840017250WorkA Formal Semantics for the SRI Hierarchical Program Design Methodology19840017251WorkOn Why It Is Impossible to Prove that the BDX90 Dispatcher Implements a Time-sharing System19840017252WorkDefining of the BDX930 Assembly Language19840017253WorkVerification of Numerical Algorithms19840017254WorkThe use of a formal simulator to verify a simple real time control program19840017255WorkHierarchical Design and Verification for VLSI19840017256WorkThree Lectures on Theorem-proving and Program Verification19840017240WorkSTP: A Mechanized Logic for Specification and Verification19840017241WorkSpecifying and Verifying Ultra-reliability and Fault-tolerance Properties19840017242WorkThe Hierarchical Specification and Mechanical Verification of the SIFT Design19840017243WorkOverview of Code Verification19840017244WorkA Summary of HDM19840017245WorkAutomatic Construction of Verification Generators from Hoare Logics19840017246WorkThe PASCAL-HDM Verification System19840017247WorkHDM/PASCAL Verification System User's Manual19840017248WorkThe SIFT Code Specification19840017249WorkThe Proof of the SIFT Implementation19840017250WorkA Formal Semantics for the SRI Hierarchical Program Design Methodology19840017251WorkOn Why It Is Impossible to Prove that the BDX90 Dispatcher Implements a Time-sharing System19840017252WorkDefining of the BDX930 Assembly Language19840017253WorkVerification of Numerical Algorithms19840017254WorkThe use of a formal simulator to verify a simple real time control program19840017255WorkHierarchical Design and Verification for VLSI19840017256WorkThree Lectures on Theorem-proving and Program Verification
No Preview Available