Soutenance de thèse
Nathalie
Tali Sznajder
Titre de la thèse
Synthèse de systèmes
distribués ouverts.
Date et lieu
Le
Jeudi 12
Novembre 2009 à Cachan à 14h00. Salle de Conférences, Pavillon
des Jardins, École Normale Supérieure de Cachan.
Plan
d'accès
Composition du jury
Résumé de la thèse
Cette
thèse est un travail sur la synthèse de systèmes
distribués ouverts. Dans le problème de synthèse,
on considère un système en interaction avec un
environnement incontrôlable, et on se donne une description
formelle de ses comportements corrects (la
spécification). On cherche alors à dériver
automatiquement un programme pour le système dont toutes les
exécutions satisfont la spécification et ce, quelle que
soit la façon dont l'environnement se comporte. Pour le
problème de synthèse de systèmes
distribués, on se donne en plus de la spécification une
description des communications possibles entre les différents
processus du système, ainsi que des communications entre
l'environnement et les processus (l'
architecture). Le but est
alors de synthétiser automatiquement un programme pour chaque
processus du système. Ce dernier problème est
indécidable en général, et le travail
effectué au cours de cette thèse vise à
comprendre les principales causes d'indécidabilité afin
de proposer les restrictions les plus naturelles possibles sous
lesquelles le problème serait décidable. On choisit en
particulier de se restreindre aux spécifications de type
externe, c'est-à-dire ne restreignant que les interactions
entre le système et l'environnement, en laissant non
spécifiées les interactions entre les processus
eux-mêmes. Dans un premier chapitre, on définit un
modèle général présentant de
manière uniforme les différents résultats de la
littérature sur le sujet, qui étaient exprimés
dans des formalismes divers. Ensuite on expose les résultats
obtenus dans le cas de systèmes distribués
synchrones. On propose une condition nécessaire sur
l'architecture des systèmes pour la décidabilité
de ce problème, puis on définit une classe
d'architectures (les architectures uniformément bien
connectées), pour laquelle cette condition devient un
critère nécessaire et suffisant.
Finalement, on essaie d'étendre cette classe en
définissant la classe des architectures bien connectées,
et on montre que le critère établi n'est plus une
condition suffisante pour la décidabilité du
problème sur cette classe plus large. La preuve
d'indécidabilité apporte des éléments
nouveaux sur les causes d'indécidabilité, permettant
d'améliorer la compréhension du problème. Le
dernier chapitre présente les travaux effectués dans le
cas de systèmes ayant un comportement asynchrone. On introduit
un nouveau modèle de communication : la communication par
signaux ; un signal est une action commune à deux processus,
mais qui n'est contrôlée que par un seul. On
s'intéresse à des spécifications externes portant
sur des ordres partiels, et on définit des
propriétés de clôture que les
spécifications doivent respecter. On montre que dans ce cadre
le problème est décidable pour tous les systèmes
dont le graphe de communication est fortement connexe.
Page personnelle
de Tali Sznajder.