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

Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS
 by Sam Owre, Dr. John Rushby, Dr. Natarajan Shankar & Friedrich von Henke.

Appears in IEEE Transactions on Software Engineering, Volume 21, Number 2.
February, 1995.
Pages 107–125.


Abstract

PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanically checked verifications for the fault-tolerant architecture, algorithms, and implementations of a model ``reliable computing platform'' (RCP) for life-critical digital flight-control applications, and by a collaborative project to formally verify the design of a commercial avionics processor called AAMP5.

Several of the formal specifications and verifications performed in support of RCP and AAMP5 are individually of considerable complexity and difficulty. But in order to contribute to the overall goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to understand, review, build on, modify, or extract part of an intricate verification.

In this paper, we outline the verifications performed, present the lessons learned, and describe some of the design decisions taken in PVS to better support these large, difficult, iterative, and collaborative verifications.

BibTEX Entry
@article{Owre95:prolegomena,
    AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar and Friedrich von Henke},
    TITLE = {Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of {PVS}},
    JOURNAL = {{IEEE} Transactions on Software Engineering},
    VOLUME = {21},
    NUMBER = {2},
    YEAR = {1995},
    PAGES = {107--125},
    MONTH = {feb},
    URL = {http://www.csl.sri.com/papers/tse95/}
}
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