NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal verification of an avionics microprocessorFormal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This report discusses a project undertaken to answer some of these questions, the formal verification of the AAMPS microprocessor. This project consisted of formally specifying in the PVS language a rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show that the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.
Document ID
19950026975
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Srivas, Mandayam, K.
(SRI International Corp. Menlo Park, CA, United States)
Miller, Steven P.
(Rockwell International Corp. Cedar Rapids, IA., United States)
Date Acquired
September 6, 2013
Publication Date
July 1, 1995
Subject Category
Computer Programming And Software
Report/Patent Number
NASA-CR-4682
ECU-8200-270
NAS 1.26:4682
Accession Number
95N33396
Funding Number(s)
PROJECT: RTOP 505-64-10-13
CONTRACT_GRANT: NAS1-18969
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available