Skip to Main content Skip to Navigation
Theses

Rare event simulation for statistical model checking

Cyrille Jegourel 1
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : In this thesis, we consider two problems that statistical model checking must cope. The first problem concerns heterogeneous systems, that naturally introduce complexity and non-determinism into the analysis. The second problem concerns rare properties, difficult to observe, and so to quantify. About the first point, we present original contributions for the formalism of composite systems in BIP language. We propose SBIP, a stochastic extension and define its semantics. SBIP allows the recourse to the stochastic abstraction of components and eliminate the non-determinism. This double effect has the advantage of reducing the size of the initial system by replacing it by a system whose semantics is purely stochastic, a necessary requirement for standard statistical model checking algorithms to be applicable. The second part of this thesis is devoted to the verification of rare properties in statistical model checking. We present a state-of-the-art algorithm for models described by a set of guarded commands. Lastly, we motivate the use of importance splitting for statistical model checking and set up an optimal splitting algorithm. Both methods pursue a common goal to reduce the variance of the estimator and the number of simulations. Nevertheless, they are fundamentally different, the first tackling the problem through the model and the second through the properties.
Document type :
Theses
Complete list of metadata

Cited literature [136 references]  Display  Hide  Download

https://hal.inria.fr/tel-01244471
Contributor : Fabrizio Biondi <>
Submitted on : Tuesday, December 15, 2015 - 6:36:50 PM
Last modification on : Tuesday, June 15, 2021 - 4:13:54 PM
Long-term archiving on: : Saturday, April 29, 2017 - 3:46:03 PM

Identifiers

  • HAL Id : tel-01244471, version 1

Citation

Cyrille Jegourel. Rare event simulation for statistical model checking. Computer Science [cs]. Universite de Rennes 1, 2014. English. ⟨tel-01244471⟩

Share

Metrics

Record views

277

Files downloads

604