Statistical model checking in Uppaal: lets practice

Statistical model-checking is a recent technique used for both verification and performance analysis of hybrid systems. It does not suffer from decidability issues or state-space explosion compared to traditional model-checking. Furthermore, it is applicable to more powerful formalisms such as stochastic hybrid automata. Its principle is simple so how simple is it really to make it work in practice? In this extended abstract, we raise a number of practical issue, some of them disconnected from the underlying theory, and show how they are addressed in Up- paal SMC