Downloading and Installing PVeStA

System Requirements

PVeStA has been built and tested using Java 1.6. Any platform with JVM 1.6 (or later) installed should be able to run PVeStA. Property verification against models expressed as probabilistic rewrite theories in Maude requires at least Maude 2.4 to be installed. The Maude executable must be accessible as the name "maude" from anywhere in the file system. This can be done by first making sure that the Maude executable is named (or linked) as "maude" and then adding its path to the user's $PATH environment variable.

Downloading PVeStA

PVeStA tarball can be downloaded here.

Installing PVeStA

Extract the PVeStA tarball:

tar -xvf pvesta.tar.gz

This will extract PVeStA in a directory named "pvesta", which has the following structure:

./pvesta/pvesta-server.jar # the PVeStA server executable ./pvesta/pvesta-client.jar # the PVeStA client executable ./pvesta/serverlist # an example server list file ./pvesta/examples/ # some verification examples

The examples directory includes the Adaptive Selective Verification case study, in addition to two examples by Koushik Sen from VeStA.

Needless to say, the server executable pvesta-server.jar and the client executable pvesta-client.jar will have to be copied to the machines on which they will be executed. See the Usage section for more information about how the tool is used.