Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-23-1 [2018/09/10 11:26]
pouzet [Équipe pédagogique]
cours:c-2-23-1 [2019/09/06 16:09] (current)
pouzet [Équipe pédagogique]
Line 4: Line 4:
 Responsable : Marc Pouzet (ENS/UPMC) Responsable : Marc Pouzet (ENS/UPMC)
  
-==== Plan du cours et intervenants prévus pour 2018-2019 ====+==== Plan du cours et intervenants prévus pour 2019-2020 ====
  
   * Fondements des langages synchrones: sémantique et compilation;   * Fondements des langages synchrones: sémantique et compilation;
Line 12: Line 12:
   * TD/TP (2*3h)   * TD/TP (2*3h)
  
-Examen: 28/11 - 12h45 - 15h45. 
  
-Débuts des cours: lundi 17 septembre 2018, 8h45 11h45, Batiment Cécile Germain, Université Diderot (Paris 7)+Débuts des cours: lundi 16 septembre 2018, 12h45 15h45, Batiment Cécile Germain, Université Diderot (Paris 7)
  
  
 ==== Objectifs : ==== ==== Objectifs : ====
  
-Les langages synchrones ont été inventés dans les années 80 et 90 pour +Les langages synchrones sont des langages dédiés pour modéliser, programmer des systèmes réactifs embarqués à la fois très complexes et très sûrs. On en trouve des exemples très représentatif dans les avions (systèmes de freinagecommande de vol dans les avions Airbus, Embraer, Comac par exemple), les trains (contrôle de bord, contrôle de la position des trains entre eux, etc.), dans les centrales électriques (arrêt d'urgence, etc.). Plusieurs de ces applications critiques sont développées avec le langage [[http://www.esterel-technologies.com/|SCADE]] issu de
-programmer les systèmes réactifs embarqués à la fois très complexes +
-et très sûrs. Ils sont utilisés en grand pour la programmation des systèmes embarqués les +
-plus critiques: systèmes de freinage des avions et commande de vol (Airbus, Embraer, Comac pour son futur avion de ligne chinois, etc.), contrôle de bord et "interlocking" +
-dans les trains, arrêt d'urgence dans les centrales électriques, etc. +
-Plusieurs de ces applications critiques sont développées avec le langage [[http://www.esterel-technologies.com/|SCADE]] issu de+
 la recherche et des langages Lustre, Lucid Synchrone et Esterel.  la recherche et des langages Lustre, Lucid Synchrone et Esterel. 
  
 Ces langages sont fondés sur le modèle du Ces langages sont fondés sur le modèle du
-[[http://www.college-de-france.fr/default/EN/all/cha_inf2009/Cours_du_13_janvier_2010_Paral.htm|parallélisme synchrone]]. Le programme est décrit dans un langage parallèle de haut niveau et +[[http://www.college-de-france.fr/default/EN/all/cha_inf2009/Cours_du_13_janvier_2010_Paral.htm|parallélisme synchrone]]. Le programme est décrit dans un langage parallèle de haut niveau dont le compilateur 
-le compilateur garantit des propriété de sûreté fortesdéterminisme, absence de blocage (deadlock), génération de code séquentiel s'exécutant en temps et mémoire bornés.  +garantit des propriété de sûreté fortes telles que le déterminisme, absence de blocage (deadlock) et génère du code séquentiel qui est garanti s'exécuter en temps et mémoire bornés. 
- +
-Les principes du parallélisme synchrone ont été repris pour traiter des applications nouvelles: calcul vidéo intensif (TVHD, radars); grandes simulations (réseaux électriques, réseaux de capteurs, interlocking); systèmes de criticité mixte (automobile); musique mixte; langages pour le web; combinaison du temps discret et du temps continu.  Ils ont été intégrés dans des langages généralistes (e.g., ReactiveC, SugarCubes en Java, ReactiveML, FRP en Haskell).+
  
 Le cours présente les principes mathématiques des langages synchrones, Le cours présente les principes mathématiques des langages synchrones,
-leurs fondements sémantiques et logiques, les techniques de compilation vers du logiciel et des circuits,+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. Le cours fait le lien avec des langages fonctionnels typés. leur vérification formelle (par model-checking) et des travaux de recherche récents. Le cours fait le lien avec des langages fonctionnels typés.
  
-Une partie du cours est consacrée aux travaux récents sur la sémantique et l'implémentation des langages  +Cette année, une partie du cours sera consacrée à deux travaux de recherche plus récents et en lien avec besoins pratiques (1) la formalisation et la preuve de correction de bout-en-bout d'un compilateur Lustre dans un assistant à la preuve; (2) la conception, la sémantique et l'implémentation d'un langage de modélisation hybride mélant temps discret et temps continu.
-pour modéliser des systèmes hybrides combinant du temps discret et du temps continu (modélisation de l'environnement physique +
-ou encore l'interface analogique/discret dans un circuit électroniquela Simulink/Stateflow. Le cours montre comment +
-étendre de manière conservatrice un langage synchrone avec du temps continu.+
  
-Il y aura deux séances de TD/TP sur machine (vraisemblablement aux séances 5 et 6) et un projet de programmation.+Il y aura une ou deux séances de TD/TP sur machine (vraisemblablement aux séances 5 et 6) et un projet de programmation.
  
 Cf. Vidéo de Gérard Berry sur les [[http://www.college-de-france.fr/default/EN/all/inn_tec2007/les_systemes_embarques_et_l__2.htm|systèmes embarqués]]; Cf. Vidéo de Gérard Berry sur les [[http://www.college-de-france.fr/default/EN/all/inn_tec2007/les_systemes_embarques_et_l__2.htm|systèmes embarqués]];
Line 53: Line 42:
  
 ==1. Fondements du parallélisme synchrone== ==1. Fondements du parallélisme synchrone==
-   * Fonctions de suites, sémantique de Kahn, causalité, continuité, composition synchrone.+   * Temps continu et temps discret. Abstraction synchrone; suites et fonctions de suites synchrones. Réseaux de processus de Kahn. Causalitécontinuitée, composition parallèle synchrone.
    * circuits booléens; composition parallèle d'automates; hiérarchie et préemption.     * circuits booléens; composition parallèle d'automates; hiérarchie et préemption. 
  
 ==2. Langages synchrones== ==2. Langages synchrones==
-   * Lustre/Lucid Synchrone et Esterel: sémantique; causalité et calcul d'horloges; compilation en code séquentiel et circuits+   * Cas d'un language de suites (Lustre): sémantique dénotationnelle et opérationnellesystèmes de types dédiés (causalité et calcul d'horloge)
-   * Réseaux de Kahn: systèmes N-synchrones et communication par buffer; systèmes insensibles aux délais (circuits élastiques). +   * Compilation formellement vérifié de Lustre vers Clight (compilateur Velus). 
-   * Temps continu/temps discret; sémantique et compilation des langages pour les systèmes hybrides+   * Conception, sémantique et implémentation d'un langage synchrone hybride (langage Zelus)
-   * ReactiveMLprogrammation synchrone en ML.+   * Synchronisme relachémodèle N-synchrone, systèmes multi-horloges périodiques, modèle quasi-synchrone. 
 +   
  
 ==3. Vérification et preuve de systèmes synchrones== ==3. Vérification et preuve de systèmes synchrones==
Line 66: Line 56:
    * Vérification par modèles : codages booléen avant/arrière des espaces d'états; BDD et solveurs SAT (k-induction).    * Vérification par modèles : codages booléen avant/arrière des espaces d'états; BDD et solveurs SAT (k-induction).
    
-==4. Circuits synchrones== 
-   * représentations efficaces des fonctions et circuits booléens; 
-   * Circuits arithmétiques: représentations des nombres, opérateurs arithmétiques, compromis surface/temps. 
- 
 ==Deux séances de TP sur machine:== ==Deux séances de TP sur machine:==
  
Line 105: Line 91:
 ==== Équipe pédagogique ==== ==== Équipe pédagogique ====
  
-| M. Pouzet | PU | ENS/UPMC | DIENS | 
-| J. Vuillemin | PU | ENS | DIENS | 
 | T. Bourke | CR | INRIA | DIENS | | T. Bourke | CR | INRIA | DIENS |
 +| M. Pouzet | PU | ENS/UPMC | DIENS |
  
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA