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

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.

@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/}
}

• wift95.pdf
• wift95.ps.gz