Timothy Bourke (12h) - Marc Pouzet (12h)
- Langages de programmation pour la programmation des systèmes réactifs.
- Exemples et applications avec les langages Lustre, Scade, Zélus et Simulink.
- Fondements mathématiques: composition synchrone; suites et fonctions; machines de Moore et de Mealy; sémantique de Kahn.
- Vérification formelle par model-checking.
- Sémantique statique et dynamique d'un langage réactif synchrone.
- Système de types dédiés: analyse des boucles de causalité (deadlock), calcul d'horloges.
- Génération de code séquentiel et sa formalisation dans un assistant de preuve.
- Conception, sémantique et implémentation d'un langage de modélisation pour les systèmes hybrides.

* TD/TP (2*3h)

Débuts des cours: mardi 17 septembre 2024, 8h45 - 11h45, Bâtiment Cécile Germain, Université Diderot (Paris 7) - salle 1002.

Les langages synchrones sont des langages dédiés à la conception et à l'implémentation du logiciel temps réel embarqué à la fois très complexes et très sûrs. Par ex.: le système de freinage et de commande de vol des avions de ligne, les moteurs électriques et la gestion des batteries d'une voiture, le contrôle de bord et le routage des trains, le système d'arrêt d'urgence d'une centrale nucléaire, etc. Plusieurs de ces logiciels très critiques sont développées avec le langage de programmation synchrone SCADE Suite (exposé au CdF) issu et intégrant les résultats de la recherche fondamentale en programmation.

Les langages synchrones sont fondés sur le modèle du parallélisme synchrone. Le système est décrit dans un langage de programmation de haut niveau disposant de constructions de programmation adaptée à la description d'un système réactif, offrant des garanties de sûreté fortes garanties à la compilation: déterminisme de la sémantique, absence d'inter-blocage (deadlock), génération de code séquentiel s'exécutant en temps et mémoire bornés.

Le cours présente les principes mathématiques des langages synchrones, leurs fondements sémantiques et logiques, les techniques de compilation vers du logiciel, leur vérification formelle par model-checking et des travaux de recherche récents; en particulier le lien avec les langages de modélisation de systèmes hybride combinant temps discret et temps continu tels que Simulink. Le cours montre les liens entre la programmation synchrone et la programmation fonctionnelle typée.

Cette année, nous commençons le cours par la présentation de travaux de recherche très récents:

* la formalisation de sémantiques et d'algorithmes de compilation avec la preuve de correction de bout-en-bout du compilateur Vélus dans un assistant à la preuve.

* La seconde partie s'intéresse à des langages synchrones issus de Lustre et vus sous l'angle de langages fonctionnels typés: on étudie l'impact de l'ordre supérieur, de structures de contrôles (e.g., réinitialisation modulaire, automates hiérarchiques), leurs sémantique statique et dynamique. On montre, par exemple, que certaines propriétés clefs telles que le déterminisme peuvent êtres décrits et vérifiés modulairement par un système de types dédié.

* Dans la troisième partie du cours, on montrera deux extensions nouvelles: - l'écriture de modèles hybrides, combinant des constructions d'un langage synchrone (à temps discret) et des équations différentielles ordinaires (ODE) pour décrire l'interaction entre du logiciel et son environnement physique. Nous verrons les questions que cela soulève en terme de conception, de sémantique statique et dynamique, de compilation et de système à l'exécution (pour faire le lien avec un solveur d'ODE).

- l'expression dans un langage réactif de calculs périodiques — une situation industrielle ancienne et fréquente, en particulier pour les commandes de vol d'un avion —. Nous verrons comment en vérifier la cohérence au moyen d'un système de type dédié (un “calcul d'horloges”) et comment produire du code séquentiel efficace.

Il y aura une ou deux séances de TD/TP sur machine et un projet de programmation.

Cf. Vidéo de Gérard Berry sur les systèmes embarqués; Jean Vuillemin sur les circuits synchrones; Nicolas Halbwachs sur Lustre; Marc Pouzet sur les langages de programmation des systèmes hybrides à temps discret/continu.

• Temps continu et temps discret. Abstraction synchrone; suites et fonctions de suites synchrones. Réseaux de processus de Kahn. Causalité, continuité, composition parallèle synchrone.
• circuits booléens; composition parallèle d'automates; hiérarchie et préemption.

• Cas d'un language de suites (Lustre); réinitialisation modulaire; automates hiérarchiques: sémantique dénotationnelle et opérationnelle; systèmes de types dédiés (causalité et calcul d'horloge).
• Compilation formellement vérifié de Lustre vers Clight (compilateur Velus).
• Conception, sémantique et implémentation d'un langage synchrone hybride (langage Zelus).
• Synchronisme relaché: modèle N-synchrone, systèmes multi-horloges périodiques, modèle quasi-synchrone.

• Observateurs synchrones: codage des propriétés de sûreté.
• Vérification par modèles : codages booléen avant/arrière des espaces d'états; BDD et solveurs SAT (k-induction).

• TP de programmation Lustre ou Esterel;
• Réalisation d'un compilateur de MiniLustre (en Ocaml)

Le cours sera a priori en français. Cependant, s'il est suivi par des étudiants non francophones et en accord avec les étudiants, ce cours pourra être donné en anglais.

Des notes de cours seront disponibles sous la forme de polycopiés ou de transparents, en français ou en anglais.

Pas de prérequis mais il est recommandé d'avoir suivi les cours de M1 “compilation” et “sémantique des langages de programmation”

2-4, 2-3, 2-8, 2-37.1

• N. Halbwachs, Synchronous programming of reactive systems. Kluwer Academic Pub. 1993.
• Donald Knuth. The Art of Computer Programming. Vol. 4A. 2011 (boolean functions).
• G. De Micheli, Synthesis and optimizations of digital circuits, McGraw-Hill, 1994.
• Edward A. Lee and Pravin Varaiya. Structure and Interpretation of Signals and Systems. Addison Wesley, 2003.
• Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. The Synchronous Languages 12 Years Later. Proceedings of the IEEE 91(1):64-83, January 2003.
• Gérard Berry. Chaire Algorithmes, machines et langages. Cours de l'année 2012-2013 (l'informatique du temps et des événements) et de l'année 2013-2014 (Le temps élargi : horloges multiples, temps discrets et temps continu).