VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems

Download:

Download VESTA 2.0 (Binaries only) here.

Installation and Getting Started

Click here.

Screenshot

Overview of VESTA 2.0:

VESTA is a tool for statistical analysis of probabilistic systems. It supports statistical model-checking and statistical evaluation of expected values of temporal expressions. For model-checking VESTA uses a sequence of inter-related statistical hypothesis testing to check if a property specified in probabilistic computation tree logic (PCTL) or continuous stochastic logic (CSL) is satisfied by a stochastic model. The details of the statistical model-checking algorithm can be found here (This paper appeared in CAV 2005). Furthermore, Vesta supports the statistical computation of expected values of expressions written in a query language called Quantitative Temporal Expressions (or QuaTEx in short). Details about QuaTEx can be found here (This paper appeared in QAPL 2005). A case study of DOS-resistant TCP 3-way handshaking protocol can be found here (This paper appeared in FCS 2005). A short description of the VESTA 2.0 tool can be found here (This tool paper appeared in QEST 2005).

Modelling Language:

The analysis algorithms of VESTA are independent of the modelling language for probabilistic systems. VESTA only assumes that it can perform discrete-event simulation of the input probabilistic model. It also assumes that the probability measure associated with the paths of the model is fixed. VESTA allows to plug-in any probabilistic modelling language provided that we provide a discrete-event simulator for the modelling language by implementing the following Java interface:

package vesta.mc;

public abstract class State {
    abstract public double getTime(); // return the current time of
                                      // the state
    abstract public State duplicate(); // duplicates the current
                                       // state and returns it.
    abstract public void pop();        // just make it an empty function
    abstract public boolean sat(int i); // sat(i) returns true if the
                                        // i-th atomic proposition
                                        // holds in the current state
    abstract public void next();        // computes a next state
                                        // of the model from the
                                        // current state using
                                        // discrete-event simulation
                                        // and returns the computed
                                        // state 
    public int ival(int i) {            // ignore this function
        throw new AnyException("ival not defined");
    }
    abstract public double rval(int r); // rval(i) returns the value of the
                                        // i-th expression in the
                                        // current state 
    public long id() {
        throw new AnyException("Id not defined");
    }
}

VESTA currently provides interfaces for two modelling languages:

A language to specify discrete-time and continuous-time Markov chains. The syntax of this language is closely related to that in PRISM.
Note that a file describing a CTMC or a DTMC model must have .ctmc extension. See vesta2/examples/Tandem.ctmc and vesta2/examples/Polling.ctmc for example.
PMaude, a executable algebraic specification language which allows to describe models in probabilistic rewrite theories.
Note that a file describing a PMaude model must have .maude extension. See vesta2/examples/Polling.maude and vesta2/examples/tcpsyn.maude for example. PMaude is not distributed with VESTA 2.0. PMaude can be obtained from here.

Interfaces for other modelling languages can be incorporated by implementing the above interface for the language.

CSL and PCTL: Logic to Express Properties for Model-Checking

VESTA supports statistical model-checking algorithms for the transient part of probabilistic computation tree logic (PCTL) and continuous stochastic logic (CSL). Some example of properties that can expressed using these logics are as follows:

P <= 0.05 [<> < 100.0 @0] : probability that a message queue eventually becomes full in less than 100 time units is less than or equal to 0.05. @0 stands for the atomic proposition full.
@0 => (P >= 0.9 [~ @1 U < 5 @2]): if a message processing server is rebooted then the probability that it recovers within 5 time units without dropping any message is greater than or equal to 0.9. @0 stands for the atomic proposition reboot, @1 stands for the atomic proposition drop, and @2 stands for the atomic proposition recover

The syntax of CSL formulas can be found here. CSL and PCTL logic is described here.

Note that a file describing a property in the form of a formula in CSL or PCTL must have .csl extension. See vesta2/examples/Tandem.csl and vesta2/examples/Polling.csl for example.

Quantitative Temporal Expressions

To gain more insight into a probabilistic model, we realized that model-checking is not sufficient. For example, we wanted to know the expected number of clients that get connected to a server in the presence of SYN flood attack. Therefore, in addition to model-checking, VESTA supports statistical evaluation of the expected values of expressions written in a query language called Quantitative Temporal Expressions (or QuaTEx in short). In QuaTEx, one can easily query about expected time, expected power consumption, expected queue size etc. Some example queries that can be encoded are as follows:

What is the expected fraction of clients that successfully connect to a server under DoS attack?
CountConnected( ) = if { s.sat(1) } then {s.rval(0)} else #CountConnected( ) fi ; eval E[ CountConnected( )] ;
What is the probability that a client connected to a server within 10 seconds after it initiated the connection request?
ProbConnected( ) = if { s.getTime( ) > 10.0 } then {0.0} else if { s.sat(0) } then {1.0} else #ProbConnected( ) fi fi ; eval E[ ProbConnected( ) ];

The expected value of a QuaTEx expression is statistically evaluated with respect to two parameters alpha and, delta provided as input. Specifically, we compute the expected value iteratively by sampling until the size of (1-alpha)100% confidence interval for the expected value gets bounded by delta. A detailed discussion of the QuaTEX is provided here.

The syntax of QuaTEx can be found here.

Note that a file describing a QuaTEx expression must have .quatex extension. See vesta2/examples/Tandem.quatex and vesta2/examples/tcpsyn.quatex for example.