Sciweavers

CAV
2004
Springer

Statistical Model Checking of Black-Box Probabilistic Systems

13 years 9 months ago
Statistical Model Checking of Black-Box Probabilistic Systems
Abstract. We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numerical and statistical analysis methods, we assume that the system under investigation is an unknown, deployed black-box that can be passively observed to obtain sample traces, but cannot be controlled. 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 a “don’t know” answer. We implemented our algorithm in a Java-based prototype tool called VeStA, and experimented with the tool using case studies ...
Koushik Sen, Mahesh Viswanathan, Gul Agha
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CAV
Authors Koushik Sen, Mahesh Viswanathan, Gul Agha
Comments (0)