Abstract FR:

Les systèmes réactifs sont les systèmes qui doivent répondre à des stimuli répétés de leur environnement par des actions sur lui. La programmation de ces systèmes est naturellement parallèle; les langages classiques y sont mal adaptés, en raison de leur asynchronisme. Dans cette thèse nous étudions la sémantique de langages synchrones spécialement conçus pour cette programmation, et en particulier celle du langage Esterel. Dans ces langages la réaction d'un programme à un stimulus est instantanée, tous les calculs le déterminant devant s’effectuer infiniment rapidement. Nous commençons par étudier le langage Esterel, dont nous donnons une sémantique "naturelle" fondée sur les histoires d'entrées et de sorties des programmes; nous la montrons équivalente à une sémantique comportementale décrivant les changements d'état causés par chaque stimulus. Nous définissons ensuite un modèle algébrique permettant de décrire l'exécution des calculs internes à une réaction. Un théorème d'abstraction exprime l'équivalence entre les sémantiques opérationnelles et comportementales des termes de ce modèle, en l'absence de communication. L'ajout de la communication conduit à une sémantique comportementale simple avec une sémantique opérationnelle non effective. L'introduction d'une analyse statique du flot de contrôle dans la sémantique opérationnelle permet de la rendre effective, et nous montrons que ceci est équivalent à l'introduction de contraintes de causalité au niveau comportemental. De plus nous montrons que ces contraintes ne modifient pas la sémantique des programmes corrects {c'est-à-dire dont l'exécution ne se bloque pas). Enfin nous décrivons un algorithme de compilation des termes de notre modèle en programmes séquentiels, lequel est rendu particulièrement efficace par l’introduction d'une représentation intermédiaire. Son application à Esterel et à des langages similaires ne requiert qu'une simple traduction structurelle.