Smart Reduction

Pepijn Crouzen 1 Frédéric Lang 2
2 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Compositional aggregation is a technique to palliate state explosion — the phenomenon that the behaviour graph of a parallel composition of asynchronous processes grows exponentially with the number of processes — which is the main drawback of explicit-state verification. It consists in building the behaviour graph by incrementally composing and minimizing parts of the composition modulo an equivalence relation. Heuristics have been proposed for finding an appropriate composition order that keeps the size of the largest intermediate graph small enough. Yet the underlying composition models are not general enough for systems involving elaborate forms of synchronization, such as multiway and/or nondeterministic synchronizations. We overcome this by proposing a generalization of compositional aggregation that applies to an expressive composition model based on synchronization vectors, subsuming many composition operators. Unlike some algebraic composition models, this model enables any composition order to be used. We also present an implementation of this approach within the CADP verification toolbox in the form of a new operator called smart reduction, as well as experimental results assessing the efficiency of smart reduction.
Type de document :
Communication dans un congrès
Dimitra Giannakopoulou and Fernando Orejas. Proceedings of Fundamental Approaches to Software Engineering (FASE'2011), Mar 2011, Saarbrucken, Germany. Springer Verlag, 6603, pp.111-126, 2011, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00572535
Contributeur : Christine Mckinty <>
Soumis le : mardi 1 mars 2011 - 16:51:17
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : lundi 30 mai 2011 - 03:00:00

Fichier

Crouzen-Lang-11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00572535, version 1

Citation

Pepijn Crouzen, Frédéric Lang. Smart Reduction. Dimitra Giannakopoulou and Fernando Orejas. Proceedings of Fundamental Approaches to Software Engineering (FASE'2011), Mar 2011, Saarbrucken, Germany. Springer Verlag, 6603, pp.111-126, 2011, Lecture Notes in Computer Science. 〈inria-00572535〉

Partager

Métriques

Consultations de la notice

269

Téléchargements de fichiers

104