|
Modélisation et validation d’algorithmes répartis
La modélisation et la validation des algorithmes répartis se heurtent au nombre d’états
possibles de tels systèmes, nombre souvent infini. Les méthodes de vérification par
exploration exhaustive du domaine d’états sont alors impossibles.
Face à ce problème, l’approche adoptée comporte deux aspects complémentaires :
- d’une part, un effort de modélisation : il s’agit de définir des abstractions de haut
niveau exprimant la répartition d’un calcul et/ou des données pour en simplifier
la description et l’analyse ;
- d’autre part, une démarche de preuve par raffinement : il s’agit, partant d’une solution
centralisée du problème, solution plus simple à valider, d’introduire la répartition par
raffinements successifs. Chaque raffinement doit bien sûr être validé.
Cette approche a été appliquée à de nombreux algorithmes classiques (exclusion
mutuelle, réplication de données, terminaison de calcul diffusant, etc.) ou originaux
(observations, vecteurs de chemins).
Voir aussi le site de l’équipe Modélisation et Validation de la Répartition à l’IRIT/ENSEEIHT.
À lire dans la même rubrique :
Revenir à la rubrique Recherches
|