Projet ANR-12-INSE-0007 – CAFEIN : Combinaison d'approches formelles pour l'étude d'invariants numériques
Programme : Ingénierie Numérique & Sécurité (INS) 2012
Année de financement : 2012
Coordinateur du projet : Monsieur Pierre-loic Garoche (ONERA DTIM)
Partenaires : Laboratoire d'Intégration des Systèmes et des Technologies; École nationale supérieure des techniques avancées; Algèbres Max-Plus et Mathématiques de la Décision; Office national d'études et de recherches aérospatiales; PROVER TECHNOLOGY; ROCKWELL COLLINS FRANCE; Université de Perpignan - Via Domitia
Montant : 809839.0 euros
Durée : 36 mois
Résumé : Ce projet s'intéresse à la vérification formelle de propriétés fonctionnelles sur des spécifications haut niveau de systèmes critiques, en particulier des systèmes de contrôle-commande décrits en Lustre qui interagissent avec un environnement physique. La complexité de ces systèmes a connu une croissance exceptionnelle ces dernières années, croissance motivée par des avancées techniques mais aussi par des motivations économiques et environnementales. De plus, ces systèmes sont soumis à de fortes contraintes liées à la certification. Devant cette hausse de complexité, le processus de certification, à base de tests essentiellement, a montré ses limites, et les méthodes formelles apparaissent comme une alternative crédible. La future norme DO-178C intègre cette évolution en recommandant l'usage de méthode formelles et de techniques basées sur
les modèles pour le processus de développement, vérification et de validation des systèmes critiques.
Cependant, malgré un intérêt croissant des utilisateurs industriels, la vérification formelle n'est pas encore prête pour un déploiement conséquent dans les processus de développement. Pour les applications industrielles, une intervention humaine, coûteuse en temps de développement et en main d'oeuvre, est encore nécessaire pour obtenir des résultats précis. Ce projet vise à réunir des experts des méthodes formelles, des systèmes hybrides, ainsi que des partenaires industriels et des fournisseurs d'outils pour élaborer, développer et valider de nouvelles techniques de coopérations de méthodes formelles dans le but d'augmenter le degré d'automatisation et donc d'applicabilité de la vérification formelle. Plus particulièrement, nous voulons appliquer ces nouvelles techniques sur des modèles haut niveau, tout en nous intéressant à la compilation de ces modèles vers du code embarqué.
Tout d'abord, le projet cherche à améliorer l'automatisation de la vérification formelle en combinant le système de k-induction et l'interprétation abstraite. En effet, la difficulté dans l'utilisation des méthodes formelles pour la vérification de tels systèmes peut être expliquée par la combinaison de deux sources de complexité. Premièrement, les structures de flot de contrôle, essentiellement basés sur la notion d'horloge - certaines parties du
code étant activés ou désactivés suivant la valeur d'une condition logique fonction des entrées ou d'états internes. Et deuxième la complexité numérique des ces programmes, qui peut s'ajouter à ces conditions d'activation des horloges, tout en admettant, dans certains cas, des invariants complexes, parfois non linéaires.
Un second axe de recherche concerne l'intégration dans l'analyse du modèle Lustre d'information provenant de la théorie des systèmes de contrôle commande et des systèmes hybrides. Nous chercherons à générer des invariants sur des systèmes de contrôle-commande formés d'un
contrôleur synchrone (le programme Lustre) et d'une description en Simulink de l'environnement continu. Nous étudierons comment ces invariants peuvent être utilisés à la fois au niveau de l'analyse du modèle Lustre que pour l'analyse des programmes embarqués.
Enfin, le projet vise à étudier l'impact de l'utilisation de nombres flottants au niveau du programme par rapport à la sémantique réelle des modèles Lustre. Cette différence de comportement peut introduire des bogues qui n'existent pas au niveau de la spécification (dépassement de capacité par exemple). Des outils existent pour évaluer formellement cette différence de comportements (Fluctuat par exemple). Dans ce projet, nous proposerons des techniques de génération de code optimisées pour la gestion des nombres flottants dans le but de minimiser la différence de sémantique entre le
programme généré et la spécification, afin de garantir la préservation de propriétés prouvées sur le code Lustre ou bien issues de la théorie mathématique du contrôle-commande.