Langages réactifs synchrones
Année 2019–2020

Début des cours: Vendredi 13 décembre 2019, Bat. Turing, 10h - 12h / 13h - 15h.

Responsable du cours: Marc Pouzet

Objectifs

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 le langage SCADE et son environnement de développement. SCADE est issu du langage synchrone Lustre et intègrent des constructions issus des langages Esterel et Lucid Synchrone.

Ils sont fondés sur le modèle du parallélisme synchrone. Le compilateur d’un langage synchrone garantit des propriété de sûreté importantes pour le logiciel critique: une sémantique déterministe, l’absence de blocage et la génération d’un code séquentiel s’exécutant en temps et mémoire bornés.

Gérard Berry, titulaire de la chaîre “Algorithmes, machines et langages” au Collège de France, a donné une présentation sur les systèmes embarqués ainsi qu’une série de cours sur la prise en compte du temps dans les programmes, en 2012-2013 et 2013-2014. Jean Vuillemin a donné un cours invité sur les circuits synchrones et nombres 2-adiques, Nicolas Halbwachs sur Lustre et Marc Pouzet sur l’extension d’un langage synchrone pour modéliser des systèmes combinant temps discret et temps continu.

Plan et notes de cours

Toutes les notes sont en anglais (course notes are in english).

• Cours 1 – 13/12/19. Une introduction à la programmation synchrone et au langage Lustre.

  Lecture: Cet article est une présentation générale des langages synchrones. J’ai mentionné les articles d’Edward Lee dans le cours: (1 et 2).

  Lire l’article de G. Berry “Real time programming : special purpose or general purpose languages”, disponible ici.

• Cours 2 et 3 — 20/12/19. Génération de code séquentiel pour Lustre. En boucle simple et automate et le problème de ordonnancement statique modulaire.

  Articles à lire:

  • Cet article décrit l’organisation d’un petit compilateur d’un langage synchrone proche de Lustre.
  • Cet article montre comment l’étendre pour compiler un langage combinant data-flow et automates hiérarchiques.
  • Le problème de l’ordonancement statique modulaire est étudié ici (version longue).
  • La génération de code en automate minimal est présentée ici.
• TP – 10/01/20. Programmation du processeur Hack en Lustre et le programme, à partir de ce livre (s’il n’est pas disponible en ligne, prendre cette copie). Le corrigé.
• Notes sur le compilateur MiniLustre. sujet en anglais, les sources OCaml.
• Cours 4 — 17/01/20. Suites, fonctions de suites et horloges. transparents et notes de cours.
• Cours 5 et 6 — 24/01/20. Représentation explicite/implicite, codage 1-hot, composition parallèle, hiérarchique. Vérification formelle.

  Sur la vérification formelle:

  • L’article de Bryant sur les bdds (indispensable !);
  • celui de Sheeran et al. sur la k-induction;
  • L’outil KIND de Hagen et Tinelli utilisant un solveur SMT. L’outil Kind2 qui combine k-induction, BMC et PDR.
  • Mes notes sur la vérification formelle sont issues du chapitre rédigé par Pascal Raymond et qui va bien plus loin.
• Cours 7 — 7/02/20. Systèmes hybrides temps continu/temps discret. Conception, sémantique et implémentation du langage Zélus.

  Articles à lire:

  • Cet article est une présentation courte de Zélus (le manuel, disponible sur la page web, contient un tutoriel sur le langage).
  • Cet article de Benveniste et al. présente une sémantique non-standard synchrone pour les systèmes hybrides combinant temps discret et temps continu. L’article de Zheng et Lee donne une sémantique utilisant le temps “super dense”.
  • La génération de code est tirée de cet article, telle que mise en oeuvre dans SCADE Hybrid.

Exercices

Une petite liste d’exercices (anciens) de programmation.

Logiciel

• Fichier donnant une liste (non exhaustive) de références bibliographiques: bibliographie
• mode Emacs pour Lustre
• Distribution de Lustre. Manuel de référence de Lustre. (version Linux à utiliser en cas de problème de liaison avec les librairies tcl/tk).
• Distribution de Lucid Synchrone
• Distribution d’Esterel (alternative avec binaire pour Linux ici).
• Distribution de ReactiveML
• Distribution de Zélus
• Distribution de Heptagon

Travail personnel:

Cette année, nous vous proposons deux projets différents; l’un consiste à écrire un compilateur vers du code séquentiel (C) de Lustre, l’autre consiste à développer un model-checker par la technique de k-induction.

A rendre au plus tard le 28 février 2020. Le sujet de compilation et le sujet de model-checker avec le code associé. Projet à réaliser seul ou en binôme sur

This document was translated from L^AT_EX by H^EV^EA.