FidelR – FidelR

FidelR se concentre sur l'application des assistants de preuve (Coq) aux langages pour la « conception assistée par modèles » de logiciels contrôle-commande embarqués et a la sûreté de leurs compilateurs. Deux aspects étroitement liés seront étudiés. Premièrement, nous étendrons le compilateur formellement vérifié Vélus avec les machines à état hiérarchiques de Scade 6. Cela nécessite de développer de nouveaux modèles sémantiques, d'implémenter des passes de compilation et de démontrer la correction de ces passes. Deuxièmement, nous développerons de nouvelles techniques et tactiques pour vérifier des modèles paramétrés avec un lien formel entre les propriétés démontrées et le code généré. L'objectif est de contribuer à renforcer et simplifier les processus existants pour qualifier un compilateur industriel et à fournir plus d'assistance par ordinateur pour la gestion rigoureuse du développement de logiciels contrôle-commande embarqués.