Doctorat
Equipe : Parallélisme
Observer la stabilisation
Début le 09/01/2002
Direction : ROZOY, Brigitte
[Joffroy BEAUQUIER]
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI
Soutenue le 15/12/2005 devant le jury composé de :
Joffroy Beauquier
Véronique Benzaken
Béatrice Bérard
Yves Métivier
Brigitte Rozoy
André Schiper
Activités de recherche :
- Vérification
- Algorithmique répartie
- Autostabilisation
- Modélisation
- Tolerance aux pannes
Résumé :
Les systèmes répartis ont deux caractéristiques importantes : ils sont
non seulement complexes, mais en plus soumis à des défaillances.
Ainsi, la vérification et l'étude de la tolérance aux défaillances
dans ces systèmes sont deux problématiques majeurs. Dans cette thèse,
nous proposons une méthode de vérification par model-checking d'un
système réparti fondée sur les ordres partiels. Nous donnons un
algorithme de parcours de graphe qui construit un sous-ensemble réduit
de l'espace des états d'un système réparti, dans lequel il est
possible de vérifier des propriétés stables du système considéré.
D'autre part, nous étudions les systèmes auto-stabilisants qui sont
des systèmes répartis naturellement tolérants aux défaillances. Un
système auto-stabilisant est un système qui, quelque soit son
initialisation finit par se comporter correctement. L'inconvénient
d'un tel système est que celui-ci ne peut pas déterminer de lui-même
s'il répond à sa spécification. Dans cette thèse, nous proposons un
nouveau modèle, fondé sur des observateurs, dans lequel un système
auto-stabilisant peut connaître cette information. Dans ce modèle,
nous prouvons qu'il est possible de construire un observateur
déterministe pour n'importe quelle tâche spécifiée sous un démon
synchrone et pour une topologie distinguée, dès lors que cette tâche
admet une solution auto-stabilisante. Nous introduisons également la
notion d'observateur probabiliste et nous prouvons que de tels
observateurs permettent d'observer une plus grande classe de systèmes
auto-stabilisants que les observateurs déterministes.
Pour en savoir plus: http://info.iut-bm.univ-fcomte.fr/staff/pilard/publication/publication.php
