Statistical Model-checking for Rare Events and Wireless Sensor Networks

Statistical model-checking is an alternative verification technique applied on stochastic systems whose size is beyond numerical analysis ability. Given a model (most often a Markov chain) and a formula, it provides a confidence interval for the probability that the model satisfies the formula. One of the main limitations of the statistical approach is the computation time explosion triggered by the evaluation of very small probabilities. In order to solve this problem, we developed a new approach based on importance sampling, coupling and uniformization which applies in the discrete and continuous setting of time bounded or unbounded properties, which will be presented in the first part. The corresponding algorithms have been implemented in our tool Cosmos. In a second part, we will use statistical model checking to solve problems on wireless sensor networks which can be modelised by partially observed Markov decision process.