UE M1 SAR -- SPECIF / LANGAGES SYNCHRONES
Le cours présente le modèle des systèmes réactifs synchrones (Machine de Mealy), le langage de description Lustre, ainsi que sa compilation (vers code C ou vers circuit) et les vérifications automatiques qui peuvent être mises en oeuvre. 2 TP permettent la mise en pratique autour de Lustre et Lesar, un petit projet permet d'aller plus loin. Le cours et les exercices reprennent en partie les supports de P. Raymond (Verimag).
Notes de Cours : (au fur et à mesure)
Articles sur langages synchrones :A synchronous language at work : The story of Lustre, N. Halbwachs, 2005.
The synchronous languages twelve years later, A. Benveniste et al, 2002.
Virtual Execution of AADL Models via a Transation into Synchronous Programs, N. Halbwachs et al, 2007.
Enoncés de TP
Lustre : utilisation de la plate-forme Lustre-v4, disponible à l'adresse : http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html (fournis par P. Raymond)
Enoncé de TP1
Enoncé de TP2
Enoncé du projet
EXAMEN :> Notes de cours et de TP autorisées et bienvenues. Au programme : écriture de programme Lustre; compilation Lustre - Automates et vérification ; compilation Esterel (si on a le temps de l'aborder en cours et TD).
Annales d'examen : énoncé 2009, énoncé 2010, énoncé 2012.