L'Agence nationale de la recherche Des projets pour la science

Translate this page in english

Ingénierie Numérique & Sécurité (INS) 2012
Projet CAFEIN

Combinaison d'approches formelles pour l'étude d'invariants numériques

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.

Partenaires

CEA LIST CEA LIST

ENSTA ParisTech École Nationale Supérieure de Techniques Avancées - Paritech

INRIA Saclay-Île de France / EPI MAXPLUS Institut national de Recherche en Informatique et Automatique - Saclay-Île de France / EPI MAXPLUS

ONERA ONERA DTIM

Prover Prover Technology

RCF Rockwell collins France

UPVD Université de Perpignan Via Dormitia

Aide de l'ANR 809 839 euros
Début et durée février 2013 - 36 mois

 

Programme ANR : Ingénierie Numérique & Sécurité (INS) 2012

Référence projet : ANR-12-INSE-0007

Coordinateur du projet :
Monsieur Pierre-loic Garoche (ONERA DTIM)
pierre-loic.garoche@nullonera.fr

 

Revenir à la page précédente

 

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.