Better Automated Importance Splitting for Transient Rare Events

Carlos E. Budde, Pedro R. d' Argenio, Arnd Hartmanns

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1 Citations

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.
LanguageEnglish
Title of host publicationDependable Software Engineering. Theories, Tools, and Applications
Subtitle of host publicationThird International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings
EditorsKim Guldstrand Larsen, Oleg Sokolsky
PublisherSpringer
Pages42-58
Number of pages17
ISBN (Electronic)978-3-319-69483-2
ISBN (Print)978-3-319-69482-5
DOIs
StatePublished - 2017
Event3rd International Symposium on Dependable Software Engineering, SETTA 2017 - Changsha, China
Duration: 23 Oct 201725 Oct 2017
Conference number: 3
http://lcs.ios.ac.cn/setta2017/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10606
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameLecture Notes in Programming and Software Engineering
PublisherSpringer

Conference

Conference3rd International Symposium on Dependable Software Engineering, SETTA 2017
Abbreviated titleSETTA
CountryChina
CityChangsha
Period23/10/1725/10/17
Internet address

Fingerprint

Model checking
Hinges
Stochastic models
Explosions
Statistical Models
Formal verification

Cite this

Budde, C. E., d' Argenio, P. R., & Hartmanns, A. (2017). Better Automated Importance Splitting for Transient Rare Events. In K. G. Larsen, & O. Sokolsky (Eds.), Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings (pp. 42-58). (Lecture Notes in Computer Science; Vol. 10606), (Lecture Notes in Programming and Software Engineering). Springer. DOI: 10.1007/978-3-319-69483-2_3
Budde, Carlos E. ; d' Argenio, Pedro R. ; Hartmanns, Arnd . / Better Automated Importance Splitting for Transient Rare Events. Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. editor / Kim Guldstrand Larsen ; Oleg Sokolsky. Springer, 2017. pp. 42-58 (Lecture Notes in Computer Science). (Lecture Notes in Programming and Software Engineering).
@inproceedings{805f962b4ccb4e3d91f37ab7c7daa944,
title = "Better Automated Importance Splitting for Transient Rare Events",
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.",
author = "Budde, {Carlos E.} and {d' Argenio}, {Pedro R.} and Arnd Hartmanns",
year = "2017",
doi = "10.1007/978-3-319-69483-2_3",
language = "English",
isbn = "978-3-319-69482-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "42--58",
editor = "Larsen, {Kim Guldstrand} and Oleg Sokolsky",
booktitle = "Dependable Software Engineering. Theories, Tools, and Applications",

}

Budde, CE, d' Argenio, PR & Hartmanns, A 2017, Better Automated Importance Splitting for Transient Rare Events. in KG Larsen & O Sokolsky (eds), Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10606, Lecture Notes in Programming and Software Engineering, Springer, pp. 42-58, 3rd International Symposium on Dependable Software Engineering, SETTA 2017, Changsha, China, 23/10/17. DOI: 10.1007/978-3-319-69483-2_3

Better Automated Importance Splitting for Transient Rare Events. / Budde, Carlos E.; d' Argenio, Pedro R.; Hartmanns, Arnd .

Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. ed. / Kim Guldstrand Larsen; Oleg Sokolsky. Springer, 2017. p. 42-58 (Lecture Notes in Computer Science; Vol. 10606), (Lecture Notes in Programming and Software Engineering).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Better Automated Importance Splitting for Transient Rare Events

AU - Budde,Carlos E.

AU - d' Argenio,Pedro R.

AU - Hartmanns,Arnd

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-69483-2_3

DO - 10.1007/978-3-319-69483-2_3

M3 - Conference contribution

SN - 978-3-319-69482-5

T3 - Lecture Notes in Computer Science

SP - 42

EP - 58

BT - Dependable Software Engineering. Theories, Tools, and Applications

PB - Springer

ER -

Budde CE, d' Argenio PR, Hartmanns A. Better Automated Importance Splitting for Transient Rare Events. In Larsen KG, Sokolsky O, editors, Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. Springer. 2017. p. 42-58. (Lecture Notes in Computer Science). (Lecture Notes in Programming and Software Engineering). Available from, DOI: 10.1007/978-3-319-69483-2_3