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

Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned
 by Sam Owre, Dr. John Rushby, Dr. Natarajan Shankar & Friedrich von Henke.

Note: a much revised version of this paper appears under the title Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS in IEEE Transactions on Software Engineering, February 1995.

Appears in FME '93: Industrial-Strength Formal Methods, Lecture Notes in Computer Science, Volume 670.
Edited by J. C. P. Woodcock and P. G. Larsen.
Springer-Verlag, Odense, Denmark.
April, 1993.
Pages 482–500.


Abstract

In collaboration with NASA's Langley Research Center, we are developing mechanically verified formal specifications for the fault-tolerant architecture, algorithms, and implementations of a ``reliable computing platform'' (RCP) for life-critical digital flight-control applications. To achieve a failure rate that is certifiably less than 10^-9 per hour, RCP employs redundant, synchronized computing channels for fault masking and transient recovery. The synchronization and sensor-distribution algorithms are resilient with respect to a hybrid fault model that includes Byzantine faults.

Several of the formal specifications and verifications performed in support of RCP are individually of considerable complexity and difficulty. But in order to contribute to the larger 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, build on, modify, or cannibalize an intricate verification.

Accordingly, we have been developing and honing our verification tools to better support these large, difficult, iterative, and collaborative verifications. Our goal is to reduce formal verifications as difficult as these to routine exercises, and to maximize the value obtained from formalization and verification.

In this paper, we describe some of the challenges we have faced, lessons learned, design decisions taken, and results obtained.

BibTEX Entry
@inproceedings{fme93,
    AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar and Friedrich von Henke},
    TITLE = {Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned},
    YEAR = {1993},
    EDITOR = {{J.} {C.} {P.} Woodcock and {P.} {G.} Larsen},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {670},
    PAGES = {482--500},
    ADDRESS = {Odense, Denmark},
    MONTH = {April},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/fme93/},
    JOURNAL = {{FME} '93: Industrial-Strength Formal Methods}
}
Files
 













 

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