Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/inria-00584684
Contributor : Carole Delporte-Gallet <>
Submitted on : Saturday, April 9, 2011 - 5:04:48 PM
Last modification on : Saturday, March 28, 2020 - 2:17:39 AM
Long-term archiving on: : Thursday, November 8, 2012 - 4:05:20 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00584684, version 1

Citation

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

Share

Metrics

Record views

188

Files downloads

220