A Parallel Statistical Model Checking and Quantitative Analysis Tool

An Overview of PVeStA

PVeStA is a client-server-based parallelization of the VeStA tool, originally developed by Koushik Sen, for statistical model checking and quantitative analysis of probabilistic systems. PVeStA implements parallelized versions of both Sen et. al.'s statistical model checking algorithm and Agha et. al.'s statistical quantitative analysis algorithm, in which random samples are computed in parallel by distributing, as evenly as possible, the task of performing Monte Carlo simulations across different computing elements.

As in the original VeStA, PVeStA supports statistical verification of properties expressed in Probabilistic Computational Tree Logic (PCTL), Continuous Stochastic Logic (CSL) or the Quantitative Temporal Expressions language (QuaTEx) against probabilistic real-time models specified as probabilistic rewrite theories in Maude or continuous- or discrete-time Markov Chains.

The work on PVeStA will be presented at CALCO-Tools 2011, in Winchester, UK, and will appear in a future volume of LNCS [pre-print | bibtex].

About PVeStA's Implementation

PVeStA is implemented in Java 1.6, based on the original implementation of VeStA. It consists of two command-line-based executable programs: (1) a client program, which essentially implements the sequential parts of the statistical verification algorithms performing simple hypothesis testing for CSL/PCTL formulas and confidence interval computations for QuaTEx expressions, and (2) a server program, which implements the role of a computing resource that generates random samples by performing discrete-event simulations of a given probabilistic model.

PVeStA can be downloaded from the Download section.

A mirror of this website is available here.