Zennou, Rachid
[Verfasser:in]
;
Université Paris Cité
[Mitwirkende:r];
Université Mohammed V (Rabat)
[Mitwirkende:r];
Bouajjani, Ahmed
[Mitwirkende:r];
Erradi, Mohammed
[Mitwirkende:r]
Algorithmic methods for the verification of consistency in distributed systems ; Méthodes algorithmiques pour la vérification de la consistance dans les systèmes distribués
Titel:
Algorithmic methods for the verification of consistency in distributed systems ; Méthodes algorithmiques pour la vérification de la consistance dans les systèmes distribués
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Aujourd'hui, nous sommes tous des utilisateurs de systèmes distribués. Un système distribué est un ensemble d'ordinateurs afin d'améliorer les performances par le partage des ressources. En effet, avec l'explosion massive d'Internet, ces systèmes sont devenus nécessaires. Malheureusement, en raison du parallélisme et de la latence de communication sur les grands réseaux, les systèmes distribués peuvent produire des comportements inattendus (incohérents) s'ils ne sont pas correctement conçus et implémentés. Par exemple, un siège dans un vol peut être attribué à deux utilisateurs d'un système de réservation de vol au même temps. Cette thèse aborde le problème de vérifier qu'une implémentation d'un système concurrent / distribué offre à ces clients les garanties de consistance attendues (consistance forte, faible ou éventuelle). En particulier, nous considérons le problème du test des systèmes concurrents / distribués pour déterminer s'ils offrent le niveau de consistance attendu par leurs utilisateurs. Pour une exécution d'un système concurrent / distribué donnée, le test confirme la consistance ou l'inconsistance du système lors de cette exécution. Nous proposons des approches de vérification dynamique par rapport à certains modèles de consistance très connus, i.e., en exécutant un grand nombre de programmes de test et en les vérifiant par rapport à un modèle de consistance donné. Le principal critère de consistance que nous considérons dans cette thèse est un modèle fondamental appelé la consistance séquentielle. Le problème de vérification de ce modèle est connu pour être NP-difficile. La raison est que, pour prouver qu'une exécution est conforme à ce modèle de consistance, il faut trouver un ordre total sur les opérations d'écriture qui l'explique. Par conséquent, il faut énumérer tous les ordres totaux possibles, dans le pire des cas. Au début, nous nous intéressons à vérifier la conformité à des modèles de consistance vérifiables en temps polynomial à l'aide de techniques basées sur la saturation. Nous ...