Formal Verification for Fault-Tolerant
Architectures: Prolegomena to the Design of PVS
Sam Owre, John Rushby, Natarajan Shankar and Friedrich von Henke
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.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
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/}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page