Mode d'emploi pour la vérification des protocoles de population

Résumé : Cet article est consacré à la vérification basée sur le modèle model-checking du modèle des protocoles de population introduit par Angluin et al.~\cite{AngluinADFP2006}. Ces deux dernières années, la vérification des protocoles de population par model-checking a fait l'objet denombreuses études et de nouveaux outils ont été proposés. Nous montrons dans cet article que, dans une certaine mesure, les outils classiques de model-checking tels que Spin et Prism peuvent être utilisés pour effectuer les vérifications. Pour cela, nous appliquons la technique d'abstraction par comptage pour obtenir des modèles abstraits de protocoles de population qui peuvent être vérifiés efficacement par les outils de model-checking existants. Le problème essentiel pour la complexité de la vérification des protocoles de population concerne la condition d'équité forte. Cette dernière ne peut être utilisée directement avec Spin même pour des exemples de relativement petite taille. Nous montrons qu'on peut cependant remplacer dans de nombreux cas cette équité par une équité faible efficacement vérifiable en Spin. Plus notable encore, nous montrons que la vérification avec la condition d'équité forte est équivalente à un problème de vérification d'un modèle probabiliste. Ainsi, le model-checker probabiliste Prism s'avère être un outil de vérification adapté aux protocoles de population.
Type de document :
Communication dans un congrès
Ducourthial, Bertrand et Felber, Pascal. 13es Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (AlgoTel), 2011, Cap Estérel, France. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00584684
Contributeur : Carole Delporte-Gallet <>
Soumis le : samedi 9 avril 2011 - 17:04:48
Dernière modification le : jeudi 11 janvier 2018 - 06:17:42
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 16:05:20

Fichier

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

Identifiants

  • HAL Id : inria-00584684, version 1

Collections

Citation

Julien Clément, Carole Delporte-Gallet, Hugues Fauconnier, Mihaela Sighireanu. Mode d'emploi pour la vérification des protocoles de population. Ducourthial, Bertrand et Felber, Pascal. 13es Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (AlgoTel), 2011, Cap Estérel, France. 2011. 〈inria-00584684〉

Partager

Métriques

Consultations de la notice

137

Téléchargements de fichiers

65