Statistical Model Checking: An Overview

Axel Legay 1 Benoît Delahaye 1 Saddek Bensalem 2
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Quantitative properties of stochastic systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for stochastic systems with respect to such logics is typically solved by a numerical approach [31,8,35,22,21,5] that iteratively computes (or approximates) the exact measure of paths satisfying relevant subformulas; the algorithms themselves depend on the class of systems being analyzed as well as the logic used for specifying the properties. Another approach to solve the model checking problem is to simulate the system for finitely many executions, and use hypothesis testing to infer whether the samples provide a statistical evidence for the satisfaction or violation of the specification. In this tutorial, we survey the statistical approach, and outline its main advantages in terms of efficiency, uniformity, and simplicity.
Type de document :
Communication dans un congrès
Runtime Verification, Nov 2010, Malta, Malta. 2010, 〈10.1007/978-3-642-16612-9_11〉
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger
Contributeur : Benoît Delahaye <>
Soumis le : lundi 9 mai 2011 - 16:03:55
Dernière modification le : vendredi 16 novembre 2018 - 01:21:59
Document(s) archivé(s) le : mercredi 10 août 2011 - 02:48:28


Fichiers produits par l'(les) auteur(s)



Axel Legay, Benoît Delahaye, Saddek Bensalem. Statistical Model Checking: An Overview. Runtime Verification, Nov 2010, Malta, Malta. 2010, 〈10.1007/978-3-642-16612-9_11〉. 〈inria-00591593〉



Consultations de la notice


Téléchargements de fichiers