Faster Statistical Model Checking by Means of Abstraction and Learning

Ayoub Nouri 1 Balaji Raman 1 Marius Bozga 1 Axel Legay 2 Saddek Bensalem 1
2 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper investigates the combined use of abstraction and probabilistic learning as a means to enhance statistical model checking performance. We are given a property (or a list of properties) for verification on a (large) stochastic system. We project on a set of traces generated from the original system, and learn a (small) abstract model from the projected traces, which contain only those labels that are relevant to the property to be verified. Then, we model-check the property on the reduced, abstract model instead of the large, original system. In this paper, we propose a formal definition of the projection on traces given a property to verify. We also provide conditions ensuring the correct preservation of the property on the abstract model. We validate our approach on the Herman's Self Stabilizing protocol. Our experimental results show that (a) the size of the abstract model and the verification time are drastically reduced, and that (b) the probability of satisfaction of the property being verified is correctly estimated by statistical model checking on the abstract model with respect to the concrete system.
Type de document :
Communication dans un congrès
RV, Sep 2014, Toronto, Canada. 2014, 〈10.1007/978-3-319-11164-3_28〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01087676
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 14:50:30
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : vendredi 27 février 2015 - 12:21:08

Fichier

rv14.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay, Saddek Bensalem. Faster Statistical Model Checking by Means of Abstraction and Learning. RV, Sep 2014, Toronto, Canada. 2014, 〈10.1007/978-3-319-11164-3_28〉. 〈hal-01087676〉

Partager

Métriques

Consultations de la notice

514

Téléchargements de fichiers

212