Abstract FR:

Dans cette these, nous proposons une approche a la programmation de systemes en utilisant le formalisme gamma. Dans ce formalisme, les programmes sont decrits par transformation de multi-ensembles. Une caracteristique distinctive de gamma est la possibilite d'exprimer les algorithmes sous une forme tres abstraite, sans sequentialite superflue. Dans notre approche, nous specifions le comportement du systeme par l'enonce des proprietes d'un programme gamma et nous derivons un programme gamma qui satisfait ces proprietes. Nous transformons alors ce programme en un reseau de processus communicants. Ces processus sont des programmes gamma pouvant etre raffines pour les mettre en uvre sur une machine. Dans notre approche, nous prouvons formellement la correction de la transformation d'un programme en un reseau de processus