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.

Better Automated Importance Splitting for Transient Rare Events / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd. - ELETTRONICO. - 10606:(2017), pp. 42-58. (Intervento presentato al convegno SETTA 2017: 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications tenutosi a China nel 2017) [10.1007/978-3-319-69483-2_3].

Better Automated Importance Splitting for Transient Rare Events

Carlos E. Budde;
2017-01-01

Abstract

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.
2017
SETTA 2017: Proceedings of the 3rd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
China
Springer International Publishing
978-3-319-69482-5
978-3-319-69483-2
Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd
Better Automated Importance Splitting for Transient Rare Events / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd. - ELETTRONICO. - 10606:(2017), pp. 42-58. (Intervento presentato al convegno SETTA 2017: 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications tenutosi a China nel 2017) [10.1007/978-3-319-69483-2_3].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314695
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? ND
social impact