Statistical model checking of black-box probabilistic systems

By

Full Text:
http://dx.doi.org/10.1007/978-3-540-27813-9_16

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 analyzed in [15]. Our empirical results show that our approach may, at least in some cases, be faster than previous analysis methods.

BibTeX

@inproceedings{conf/cav/SenVA04,
author = "Sen, Koushik and Viswanathan, Mahesh and Agha, Gul",
editor = "Alur, Rajeev and Peled, Doron",
title = "Statistical Model Checking of Black-Box Probabilistic
Systems",
booktitle = "CAV",
crossref = "conf/cav/2004",
ee = "http://dx.doi.org/10.1007/978-3-540-27813-9_16",
keywords = "formal methods, sensor networks, real-time systems",
pages = "202-215",
year = "2004",
}

@proceedings{conf/cav/2004,
editor = "Alur, Rajeev and Peled, Doron",
title = "Computer Aided Verification, 16th International
Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004,
Proceedings",
isbn = "3-540-22342-8",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "3114",
year = "2004",
}