Oct 17, 2017: Carlos Budde: Better Automated Importance Splitting for Transient Rare Events

October 17, 2017Better Automated Importance Splitting for Transient Rare Events
Room: Hal B 2BCarlos Budde

Statistical model checking uses simulation to overcome the state space
explosion problem in formal verification. Yet its runtime explodes when
faced with rare events, unless a rare event simulation method like
importance splitting is used. The effectiveness of importance splitting
hinges on nontrivial model-specific inputs: an importance function with
matching splitting thresholds. This prevents its use by non-experts for
general classes of models. In this paper, we propose new method
combinations with the goal of fully automating the selection of all
parameters for importance splitting. We focus on transient
(reachability) properties, which particularly challenged previous
techniques, and present an exhaustive practical evaluation of the new
approaches on case studies from the literature. We find that using
Restart simulations with a compositionally constructed importance
function and thresholds determined via a new expected success method
most reliably succeeds and performs very well. Our implementation
within the Modest Toolset supports various classes of formal stochastic
models and is publicly available.