L'objectif général de ce stage de DEA consiste à trouver des solutions à un challenge important et difficile:
passer d'un modèle infini d'un système à objets répartis,
à
un modèle fini pour model checking.
Nous avons développé ProActive,
une bibliothèque 100% Java, qui fournit :
o des objets distants,
o des appels asynchrones avec futurs transparents,
o de la migration d'objets actifs (mobilité),
le tout offrant des mécanismes
de synchronisation de haut niveau qui simplifient la programmation répartie.
Dans ce cadre, nous avons défini le calcul ASP (Asynchronous Sequential Processes),
un calcul d'objets à la Abadi-Cardelli, qui modélise
de façon précise et élégante la sémantique infinie d'un tel système à objets répartis.
Voir ici
pour une présentation rapide de ProActive
et du Calcul ASP.
D'autre part, nous avons commencé la vérification formelle par
model checking de systèmes à objets répartis.
Nous utilisons un modèle à base d'automates finis synchronisés, et des outils
de vérification permettant de composer, de minimiser et de comparer de
tels systèmes, et de vérifier leur propriétés comportementales (absence
de deadlock, propriétés de sureté et de vivacité).
Le sujet de DEA consiste donc à:
trouver un ou plusieurs mappings d'un calcul à objets
répartis vers un modèle fini.
On pourra par exemple définir différents sous-ensembles du calcul d'objets
pour lesquels on définira différents mappings. Ce genre d'approche utilise des
restrictions syntaxiques du langage, et a déjà été utilisé dans d'autres
contextes, par exemple pour Java ou pour les calculs de processus.
En fonction des affinités de l'étudiant, ce stage pourra être plus ou moins formel, et présenter plus ou moins de mise en oeuvre.
Ces travaux pourront naturellement se poursuivre en Thèse de Doctorat.