Title :
Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods
Author :
Miller, Steven P. ; Srivas, Mandayam
Author_Institution :
Collins Commercial Avionics, Rockwell Int. Corp., Cedar Rapids, IA, USA
Abstract :
This paper describes the experiences of Collins Commercial Avionics and SRI International informally specifying and verifying the microcode for the AAMP5 microprocessor with the PVS verification system. This project was conducted to determine if an industrial microprocessor designed for use in real-time embedded systems could be formally specified at the instruction set and register transfer levels and if formal proofs could be used to prove the microcode correct. The paper provides a brief technical overview, but its emphasis is on the lessons learned in using PVS for an example of this size and the implications for using formal methods in an industrial setting
Keywords :
computer testing; firmware; formal verification; integrated circuit testing; microprocessor chips; real-time systems; AAMP5 microprocessor; PVS verification system; formal methods; formal proofs; formal verification; industrial microprocessor; instruction set level; microcode; real-time embedded systems; register transfer level; Aerospace electronics; Computer aided software engineering; Computer science; Error correction; Formal specifications; Formal verification; Hardware; Laboratories; Microprocessors; NASA;
Conference_Titel :
Industrial-Strength Formal Specification Techniques, 1995. Proceedings., Workshop on
Conference_Location :
Boca Raton, FL
Print_ISBN :
0-8186-7005-3
DOI :
10.1109/WIFT.1995.515475
