Résumé
E. Ledinot a présenté l’évolution des systèmes informatiques pour l’avionique, qui ont grandi en taille d’un facteur 100 entre 1980 (Mirage F1) et 2000 (Rafale 2000), avec une avionique de plus en plus modulaire. Il a détaillé les problèmes de séquencement et de parallélisation des fonctions, puis montré la difficulté de les réaliser avec les méthodes de programmation déterministe classiques, qui demandent de tout ordonnancer à la main. Il a expliqué pourquoi Esterel résout ce problème en assurant automatiquement un ordonnancement correct par construction et en engendrant un code aux performances prévisibles. Il a montré pourquoi la composition de sous-systèmes développés par des personnes différentes conduit à des problèmes de causalité complexes, résolus dans les dernières versions du compilateur Esterel v5 fondées sur la sémantique constructive. Il a enfin montré pourquoi le nouveau système SCADE 6 décrit ci-dessous est un outil essentiel pour la complexité encore supérieure des applications futures, car il unifie contrôle continu et contrôle discret dans un formalisme graphique familier aux ingénieurs et mathématiquement bien défini.
Emmanuel Ledinot
E. Ledinot est directeur des études scientifique amont de Dassault Aviation. Avec son équipe, il a été un pionnier de l’utilisation des méthodes formelles, et particulièrement d’Esterel et de ses outils de vérification formelle. Esterel n’aurait pas pu atteindre la maturité sans les exemples qu’il nous a fournis, de taille et de complexité bien plus grandes que ceux que nous imaginions au laboratoire.
