L'analyse des dépendances de flot de données est une étape cruciale lors de la parallélisation. La description détaillée des dépendances entre opérations et pour chaque élément de tableau rend possible l'application de techniques de parallélisation performantes. Cependant, ce type d'analyse a deux principaux inconvénients~: son coût élevé et son domaine restreint à des dépendances affines en fonction des compteurs de boucles. On décrit d'abord dans cette thèse un algorithme polynômial pour le calcul des dépendances affines, dont la complexité et le domaine d'application sont meilleurs que ceux des méthodes existantes. Puis, dans la continuité des travaux de J.-F. Collard, on propose un cadre général pour l'analyse, éventuellement approchée, de n'importe quelle dépendance. Le modèle de programmes est formé des programmes sans procédure, comportant des accès quelconques aux éléments de tableaux. Une méthode itérative originale trouve des propriétés entre les contraintes non-affines du problème afin d'améliorer la précision du résultat. Notre méthode est capable de tirer parti de n'importe quelle caractérisation affine de ces contraintes et possède un critère d'optimalité de l'approximation. Enfin, plusieurs applications traditionnelles de l'analyse de flot de données sont adaptées à notre méthode approchée et nous détaillons plus particulièrement l'expansion mémoire, en donnant une méthode offrant un compromis entre surcoût à l'exécution, taille mémoire et degré de parallélisme.

Les travaux décrits dans ce manuscrit de thèse s'inscrivent dans le cadre des méthodes formelles pour les langages de spécifications formées d'automates communicants. Ce type de langage est largement utilisé dans les industries de pointe où le niveau de fiabilité requis est élevé (e.g. aéronautique, transports), car ils permettent d'améliorer la précision des spécifications et d'exploiter des outils de simulation, de test ou de vérification qui contribuent à la validation des spécifications. Un frein au passage à l'échelle industrielle de ces méthodes formelles est connu sous le nom de l'explosion combinatoire, qui est due à la fois à la manipulation de larges domaines numériques, et au parallélisme intrinsèque aux spécifications.<br />L'idée que nous proposons consiste à contourner ce phénomène en appliquant des techniques de réduction paramétrée, pouvant être désignées sous le terme anglo-saxon "slicing'', en amont d'une analyse complexe. Cette analyse peut ainsi être effectuée a posteriori sur une spécification réduite, donc potentiellement moins sujette à l'explosion combinatoire. Notre méthode de réduction paramétrée est basée sur des relations de dépendances dans la spécification sous analyse, et est fondée principalement sur les travaux effectués par les communautés de la compilation et du slicing de programmes. Dans cette thèse nous établissons un cadre théorique pour les analyses statiques de spécifications formées d'automates communicants, dans lequel nous définissons formellement les relations de dépendances mentionnées ci-dessus, ainsi que le concept de "tranche" de spécification par rapport à un "critère" de réduction. Ensuite, nous décrivons et démontrons les algorithmes efficaces que nous avons mis au point pour calculer les relations de dépendances et les tranches de spécifications, et enfin nous décrivons notre mise en oeuvre de ces algorithmes dans l'outil "Carver", pour la réduction paramétrée de spécifications formées d'automates communicants.