TLPVS is PVS implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to an implementation of a framework for existing rules, it also has new methods which are particularly useful in a deductive LTL system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems - systems in which the number of processes is unbounded - and our - verification rules are appropriate to such systems.
TLPVS was implemented by Tamarah Arons.
PVS and TLPVS are already installed on eeyore.
To start PVS simply type ./pvs from any directory.
In order to run TLPVS follow the instructions in the next section ‘Running TLPVS’. On eeyore the TLPVS library can be found at /users/ariel/TLPVS.
If you want to install TLPVS on your own machine you should do the following:
PVS installed. Latest version and instructions are available here.
Download the most recent version of TLPVS into a new directory, e.g. TLPVS
Run PVS in the TLPVS directory and enter the following commands:
Undump the file dump27p12p06.dat into the current working directory.
undumpting should also create a subdirectory PVSHOME.
Load the main file temporal_logic_prelude.
Prove all theories imported by the loaded file.
Exit PVS (will create binaries and the .pvscontext file).
(Note that proving all theories may take a couple of minutes.)
Place the file pvs-strategies in the working directory.
Start PVS (by typing ./pvs)
Load the TLPVS library:
(The command will ask you for the directory of the library, which is wherever you have installed TLPVS.)
Load your own theory files (e.g. bakery.pvs).
The Analysis of Computer Systems web site