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

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.