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

    7 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 Dive into the research topics of 'Better Automated Importance Splitting for Transient Rare Events'. Together they form a unique fingerprint.

  • 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