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.

A statistical model checker for nondeterminism and rare events / Budde, Carlos E.; R. D'Argenio., Pedro; Hartmanns, Arnd; Sedwards, Sean. - ELETTRONICO. - 10806:(2018), pp. 340-358. (Intervento presentato al convegno TACAS 2018: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Greece nel 2018) [10.1007/978-3-319-89963-3_20].

A statistical model checker for nondeterminism and rare events

Carlos E. Budde;
2018-01-01

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.
2018
TACAS 2018: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND
Springer Verlag
978-3-319-89962-6
978-3-319-89963-3
Budde, Carlos E.; R. D'Argenio., Pedro; Hartmanns, Arnd; Sedwards, Sean
A statistical model checker for nondeterminism and rare events / Budde, Carlos E.; R. D'Argenio., Pedro; Hartmanns, Arnd; Sedwards, Sean. - ELETTRONICO. - 10806:(2018), pp. 340-358. (Intervento presentato al convegno TACAS 2018: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Greece nel 2018) [10.1007/978-3-319-89963-3_20].
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/314683
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 27
  • ???jsp.display-item.citation.isi??? 26
  • OpenAlex ND
social impact