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.

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.

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

• fme93.dvi
• fme93.pdf
• fme93.ps