Formal verification for fault-tolerant architectures: prolegomena to the design of PVS

摘要: 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 developing formal specifications mechanically checked verifications for fault-tolerant architecture, algorithms, implementations model "reliable computing platform" (RCP) life-critical digital flight-control applications, collaborative project to formally verify commercial avionics processor called AAMP5. Several performed support RCP AAMP5 are individually considerable complexity difficulty. But order contribute overall goal, it has often been necessary modify completed accommodate changed assumptions or requirements, people other than original developer have needed understand, review, build on, modify, extract part an intricate verification. We outline performed, present lessons learned, describe some decisions taken better these large, difficult, iterative, verifications. >