A Statistical Model Checker for Nondeterminism and Rare Events

Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns, Sean Sedwards

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

Abstract

Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this tool paper, we present modes: a statistical model checker that combines fully automated importance splitting to efficiently estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the Modest Toolset, it supports a variety of input formalisms natively and via the Jani exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities with an experimental evaluation across multi-core and distributed setups on three exemplary case studies.
LanguageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II
EditorsDirk Beyer, Marieke Huisman
Place of PublicationCham
PublisherSpringer
Pages340-358
Number of pages19
ISBN (Electronic)978-3-319-89963-3
ISBN (Print)978-3-319-89962-6
DOIs
StatePublished - 2018

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10806
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Model checking
Software architecture
Explosions
Sampling
Statistical Models

Cite this

Budde, C. E., D'Argenio, P. R., Hartmanns, A., & Sedwards, S. (2018). A Statistical Model Checker for Nondeterminism and Rare Events. In D. Beyer, & M. Huisman (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II (pp. 340-358). (Lecture Notes in Computer Science; Vol. 10806). Cham: Springer. DOI: 10.1007/978-3-319-89963-3_20
Budde, Carlos E. ; D'Argenio, Pedro R. ; Hartmanns, Arnd ; Sedwards, Sean. / A Statistical Model Checker for Nondeterminism and Rare Events. Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. editor / Dirk Beyer ; Marieke Huisman. Cham : Springer, 2018. pp. 340-358 (Lecture Notes in Computer Science).
@inproceedings{7addba7ad54b4d3eb8a8ea77cf23b224,
title = "A Statistical Model Checker for Nondeterminism and Rare Events",
abstract = "Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this tool paper, we present modes: a statistical model checker that combines fully automated importance splitting to efficiently estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the Modest Toolset, it supports a variety of input formalisms natively and via the Jani exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities with an experimental evaluation across multi-core and distributed setups on three exemplary case studies.",
author = "Budde, {Carlos E.} and D'Argenio, {Pedro R.} and Arnd Hartmanns and Sean Sedwards",
note = "Open Access",
year = "2018",
doi = "10.1007/978-3-319-89963-3_20",
language = "English",
isbn = "978-3-319-89962-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "340--358",
editor = "Dirk Beyer and Marieke Huisman",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

}

Budde, CE, D'Argenio, PR, Hartmanns, A & Sedwards, S 2018, A Statistical Model Checker for Nondeterminism and Rare Events. in D Beyer & M Huisman (eds), Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10806, Springer, Cham, pp. 340-358. DOI: 10.1007/978-3-319-89963-3_20

A Statistical Model Checker for Nondeterminism and Rare Events. / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd; Sedwards, Sean.

Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. ed. / Dirk Beyer; Marieke Huisman. Cham : Springer, 2018. p. 340-358 (Lecture Notes in Computer Science; Vol. 10806).

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

TY - GEN

T1 - A Statistical Model Checker for Nondeterminism and Rare Events

AU - Budde,Carlos E.

AU - D'Argenio,Pedro R.

AU - Hartmanns,Arnd

AU - Sedwards,Sean

N1 - Open Access

PY - 2018

Y1 - 2018

N2 - Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this tool paper, we present modes: a statistical model checker that combines fully automated importance splitting to efficiently estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the Modest Toolset, it supports a variety of input formalisms natively and via the Jani exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities with an experimental evaluation across multi-core and distributed setups on three exemplary case studies.

AB - Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this tool paper, we present modes: a statistical model checker that combines fully automated importance splitting to efficiently estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the Modest Toolset, it supports a variety of input formalisms natively and via the Jani exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities with an experimental evaluation across multi-core and distributed setups on three exemplary case studies.

U2 - 10.1007/978-3-319-89963-3_20

DO - 10.1007/978-3-319-89963-3_20

M3 - Conference contribution

SN - 978-3-319-89962-6

T3 - Lecture Notes in Computer Science

SP - 340

EP - 358

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer

CY - Cham

ER -

Budde CE, D'Argenio PR, Hartmanns A, Sedwards S. A Statistical Model Checker for Nondeterminism and Rare Events. In Beyer D, Huisman M, editors, Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. Cham: Springer. 2018. p. 340-358. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-89963-3_20