Abstract FR:

Cette these porte sur la caracterisation des comportements des programmes repartis spmd, produits par distribution automatique de programmes sequentiels. Il s'agit d'un travail de modelisation s'appuyant sur deux outils theoriques: la theorie des ensembles ordonnes et les semi-commutations. L'ensemble des comportements d'un programme spmd est represente par une structure adequate, un automate d'ordres. Les resultats obtenus s'appliquent aussi bien aux programmes sequentiels imperatifs qu'aux programmes reactifs synchrones. Un cadre formel pour la preuve de correction de schemas de repartitions est propose et applique sur un exemple complet: la preuve de correction d'un schema de repartition de programmes sequentiels imperatifs. La derniere partie porte sur la caracterisation de l'asynchronisme et du comportement des canaux de communications d'une classe particuliere de programmes spmd. Les resultats etablis permettent de decider de la bornitude de l'asynchronisme et des canaux de communication