Statistical model checking of black-box probabilistic systems
By
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", }