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 article, we present modes: a statistical model checker that combines fully automated importance splitting to 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 using experiments across multi-core and distributed setups on three case studies and report on an extensive performance comparison with three current statistical model checkers.

An efficient statistical model checker for nondeterminism and rare events / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd; Sedwards, Sean. - In: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. - ISSN 1433-2779. - ELETTRONICO. - 22:6(2020), pp. 759-780. [10.1007/s10009-020-00563-2]

An efficient statistical model checker for nondeterminism and rare events

Carlos E. Budde;
2020-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 article, we present modes: a statistical model checker that combines fully automated importance splitting to 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 using experiments across multi-core and distributed setups on three case studies and report on an extensive performance comparison with three current statistical model checkers.
2020
6
Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd; Sedwards, Sean
An efficient statistical model checker for nondeterminism and rare events / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd; Sedwards, Sean. - In: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. - ISSN 1433-2779. - ELETTRONICO. - 22:6(2020), pp. 759-780. [10.1007/s10009-020-00563-2]
File in questo prodotto:
File Dimensione Formato  
Budde2020_Article_AnEfficientStatisticalModelChe.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Creative commons
Dimensione 1.08 MB
Formato Adobe PDF
1.08 MB Adobe PDF Visualizza/Apri

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/314703
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? 12
social impact