| タイトル | Towards the formal specification of the requirements and design of a processor interface unit |
| 本文（外部サイト） | http://hdl.handle.net/2060/19940019990 |
| 著者（英） | Fura, David A.; Windley, Phillip J.; Cohen, Gerald C. |
| 著者所属（英） | Boeing Defense and Space Group |
| 発行日 | 1993-12-01 |
| 言語 | eng |
| 内容記述 | Work to formally specify the requirements and design of a Processor Interface Unit (PIU), a single-chip subsystem providing memory interface, bus interface, and additional support services for a commercial microprocessor within a fault-tolerant computer system, is described. This system, the Fault-Tolerant Embedded Processor (FTEP), is targeted towards applications in avionics and space requiring extremely high levels of mission reliability, extended maintenance free operation, or both. The approaches that were developed for modeling the PIU requirements and for composition of the PIU subcomponents at high levels of abstraction are described. These approaches were used to specify and verify a nontrivial subset of the PIU behavior. The PIU specification in Higher Order Logic (HOL) is documented in a companion NASA contractor report entitled 'Towards the Formal Specification of the Requirements and Design of a Processor Interfacs Unit - HOL Listings.' The subsequent verification approach and HOL listings are documented in NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit' and NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit - HOL Listings.' |
| NASA分類 | COMPUTER SYSTEMS |
| レポートNO | 94N24463
NASA-CR-4521
NAS 1.26:4521 |
| 権利 | No Copyright |
|
