Contributions to Statistical Model Checking

Axel Legay 1
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Statistical Model Checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result by using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows us to handle requirements that cannot be expressed in classical temporal logics. The approach has been implemented in several toolsets, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. Unfortunately, SMC is not a panacea and many important classes of systems and properties are still out of its scope. Moreover, In addition, SMC still indirectly suffers from an explosion linked to the number of simulations needed to converge when estimating small probabilities. Finally,the approach has not yet been lifted to a professional toolset directly usable by industry people. In this thesis we propose several contributions to increase the efficiency of SMC and to wider its applicability to a larger class of systems. We show how to extend the applicability of SMC to estimate the probability of rare-events. The probability of such events is so small that classical estimators such as Monte Carlo would almost always estimate it to be null. We then show how to apply SMC to those systems that combine both non-deterministic and stochastic aspects. Contrary to existing work, we do not use a learning-based approach for the non-deterministic aspects, but rather exploit a smart sampling strategy. We then show that SMC can be extended to a new class of problems. More precisely, we consider the problem of detecting probability changes at runtime. We solve this problem by exploiting an algorithm coming from the signal processing area. We also propose an extension of SMC to real-time stochastic system. We provide a stochastic semantic for such systems, and show how to exploit it in a simulation-based approach. Finally, we also consider an extension of the approach for Systems of Systems. Our results have been implemented in Plasma Lab, a powerful but flexible toolset. The thesis illustrates the efficiency of this tool on several case studies going from classical verification to more quixotic applications such as robotic.
Type de document :
HDR
Computer Science [cs]. Inria Rennes, 2015
Liste complète des métadonnées

Littérature citée [91 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01244469
Contributeur : Fabrizio Biondi <>
Soumis le : mardi 15 décembre 2015 - 18:31:10
Dernière modification le : mercredi 11 avril 2018 - 02:00:07
Document(s) archivé(s) le : samedi 29 avril 2017 - 15:44:40

Fichier

Identifiants

  • HAL Id : tel-01244469, version 1

Citation

Axel Legay. Contributions to Statistical Model Checking. Computer Science [cs]. Inria Rennes, 2015. 〈tel-01244469〉

Partager

Métriques

Consultations de la notice

333

Téléchargements de fichiers

161