Statistical Model Checking (SMC) is a formal verification technique that combines simulation and statistical methods for the analysis of stochastic systems. It represents a powerful scalable alternative to numerical probabilistic model checking techniques that suffer from state space explosion issues.
Given a formal model of the stochastic system S and a formal specification of the requirement to verify \phi, SMC can answer two types of questions:
- Quantitative: What is the probability that S satisfies \phi ?
- Qualitative: Is the probability for S to satisfy \phi greater or lower than some given threshold \theta ?
The quantitative question can be answered by using probability estimation techniques based on Chernoff-Hoeffding bound. It mainly consists of computing an estimation p’ of p (the actual probability for S to satisfy \phi) such that Pr(|p’-p|<\delta)>=1-\alpha, where \delta and \alpha are respectively the required precision and the confidence level [1] [2].
Regarding the qualitative question, it is mainly answered using a hypothesis testing approach. Assuming p is the probability for S to satisfy \phi, hypothesis tesing decides which of the hypothesis H_0:p>=\theta against H_1:p<\theta$$ is correct, given a confidence level (\alpha,\beta$$). One important work proposed in this context can be found in [3]. It relies on the Wald Probability ratio Test [4]
We implemented statistical model checking algorithm in the SBIP tool that supports different stochastic models, i.e. discrte-time Markov chains (DTMCs), continous-time Markov chains (CTMCs), and generalized semi-Markov processes (GSMPs). All these models can described in a high-level component-based modeling formalism BIP. For properties specification, the tool supports bounded LTL and MTL logics.