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 ...

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Koushik Sen, Mahesh Viswanathan, Gul Agha
• Keywords: Analysis Methods, CAV 2004, Continuous Stochastic Logic, Formal Methods, Statistical Analysis Methods