Experiments with distributed Model-Checking of group-based applications

Ludovic Henrio 1 Eric Madelaine 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Group-based distributed systems are specific cases of distributed applications with a parameterized topology. They are naturally modelled by systems with a very large state space. We encode the behavioural semantics of group-based applications using the intermediate format FIACRE. We have experimented with model-checking of such systems, using the CADP verification toolset, and in particular the distributor tool. This allowed us to generate very large but finite state-space on the PacaGrid cloud infrastructure. We have then been able to compare different techniques for generating state-spaces, and experiment with different sizes of the modelled system and of the experimental platform.
Type de document :
Communication dans un congrès
Sophia-Antipolis Formal Analysis Workshop, Oct 2010, Sophia-Antipolis, France. 3p., 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00538499
Contributeur : Eric Madelaine <>
Soumis le : mardi 23 novembre 2010 - 10:26:09
Dernière modification le : jeudi 11 janvier 2018 - 16:32:47
Document(s) archivé(s) le : jeudi 24 février 2011 - 02:27:22

Fichier

05_Madelaine_SAFA2010_final.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00538499, version 1

Collections

Citation

Ludovic Henrio, Eric Madelaine. Experiments with distributed Model-Checking of group-based applications. Sophia-Antipolis Formal Analysis Workshop, Oct 2010, Sophia-Antipolis, France. 3p., 2010. 〈inria-00538499〉

Partager

Métriques

Consultations de la notice

271

Téléchargements de fichiers

130