SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods
 by Steven P. Miller and Mandayam Srivas.

From WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques.
ieeecs, Boca Raton, FL.
April, 1995.
Pages 2–16.


Abstract
This paper describes the experiences of Collins Commercial Avionics and SRI International in formally specifying and verifying the microcode for the AAMP5 microprocessor with the PVS verification system. The 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 on an example of this size and the implications for using formal methods in an industrial setting.
BibTEX Entry
@inproceedings{Miller&Srivas95,
    AUTHOR = {Steven {P.} Miller and Mandayam Srivas},
    TITLE = {Formal Verification of the {AAMP5} Microprocessor: {A} Case Study in the Industrial Use of Formal Methods},
    BOOKTITLE = {{WIFT} '95: Workshop on Industrial-Strength Formal Specification Techniques},
    YEAR = {1995},
    PAGES = {2--16},
    ADDRESS = {Boca Raton, {FL}},
    MONTH = {April},
    ORGANIZATION = {ieeecs},
    URL = {http://www.csl.sri.com/papers/wift95/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy