INS - Ingénierie Numérique & Sécurité

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

Combinaison d’analyses formelles pour l’étude d’invariants numériques

Vers la coopération de méthodes pour l'analyse de systèmes cyber-physiques critiques: de la conception à l'implantation.

De nombreuses problématiques au long du cycle de développement

Le développement des systèmes critiques embarqués autorise désormais l'utilisation des méthodes formelles pour garantir le bon comportement du système final et obtenir des crédits de certification. <br /> <br />Ces méthodes formelles restent cependant utilisées dans des cas très spécificiques et ne constituent pas le moyen principal de vérification et validation. Les besoins identifiés par le projet CAFEIN sont articulés autour du principe de collaboration de ces méthodes pour augmenter leur applicabilité et efficacité. En particulier, les objectifs concernent la définitions de nouvelles méthodes de vérification au niveau modèle, la prise en compte de la sémantique hybride, tant pour la compilation que la vérification et, enfin la ­compilation des réels en arithmétique flottante. <br /> <br />Un des enjeux est l'évaluation sur des exemples significatifs­ industriels­ open­source. Plus spécifiquement les méthodes mises au point ont été évaluées sur les exemples suivants: le Triplex Voter (Rockwell Collins), le cas d'étude Research Open­Source Avionics and Control Engineering (ROSACE) et le NASA Transport Class Model (TCM).

Les travaux ont été structurés en fonction de leur positionnement dans le cycle de développement. La première tâche concerne la collaboration de méthodes au niveau modèle (par exemple modèle synchrone) et les problématiques de préservation de propriétés le long du développement. La seconde tâche étudie des problématiques plus amont avec la prise en compte de la dynamique de l’objet contrôlé: la sémantique hybride. Enfin la troisième tâche s'intéresse plus spécifiquement à l'impact de la précision machine fini sur le code généré et les analyses.

La première tâche a permis de proposer des nouvelles méthodes permettant d'effectuer de la synthèses d'invariants, par exemple par élimination de
quantificateurs ou en utilisant des outils numériques comme l'optimisation convexe. Des propositions ont été faites pour permettre de revalider automatiquement des propriétés invariantes inductives au niveau du code généré.

En ce qui concerne les systèmes hybrides des méthodes de simulation ensembliste ont été développée, en particulier à l'aide d'arithmétique affine et de zonotopes. Enfin des extensions SMT pour les systèmes hybrides permettent d'étudier des propriétés inductives sur des modèles hybrides.

­Pour l'axe sur la précision des calculs, des progrès ont été fait sur les méthodes de calculs d'erreurs flottantes, par exemple à l'aide d'extensions quadratiques de l'arithmétique affine, mais ces méthodes ont également été intégrées à la chaîne de compilation pour en améliorer les performances numériques.

­

Les perspectives sont nombreuses et concernent chaque tâche: la mise au point de nouvelles méthodes collaboratives permettant la synthèse automatique d'invariants plus riches, l'extension des méthodes proposées en SMT vers l'analyse de propriétés de sûreté (à temps infini) pour les systèmes hybrides dirigés par le temps, et, enfin, la­ prise en compte de la sémantique flottante dès le niveau modèle.

Les méthodes de revalidation des propriétés le long du cycle de développement sont également très attirantes pour soutenir le développement et l'utilisation des méthodes formelles dans l'industrie.

42 publications dont 19 collaboratives, des prototypes et une collaboration fructueuse avec le projet américain jumelé NSF CrAVES.

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.

Coordinateur du projet

Monsieur Pierre-loic Garoche (ONERA DTIM) – pierre-loic.garoche@enac.fr

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.

Partenaire

RCF Rockwell collins France
Prover Prover Technology
UPVD Université de Perpignan Via Dormitia
INRIA Saclay-Île de France / EPI MAXPLUS Institut national de Recherche en Informatique et Automatique - Saclay-Île de France / EPI MAXPLUS
CEA LIST CEA LIST
ENSTA ParisTech École Nationale Supérieure de Techniques Avancées - Paritech
ONERA ONERA DTIM

Aide de l'ANR 809 839 euros
Début et durée du projet scientifique : janvier 2012 - 36 Mois

Liens utiles

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter