TLPVS

TLPVS is our 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 implementing a framework for existing rules, we have also derived 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.

The paper TLPVS: A PVS-Based LTL Verification System describes TLPVS.

The most recent version of TLPVS is here (April, 2004).

We also provide some examples. They all run with April version of TLPVS:
The UML MARS example
The UML prime-sieve example
The Mips hardware example

For any questions or comments, please e-mail: tamarah_dot_arons_at_weizmann.ac.il.

Dept. of Computer Science and Applied Math
The Weizmann Institute of Science
Rehovot 76100, Israel
TelePhone: +972-8-934-3434
Telefax: +972-8-934-4122
To comment on this service, send feedback to the Nir Piterman