NASA Logo

NTRS

NTRS - NASA Technical Reports Server

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
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
Funding Number(s)
CONTRACT_GRANT: NAS1-15528
PROJECT: SRI PROJ. 7821
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Available Downloads

NameType 19840017239.pdf STI

Related Records

IDRelationTitle19840017240Analytic SubsidiarySTP: A Mechanized Logic for Specification and Verification19840017241Analytic SubsidiarySpecifying and Verifying Ultra-reliability and Fault-tolerance Properties19840017242Analytic SubsidiaryThe Hierarchical Specification and Mechanical Verification of the SIFT Design19840017243Analytic SubsidiaryOverview of Code Verification19840017244Analytic SubsidiaryA Summary of HDM19840017245Analytic SubsidiaryAutomatic Construction of Verification Generators from Hoare Logics19840017246Analytic SubsidiaryThe PASCAL-HDM Verification System19840017247Analytic SubsidiaryHDM/PASCAL Verification System User's Manual19840017248Analytic SubsidiaryThe SIFT Code Specification19840017249Analytic SubsidiaryThe Proof of the SIFT Implementation19840017250Analytic SubsidiaryA Formal Semantics for the SRI Hierarchical Program Design Methodology19840017251Analytic SubsidiaryOn Why It Is Impossible to Prove that the BDX90 Dispatcher Implements a Time-sharing System19840017252Analytic SubsidiaryDefining of the BDX930 Assembly Language19840017253Analytic SubsidiaryVerification of Numerical Algorithms19840017254Analytic SubsidiaryThe use of a formal simulator to verify a simple real time control program19840017255Analytic SubsidiaryHierarchical Design and Verification for VLSI19840017256Analytic SubsidiaryThree Lectures on Theorem-proving and Program Verification