Importance Splitting in Uppaal

Statistical Model Checking is a simulations-based verification technique that has gathered increased focus in the past ten years, due to its applicability to handle much larger models compared to exhaustive verification techniques used in model checking. Statistical Model Checking is also applicable to a larger class of systems than exhaustive methods—in particular its ability to handle hybrid systems is important. To apply statistical model checking we must however accept that verification results are probabilistic, and simulations exercise only the most likely behaviour of models. Unfortunately the events we are often interested in finding/estimate the probability of are rare. In its core form, Statistical Model Checking cannot reliably estimate such events. In this work we investigate how to incorporate the rare event simulating technique importance splitting into Uppaal SMC.