Systèmes réactifs logiciels, le design du langage synchrone Esterel v5

Documents et médias

Résumé

Le langage synchrone Esterel v5 a été développé à partir de 1982 dans mon équipe mixte École des mines/Inria à Sophia-Antipolis. En parallèle, celle de N. Halbwachs et P. Caspi développait Lustre à Grenoble et celle d’A. Benveniste et P. Le Guernic développait Signal à Rennes. Esterel visait les applications à contrôle dominant (grands automates, protocoles de communication, interfaces homme-machine, etc.) alors que Lustre et Signal visaient les applications de type flot de données (contrôle continu, traitement du signal). Les trois équipes, chacune composée d’informaticiens et d’automaticiens, ont convergé vers l’utilisation du principe synchrone avec un temps logique nul et un temps physique prédictible, implémenté par une boucle à 4 temps attente / lecture des entrées / calcul de la réaction / production des sorties. L’approche synchrone conduit à un parallélisme déterministe et à la prédictibilité des spécifications et de l’implémentation. Les sémantiques formelles des trois langages ont dirigé leur conception et leur implémentation.

En 1990, en collaboration avec l’équipe de J. Vuillemin chez Digital Equipment, nous avons compris que notre hypothèse de synchronisme logiciel rejoignait celle faite implicitement par les concepteurs de circuits. Cela nous a permis de résoudre deux problèmes cruciaux pour Esterel : la compréhension de la causalité synchrone et l’explosion exponentielle en taille du code généré dans l’implémentation par des automates finis déterministes. Elle a aussi permis de mieux comprendre la correspondance entre automates finis déterministes et non-déterministes [1]. Enfin, traduire les programmes en circuits a permis d’effectuer des vérifications formelles automatiques de propriétés de sûreté : l’ascenseur ne peut pas voyager la porte ouverte, l’avion ne peut pas rétracter son train d’atterrissage quand il est au sol, etc. Le compilateur Esterel a été couplé avec le vérifieur formel TiGeR de Madre, Coudert et Touati développé au même labo qui tirait parti des nouveautés sur la représentation de fonctions booléennes par les BDD (Binary Decision Diagrams). Ces vérifications feront l’objet de plusieurs cours en 2014-2015.

Design et sémantique d’Esterel v5

Ce cours a présenté les fondements d’Esterel : l’hypothèse synchrone, les instructions temporelles primitives ou dérivées, le style de programmation induit [2], la réduction potentiellement exponentielle de la taille des sources par rapport aux méthodes classiques d’automates et la sémantique constructive du langage [3] fondée sur une logique constructive de réécriture des termes. L’idée de cette sémantique est directement issue de l’utilisation de la logique booléenne constructive pour les circuits cycliques.

Références

[1] Détails dans G. Berry, « Penser, modéliser et maîtriser le calcul informatique », Cours et travaux du Collège de France, 110^e année, Paris, Collège de France, 897-926.

[2] Voir le programme du coureur à pieds dans la leçon inaugurale, sous forme vidéo, ou dans Le temps et les événements en informatique, G. Berry, Fayard/Collège de France, 2013 : Édition numérique.

[3] The Constructive Semantics of Pure Esterel