Statistical Verification with PVeStA

Usage Description

Generally, the following steps are involved in performing a verification task with PVeStA:

  1. running the server executable pvesta-server.jar on each server machine
  2. creating a list of server addresses in a file
  3. running the client executable pvesta-client.jar with all the appropriate verification parameters, including the server address list file

Running the Server

The server is run simply by issuing the following command:

$java -jar pvesta-server.jar [PORT]

with PORT an optional parameter specifying the port at which the server will listen to incoming client simulation requests. If not specified, the default port 49046 is used.

Creating the Server List

The server list is a simple text file containing the addresses and ports of PVeStA servers to be used by the client, one address:port pair per line. For example, the following is a valid server list:

localhost:49046 localhost:49047

Running the Client

The client program pvesta-client.jar is where a verification task is initiated. The program takes as input a number of arguments, some of which are optional. A list of all arguments can be displayed using the -help option:

$java -jar pvesta-client.jar -help -help,-? displays help information -m,-model <string> model file name - mandatory option -f,-formula <string> formula file name - mandatory option -l,-list <string> serverlist file name and path [default "serverlist"] -k,-kfactor <decimal integer> load factor [default 1] -delta1,-d1 <float (0.0,1.0)> delta1 [default 0.01] -a,-alpha <float (0.0,1.0)> alpha [default 0.01] -b,-beta <float (0.0,1.0)> beta [default 0.01] -delta2,-d2 <float (0.0,1.0)> delta2 [default 0.01] -ps,-pstopping <float (0.0,1.0)> stopping probability [default 0.05] -pd,-pdiscount <float (0.0,1.0]> discount probability [default 1.0] -cs,-cache-size <decimal integer> cache size [default 0] -s,-max-samplesize <decimal integer> max sample size [default 100000000] -arg,-argument <float> argument for the model

Most of these arguments are inherited from the original VeStA tool. More details about these parameters can be found in the cited references in VeStA's site. The server list and load factor parameters are specific to PVeStA though.

As an example, to model check a QuaTEx formula in formula.quatex against a Maude model in model.maude using the servers listed in servers.txt and default values for all other verification parameters, we may issue the following command:

$ java -jar pvesta-client.jar -l servers.txt -m model.maude -f formula.quatex

Important note A: Currently, the model and formula files must be in the current working directory for both the server and client executables. In other words, one has to change to the directory in which the model and formula files are first and then run the executables from there. See the example below.

Important note B: File name extensions must match the content type of the file. In particular, Markov chain model file names must end with ".ctmc", Maude models with ".maude", CSL/PCTL formulas with ".csl", and, finally, QuaTEx formulas with ".quatex", as illustrated by the examples accompanying PVeStA.

An Example

We will use the ASV case study packaged in the PVeStA tarball (see the Download page) to illustrate a typical workflow in carrying out a verification task. Suppose we want to statistically evaluate the QuaTEx formula stored in success.quatex for the ASV Maude model in asv-ideal.maude within a 95% confidence interval of size at most 0.01. Suppose also that this task is to be run on two servers localhost and remote-host at the default port, where localhost will also be hosting the client process.

We run the server executables by first changing to the asv directory on both machines:

$ cd [path-to-pvesta]/examples/asv $ java -jar [path-to-pvesta]/pvesta-server.jar > server.out &

where the actual path to PVeStA's root directory is to be substituted for [path-to-pvesta] above. Next, we create a server list file serverlist containing the following two lines:

localhost:49046 remote-host:49046

Now, with the current working directory being [path-to-pvesta]/examples/asv/, we may initiate the verification task by issuing the command:

$ java -jar [path-to-pvesta]/pvesta-client.jar -l [path-to-serverlist-file]/serverlist \ -m asv-ideal.maude -f success.quatex -a 0.05

Results are displayed once the verification task is completed. The servers will continue to run waiting for further simulation requests for ASV.