An efficient statistical model checker for nondeterminism and rare events
- PDF / 1,114,803 Bytes
- 22 Pages / 595.276 x 790.866 pts Page_size
- 63 Downloads / 184 Views
STTT Special Issue TACAS 2018
An efficient statistical model checker for nondeterminism and rare events Carlos E. Budde1
· Pedro R. D’Argenio2,3,4
· Arnd Hartmanns1
· Sean Sedwards5
© The Author(s) 2020
Abstract Statistical model checking avoids the state space explosion problem in verification and naturally supports complex nonMarkovian 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.
1 Introduction Statistical model checking (SMC [1,49,81]) is a formal verification technique for stochastic systems. Using a formal stochastic model, specified as e.g. a continuous-time Markov chain (CTMC) or a stochastic variant of Petri nets, SMC can The authors are listed in alphabetical order. This work was supported by ANPCyT Project PICT-2017-3894 (RAFTSys), by ERC Grant 695614 (POWVER), by the JST ERATO HASUO Metamathematics for Systems Design Project (JPMJER1603), by the NWO SEQUOIA Project, by NWO VENI Grant 639.021.754, and by SeCyT-UNC Project 33620180100354CB (ARES).
B
Arnd Hartmanns [email protected] Carlos E. Budde [email protected] Pedro R. D’Argenio [email protected] Sean Sedwards [email protected]
1
University of Twente, Enschede, The Netherlands
2
Universidad Nacional de Córdoba, Córdoba, Argentina
3
CONICET, Córdoba, Argentina
4
Saarland University, Saarbrücken, Germany
5
University of Waterloo, Waterloo, Canada
answer questions such as “what is the probability of system failure between two inspections” or “what is the expected time to complete a given workload”. SMC is gaining popularity for complex applications where traditional exhaustive probabilistic model checking is limited by the state space explosion problem and by the inability to efficiently handle non-Markovian formalisms or complex continuous dynamics. At its core, SMC is the integration of classical Monte Carlo simulation with formal models. By only sampling concrete traces of the model’s behaviour, its memory usage is effectively constant in the size of the state space, and it is applicable to any behaviour that can effectively be simulated. However, its use in formal verification faces two key challenges: rare events and nondeterminism. The result of an SMC analysis is an estimate qˆ of some actual quantity of interest q together wi
Data Loading...
