Ce travail porte sur la programmation et la verification des systemes reactifs. Il consiste dans une premiere partie en la definition d'un langage mixte imperatif/declaratif, nomme ArgoLus, fonde sur les langages synchrones Argos et Lustre. Argos est un langage imperatif a base d'automates paralleles et hierarchises. Lustre est un langage declaratif fonde sur le modele flots de donnees. Le langage ArgoLus permet de melanger au niveau source ces deux langages. La definition des traductions structurelles d'ArgoLus en Argos ou en Lustre offre deux solutions interessantes pour mettre en oeuvre ce langage, tout en profitant des environnements deja existants. Dans un deuxieme temps la semantique d'Argos en termes de graphes temporises a ete definie. Initialement, celle-ci est definie en termes de systemes de transitions etiquetees. L'inconvenient de ce modele est lie au phenomene d'explosion du nombre d'etats qui limite les possibilites de verification formelle. Une des causes de cette explosion est la presence dans les programmes de compteurs d'occurrences d'evenement. Les graphes temporises sont des automates etendus avec des compteurs de temps, dont la taille est independante des valeurs limites des compteurs du programme. Par consequent, ils sont moins sensibles au phenomene d'explosion du nombre d'etats, d'ou une amelioration des possibilites de verification formelle. De plus, il est possible grace a ce modele d'exprimer des proprietes quantitatives faisant reference au temps. Enfin, un troisieme aspect de ce travail porte sur l'utilisation pour les systemes reactifs d'outils de verification formelle, non concus exactement pour ce type de systemes.

La programmation synchrone a ete proposee pour faciliter la conception et la programmation des systemes reactifs (systemes dont le role est de reagir continument a leur environnement physique, celui-ci etant incapable de se synchroniser avec le systeme). Ces systemes sont tres souvent repartis, que ce soit pour des raisons d'implantation physique, d'amelioration des performances ou de tolerance aux pannes. En outre, les travaux sur la compilation des langages synchrones ont conduit a utiliser une representation interne des programmes sous forme d'un automate d'etats fini : c'est le format OC. Ce travail porte donc sur la repartition automatique des programmes OC. La principale difficulte est d'assurer l'equivalence fonctionnelle et temporelle entre le programme centralise initial et le programme reparti, et de prouver cette equivalence, ce qui est indispensable dans le domaine du temps reel critique. Nous nous attachons egalement a minimiser localement la structure de controle de chaque programme reparti. Pour cela nous developpons un algorithme original de reduction des tests ``a la volee'' utilisant des techniques de bisimulation. D'autre part nous definissons completement l'environnement d'execution des programmes repartis. Ici notre principal souci est de fournir une solution la plus proche possible de l'execution centralisee. Enfin dans le but d'expliquer les desynchronisations introduites par la repartition, nous proposons une semantique originale du langage synchrone Lustre, semantique definie par des ordres partiels.