Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087676
Contributor : Uli Fahrenberg <>
Submitted on : Wednesday, November 26, 2014 - 2:50:30 PM
Last modification on : Wednesday, June 16, 2021 - 3:41:38 AM
Long-term archiving on: : Friday, February 27, 2015 - 12:21:08 PM

File

rv14.pdf
Files produced by the author(s)

Identifiers

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. ⟨10.1007/978-3-319-11164-3_28⟩. ⟨hal-01087676⟩

Share

Metrics

Record views

1215

Files downloads

1344