Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Systemes synchrones (24h, 3 ECTS)

Responsables : Marc Pouzet (Univ. Pierre et Marie Curie et ENS Ulm) et Jean Vuillemin (ENS Ulm)

Plan du cours et intervenants prévus pour 2010-2011

1. Langages synchrones (4 cours - 12h, Marc Pouzet)
2. Circuits synchrones (4 cours - 12h, Jean Vuillemin)
3. TD/TP (2 * 3h, Louis Mandel)

Débuts des cours: mercredi 23 septembre 2010, 16h15 - 19h15, ENS.

Objectifs :

Les langages synchrones rencontrent actuellement de nombreux succès dans la réalisation de systèmes embarqués qui sont à la fois très complexes et très sûrs. On en rencontre des exemples très significatifs d'utilisation dans les avions, les trains, les centrales nucléaire ou les téléphones portables. Le système de commande de vol des Airbus, par exemple, est développé avec l'outil SCADE fondé sur le langage synchrone Lustre.

Le cours proposé donne une introduction au modèle de concurrence synchrone et aux langages de programmation qui en sont issus. Il présente leurs fondements théoriques, la sémantique des principaux langages, leur compilation, leur vérification formelle en abordant les travaux les plus récents. Ce cours prend en compte les aspects logiciels et matériels qui sont indissociablement liés.

Cette année, nous consacrerons un cours de 3h a la formalisation d'un compilateur de Lustre vers C à l'aide de Coq ainsi qu'un cours sur la théorie des systèmes N-synchrones. Deux séances de TD/TP sur machine seront organisées.

Plan du cours :

1. Fondements des systèmes synchrones

• Fonctions sur les suites discrètes, causalité, continuité, synchronisme.
• Circuits et automates booléens; composition synchrone; réseaux de Kahn, flots et horloges.

2. Langages synchrones

• Lustre et Esterel: sémantique dénotationnelle, sémantique comportementale. Types et horloges. Compilation.
• Langages synchrones fonctionnels.
• Désynchronisation. Systèmes insensibles aux délais (circuits élastiques).
• Systèmes N-synchrones; communication par buffer, gîgue, temps d'exécution.

3. Vérification et preuve de systèmes synchrones

• Observateurs synchrones: codages Lustre/Esterel 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).

4. Circuits synchrones

• Circuits électroniques : de l'analogique au digital, du temps continu au temps discret synchrone. Logique combinatoire et mémoires.
• Circuits programmables : structure et programmation des FPGA. Systèmes re-configurables.
• Circuits arithmétiques: représentations des nombres, opérateurs arithmétiques, compromis surface/temps.

Langues du cours :

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.

Supports de cours :

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

Pré-requis :

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

Cours liés :

• 2-4, 2-3, 2-8.

Bibliographie :

• N. Halbwachs, Synchronous programming of reactive systems. Kluwer Academic Pub. 1993.
• Stephen A. Edwards. Languages for Digital Embedded Systems. Kluwer. 2000.
• 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. 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.

Les années précédentes

• Année 2009-2010
• Année 2008-2009
• Année 2007-2008
• Année 2006-2007

Équipe pédagogique

Attachment	Action	Size	Date	Who	Comment
Stages_qa_IP_version1.doc	manage	34.5 K	26 Oct 2004 - 06:47	LouisGranboulan