Loading...
Please wait, while we are loading the content...
Similar Documents
Towards the formal verification of the requirements and design of a processor interface unit
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Cohen, Gerald C. Fura, David A. Windley, Phillip J. |
| Copyright Year | 1993 |
| Description | The formal verification of the design and partial requirements for a Processor Interface Unit (PIU) using the Higher Order Logic (HOL) theorem-proving system is described. The processor interface unit is a single-chip subsystem within a fault-tolerant embedded system under development within the Boeing Defense and Space Group. It provides the opportunity to investigate the specification and verification of a real-world subsystem within a commercially-developed fault-tolerant computer. An overview of the PIU verification effort is given. The actual HOL listing from the verification effort are documented in a companion NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit - HOL Listings' including the general-purpose HOL theories and definitions that support the PIU verification as well as tactics used in the proofs. |
| File Size | 3175994 |
| Page Count | 64 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19940019602 |
| Archival Resource Key | ark:/13960/t3xt0mz27 |
| Language | English |
| Publisher Date | 1993-12-01 |
| Access Restriction | Open |
| Subject Keyword | Fault Tolerance Specifications Microprocessors Theorem Proving Software Reliability Formalism Program Verification Computers Computer Programs Ntrs Nasa Technical Reports ServerĀ (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |