Résumé
Compilation d’Esterel v5
Le cours suivant a présenté la compilation d’Esterel en logiciel ou matériel. Historiquement, elle a connu plusieurs phases : traduction des programmes en automates déterministes par calcul symbolique (avec L. Cosserat), traduction en automates bien plus efficace avec meilleure gestion de la causalité (avec G. Gonthier, base de la première industrialisation), puis traduction en circuits fondée sur la sémantique constructive qui évite toute explosion du code. Cette traduction peut être vue comme la construction pour chaque programme d’un réseau de preuves regroupant l’ensemble des preuves constructives du programme pour toutes les entrées possibles, en rejoignant encore une fois le paradigme de Curry-Howard, « calculer c’est prouver ».
Pour les cibles logicielles, les sémantiques mathématiques et les implémentations fondées sur elles ont été déterminantes pour les succès initiaux d’Esterel et pour son industrialisation par CISI-Ingénierie, Simulog, puis ILOG. Elles ont contribué au dialogue avec les utilisateurs, en particulier en avionique (Dassault Aviation). Esterel v5 a été utilisé en protocoles de communication (Bell Labs, ATT, British Telecom), en robotique (Inria). Pour les circuits, Esterel v5 a été commercialisé par Synopsys comme composant d’un logiciel de CAO de systèmes électroniques : il a été directement utilisé par Cadence Design Systems pour la conception conjointe matériel/logiciel, et par Intel et Texas Instruments pour la spécification de circuits de contrôle.
