Systèmes réactifs et synchrones

Enseignants : Marc Pouzet, Alexandre Chapoutot

Cours :

Les langages synchrones permettent de programmer des systèmes réactifs embarqués à la fois très complexes et très sûrs. Ils rencontrent un grand succès dans divers domaines industriels, pour la programmation du logiciel de controle/commande dans les avions, les trains, les centrales nucléaires, etc. Le système de commande de vol des Airbus, par exemple, est développé avec l’outil SCADE issu du langage synchrone Lustre.
Ils sont fondés sur le modèle du parallélisme synchrone qui introduit une notion de temps logique dans les programmes et donne la possibilité d’écrire des programmes parallèles déterministes. Le compilateur d’un langage synchrone garantit des propriétés de sûreté importantes pour le logiciel critique: exécution déterministe du code, absence de blocage (deadlock), génération de code séquentiel s’exécutant en temps et mémoire bornés, génération de code parallèle, etc.
Le cours donne une introduction au modèle synchrone et à quelques langages qui en sont issus. Il présente leurs fondements mathématiques, les techniques de compilation vers du logiciel et des circuits, leur vérification formelle (par model-checking) et certains travaux de recherche récents. Nous consacrerons la fin du cours aux travaux actuels sur la sémantique et l’impl’ementation des langages de modélisation des systèmes hybrides combinant temps discret et temps continu, tels que Simulink/Stateflow et Modelica.

TD : 11 heures de TD pour 10 heures de cours

Prérequis :