VeStA (Verification based on Statistical Analysis)

Tool Author: Koushik Sen


Vesta: Roman Goddess of Hearth and Fire
VeStA is an efficient tool for verification based on statistical analysis. It has two componenets: the learning-CTMC module and the model-checking module.

Learning Continuous-time Markov Chains

This module implements the algorithm to learn CTMC described in [SVActmc04]. The algorithm correctly identifies the CTMC model in the limit when it is given samples drawn from a distribution generated by a CTMC. One technical difficulty when talking about samples drawn from a CTMC is that traditionally CTMCs are unlabeled, and so they only have runs, which are sequences of states that are traversed and not traces. However, the problem is that when samples are drawn from an implementation getting information that uniquely identifies states is expensive and impractical, and can lead to the construction of a very large model which does not collapse equivalent states. To address this difficulty, we introduce the model of an Edge Labeled Continuous-time Markov Chain where edges are labeled from a finite set of alphabet and traces are sequences of edge labels which are given to the learning algorithm.

Model-Checker

The model-checker can perform statistical verification of deployed black-box probabilistic systems. The tool is based on a new statistical approach to analyzing stochastic systems against CSL specifications (subset containing time-bounded until operator) as described in [SVAcav04]. Given a set of executions obtained by Monte Carlo simulation and a property, our algorithm checks, based on statistical hypothesis testing, whether the sample provides evidence to conclude the satisfaction or violation of a property, and computes a quantitative measure (p-value of the tests) of confidence in its answer; if the sample does not provide statistical evidence to conclude the satisfaction or violation of the property, the algorithm may respond with an "don't know" answer. We have experimented with the tool using case studies previously analyzed in Younes and Simmons' tool, ProVer. Our empirical results show that our approach has a significantly good running time than previous analysis methods and demonstrate the feasibility of our approach.

Downloads

The code for the learning module can be downloaded here.
The code for the model-checker module can be downloaded here.
To obtain the code for the model-checker proposed in the paper "On Statistical Model Checking of Stochastic Systems" (under submission) send me mail at ksen@cs.uiuc.edu .

Documentation

For more details about the tool please refer to the following papers: