NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Interpreter composition issues in the formal verification of a processor-memory moduleThis report describes interpreter composition techniques suitable for the formal specification and verification of a processor-memory module using the HOL theorem proving system. The processor-memory module is a multichip subsystem within a fault-tolerant embedded system under development within the Boeing Defense and Space Group. Modeling and verification methods were developed that permit provably secure composition at the transaction-level of specification, significantly reducing the complexity of the hierarchical verification of the system.
Document ID
19940028269
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Fura, David A. (Boeing Co. Seattle, WA, United States)
Cohen, Gerald C. (Boeing Co. Seattle, WA, United States)
Date Acquired
September 6, 2013
Publication Date
May 1, 1994
Publication Information
Publisher: NASA
Subject Category
Computer Programming And Software
Report/Patent Number
NAS 1.26:4594
NASA-CR-4594
Accession Number
94N32775
Funding Number(s)
PROJECT: RTOP 505-64-50-04
CONTRACT_GRANT: NAS1-18586
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