Abstract FR:

Le travail présenté dans cette thèse s'inscrit dans le cadre du développement raisonné de programmes parallèles résolvant des problèmes de type transformationnels, et implantés sur des architectures DMPC. Nous y présentons un formalisme permettant la description des données et des dépendances, et des règles de raffinement permettant de transformer progressiveùent des énoncés exprimés sous la forme d'un ensemble de propriétés, en calculs et en communications. La méthode proposée, basée sur la distinction des calculs et des communications, se décompose en trois étapes principales: à partir d'une spécification parallèle exprimée dans notre formalisme, sous la forme d'une propriété de sureté et d'une propriété de vivacité, On précise les calculs par raffinements de la première propriété. Elle associe un processus à chaque variable en introduisant des propriétés de coopération qui permettent de caractériser les dépendances de variables, les propriétés de coopération sous la forme de relation dites de communications. Enfin, on représente la solution parallèle sous forme de processus communicants séquentiels