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 contributionAcademicpeer-review

3 Citations (Scopus)
1 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017)
EditorsKim Guldstrand Larsen, Oleg Sokolsky
Place of PublicationCham
PublisherSpringer
Pages42-58
Number of pages17
ISBN (Electronic)978-3-319-69483-2
ISBN (Print)978-3-319-69482-5
DOIs
Publication statusPublished - 2017
Event3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, 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

Conference

Conference3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, 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.), Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017) (pp. 42-58). (Lecture Notes in Computer Science; Vol. 10606). Cham: Springer. https://doi.org/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. Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017). editor / Kim Guldstrand Larsen ; Oleg Sokolsky. Cham : Springer, 2017. pp. 42-58 (Lecture Notes in Computer Science).
@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 = "Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017)",

}

Budde, CE, D'Argenio, PR & Hartmanns, A 2017, Better Automated Importance Splitting for Transient Rare Events. in KG Larsen & O Sokolsky (eds), Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017). Lecture Notes in Computer Science, vol. 10606, Springer, Cham, pp. 42-58, 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017, Changsha, China, 23/10/17. https://doi.org/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 .

Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017). ed. / Kim Guldstrand Larsen; Oleg Sokolsky. Cham : Springer, 2017. p. 42-58 (Lecture Notes in Computer Science; Vol. 10606).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 - Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017)

A2 - Larsen, Kim Guldstrand

A2 - Sokolsky, Oleg

PB - Springer

CY - Cham

ER -

Budde CE, D'Argenio PR, Hartmanns A. Better Automated Importance Splitting for Transient Rare Events. In Larsen KG, Sokolsky O, editors, Proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017). Cham: Springer. 2017. p. 42-58. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-69483-2_3