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 
, SMC can answer two types of questions:
- Quantitative: What is the probability that S satisfies ?
- Qualitative: Is the probability for S to satisfy greater or lower than some given threshold
?
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 ) such that Pr(|p’-p|<
)>=
, where and 
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 , hypothesis tesing decides which of the hypothesis 
against 
is correct, given a confidence level (
). 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.
