Systems Verification using Randomized Exploration of Large State Spaces

Abstract : Exhaustive verification often suffers from the state-explosion problem, where the reachable state space is too large to fit in main memory. For this reason, and because of disk swapping, once the main memory is full very little progress is made, and the process is not scalable. To alleviate this, partial verification methods have been proposed, some based on randomized exploration, mostly in the form of random walks. In this paper, we enhance partial, randomized state-space exploration methods with the concept of resource-awareness: the exploration algorithm is made aware of the limits on resources, in particular memory and time. We present a memory-aware algorithm that by design never stores more states than those that fit in main memory. We also propose criteria to compare this algorithm with similar other algorithms. We study properties of such algorithms both theoretically on simple classes of state spaces and experimentally on some preliminary case studies.
Type de document :
Communication dans un congrès
SPIN, 2008, Los Angeles, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00953617
Contributeur : Arnaud Legrand <>
Soumis le : vendredi 28 février 2014 - 14:11:30
Dernière modification le : mercredi 7 octobre 2015 - 01:15:16
Document(s) archivé(s) le : vendredi 30 mai 2014 - 15:30:28

Fichier

Abed-Vincent-SPIN-2008.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00953617, version 1

Collections

Citation

Nazha Abed, Stavros Tripakis, Jean-Marc Vincent. Systems Verification using Randomized Exploration of Large State Spaces. SPIN, 2008, Los Angeles, 2008. 〈hal-00953617〉

Partager

Métriques

Consultations de
la notice

243

Téléchargements du document

127