Distributed Verification of Rare Properties using Importance Splitting Observers

Cyrille Jegourel 1 Axel Legay 1 Sean Sedwards 1 Louis-Marie Traonouez 1
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance splitting make it appealing for SMC, but optimising its performance in the standard way makes distribution inefficient. We show how it is possible to achieve equivalently good results in less time by distributing simpler algorithms. We first explore the challenges posed by importance splitting and present an algorithm optimised for distribution. We then define a specific bounded time logic that is compiled into memory-efficient observers to monitor executions. Finally, we demonstrate our framework on a number of challenging case studies.
Type de document :
Communication dans un congrès
Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Sep 2015, Edinburgh, United Kingdom. 72
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01238982
Contributeur : Sean Sedwards <>
Soumis le : lundi 7 décembre 2015 - 12:30:25
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : mardi 8 mars 2016 - 12:34:58

Fichier

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

Identifiants

  • HAL Id : hal-01238982, version 1

Citation

Cyrille Jegourel, Axel Legay, Sean Sedwards, Louis-Marie Traonouez. Distributed Verification of Rare Properties using Importance Splitting Observers. Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Sep 2015, Edinburgh, United Kingdom. 72. 〈hal-01238982〉

Partager

Métriques

Consultations de la notice

486

Téléchargements de fichiers

57