La vérification formelle d'un compilateur Lustre

Le séminaire portera sur la formalisation et la preuve d'un générateur de code impératif pour un noyau du langage Lustre, réalisées dans l'assistant de preuve Coq. Une telle vérification formelle, nouvelle dans le domaine, pourrait avantageusement compléter à l’avenir les méthodes de certification actuellement employées pour le langage industriel SCADE 6, qui intègre Lustre et une forme simplifiée d’Esterel sans réincarnation et est utilisé pour programmer des logiciels de contrôle-commande d'applications critiques. Même si le cœur du compilateur ici traité n’est qu’un petit morceau du système total, c’en est un morceau essentiel car tout bug engendré par le compilateur peut avoir des conséquences imprévisibles et potentiellement graves. L’exposé présentera la spécification et la vérification d’un générateur de code simple qui gère les traits principaux de Lustre : l'échantillonnage, les nœuds et les délais. La chaîne de génération de code intègre aussi le compilateur C formellement vérifié CompCert pour produire un code assembleur qui calcule successivement les valeurs spécifiées par le modèle sémantique flot de données. Les garanties offertes par CompCert permettent d'étendre le théorème de correction de la traduction de Lustre à toute la chaîne de compilation des programmes Lustre vers l'assembleur en assurant ainsi une garantie de correction de bout en bout.