Ce site public a pour objet de fournir des informations sur le projet ANR SETIN Checkbound ANR-06-SETI-002 |
Stochastic model checking can be performed by numerical or statistical methods. In model checking formalism, models are checked to see if the considered measures are guaranteed or not, bounding techniques become useful. We propose to apply Stochastic Comparison technique for numerical stochastic model checking. The main advantage of this approach is the possibility to derive transient and steady-state bounding distributions as well as the possibility to avoid the state space explosion problem. For the statistical model checking we propose to study the application of perfect simulation by coupling in the past. This method has been shown that to be efficient when the underlying system is monotonous for the exact steady-state distribution sampling. We consider to extend this approach for transient analysis and to model checking by means of bounding models and the stochastic monotonicity. One of difficult problems for model checking formalism is when the state space is infinite. In some cases, it would be possible to consider bounding models defined in finite state space.
Indeed, formal verification using model checking and performance and dependability evaluation have a lot of things in common. We think that it would be interesting to apply the methods that we have a large experience in quantitative evaluation in the context of stochastic model checking.