These specifications and proofs in PVS support the paper, "A Unified Fault-Tolerance Protocol,"
submitted to Formal Techniques in Fault-Tolerant and Real-Time Systems (FTRTFT), 2004.

Email the Corresponding Author, Paul Miner, at paul.s.miner@nasa.gov with any questions or inquiries.



To re-run the theory proofs, you will need to:

1.  Download the NASA Langley Research Center PVS Libraries for PVS 3.1 and the PVS strategies Manip and Field (all are obtainable in one tar file on the download page, and instructions are there, too).  If you already have downloaded the libraries, make sure they are up-to-date.

2. Download the dump file of the PVS theories (an un-tarred verion is available here for browsing).

3. Unpack the file (tar -xzvf unified.tgz), and undump the file in PVS (M-x undump-pvs-files).  All files are imported by FTRTFT_top.pvs.

Curator and Responsible NASA Official: Lee Pike
larc privacy statement
last modified: 04 May 2004