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 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 talk, I will 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.
The following article covers this material in more detail: " Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS" by Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke (IEEE Transactions on Software Engineering, Vol 21., No. 2, Feb. 1995, pp. 107-125).