Translation of ambient-calculus into IF-2.0, a language for classical transition systems

Ecole: UNIVERSITE DE GRENOBLE 1 - JOSEPH FOURIER
Entreprise: aucune
Niveau: BAC + 5
A l'ère des terminaux mobiles et de l'expansion des réseaux de communication, on trouve de plus en plus d'applications mettant en oeuvre du code se déplaçant sur différents sites, au cours de son exécution, par exemple les services de téléphonie mobile ou dans la gestion de flottes de véhicules. Le contexte du code mobile présente des difficultés particulières. En effet le déplacement du code modifie constamment la topologie du réseau, la localisation d'un processus devient complexe. Or cette localisation est obligatoire d'une façon ou d'une autre dans le cas d'un protocole de communication.
Un exemple en est le protocole RDP (Result Delivery Protocol) développé à l'université de São Paolo. Nous avons modélisé ce protocole en utilisant le language IF-2.0. Les réflexions et analyses tirées de cette étude nous ont poussées à réfléchir sur la traduction d'une algèbre de processus: l'ambiant-calcul vers le language IF-2.0
L'ambiant-calcul procure des primitives de mobilité et de communication, quant à IF-2.0, son environnement de validation est constamment étendu par les recherches dont il fait l'objet, au laboratoire Verimag et ailleurs.
Dans ce rapport, nous proposons une traduction d'un fragment de l'ambiant-calcul vers IF-2.0. Après une présentation de la syntaxe et de la sémantique de ces deux langages, nous verrons la fonction de traduction elle-même ainsi que sa validité par énumération exhaustive. Nous avons relégué à la dernière partie l'étude du protocole RDP bien que chronologiquement elle ait eu lieu avant. Enfin, en annexe, on trouvera le code source de la modélisation de RDP en IF-2.0