Résumé
Ce cours a d’abord étudié l’insertion de programmes Esterel (ou synchrones en général) dans des environnements d’exécution arbitraires en détaillant les différentes façons de recevoir ou d’émettre des événements par une machine d’exécution reliant le monde localement synchrone d’Esterel et le monde extérieur asynchrone. Il a détaillé la primitive « exec » d’appel et de gestion d’actions asynchrones, introduite initialement pour le contrôle de robots et déjà brièvement présentée lors du premier cours.
Le cours a ensuite étudié les différentes façons de démontrer automatiquement des propriétés des programmes Esterel, en s’appuyant sur les techniques présentées en 2014-2016 pour la vérification de programmes : calculs directs sur automates explicites, méthodes implicites de vérification à l’aide de solveurs SAT/SMT, etc. Des exemples industriels ont illustré la complémentarité entre les mises au point par simulation et par preuve automatique, mettant en valeur la puissance de cette dernière approche.
