Projets APR

Équipe : APR

  • LCHIP - Low Cost High Integrity Platform

    Le projet LCHIP vise à faciliter grandement le développement d'applications sûres à haut niveau de criticité en fournissant : - un environnement de développement complet permettant de générer et prouver mathématiquement et automatiquement du logiciel à algorithmie bornée, - une plateforme sécurisée et à bas coût pour l'exécution de ces applicatifs, afin de garantir un niveau de sûreté maximal. L'intégration transparente à des langages métier (DSL) et des chaines de production de code tierces autorisent un déploiement sans douleur dans des processus de développement existants et favorisent l'exploitation de la technologie en dehors du consortium.

    Responsable : Thierry LECOMTE
    01/10/2016
    Plus d'informations ici
  • MOPSA - Plateforme ouverte et modulaire pour l'analyse statique

    Le projet Mopsa vise à créer des méthodes et des outils pour rendre les logiciels plus fiables. Les erreurs de programmation sont omniprésentes, avec des conséquences allant de la simple frustration des utilisateurs jusqu'à des pertes pertes économiques voire humaines. Les méthodes traditionnelles basées sur les tests sont insuffisantes pour éliminer toutes les erreurs. Le projet développera des analyses statiques permettant de détecter, dès la compilation, des classes de défauts de programme, en s'appuyant sur la théorie de l'interprétation abstraite. Celle-ci permet en effet de concevoir des analyses approchées (permettant le passage à l'échelle sur des gros programmes) et sûres (aucun défaut n'est manqué). L'analyse statique a connu des succès récents : Astrée, un analyseur industriel a pu prouver l'absence d'erreur d'exécution dans des logiciels d'Airbus. Ces résultats sont néanmoins encore limités au contexte spécifique et bien contrôlé des systèmes embarqués critiques. Le projet vise à développer plus avant l'analyse statique en ciblant des logiciels plus grands, plus complexes et plus hétérogènes, et en la rendant plus facilement utilisable par des ingénieurs non spécialisés pour améliorer les logiciels plus grand public. Nous nous concentrerons sur l'analyse des logiciels open source, facilement accessibles, complexes, répandus et importants d'un point de vue économique (ils sont utilisés dans de nombreuses infrastructures et entreprises), mais aussi du point de vue de la société et de l'éducation (en promouvant les logiciels développés et vérifiés pour et par les citoyens). L'objectif principal que nous considérons est l'ensemble des technologies au cœur de l'Internet sur lesquelles une analyse statique pourrait être appliquée pour assurer un Internet plus sûr. Les défis scientifiques que nous devons surmonter comprennent la conception d'analyses évolutives produisant des informations pertinentes, le support de nouveaux langues populaires (comme Python), et l'analyse de propriétés plus adaptées au développement continu de logiciels. Au cœur du projet se trouve la construction d'une plate-forme d'analyse statique open source. Elle servira non seulement à mettre en œuvre et à évaluer les résultats du projet, mais aussi à créer une dynamique encourageant la recherche en analyse statique et accélérant son adoption dans les communautés de développement open source.

    Responsable : Antoine MINÉ
    01/06/2016
    Plus d'informations ici
  • COVERIF - Vers une combinaison de l’interprétation abstraite et de la programmation par contraintes pour la vérification de propriétés critiques pour des programmes embarqués avec des calculs en virgule flottan

    Pouvoir vérifier la correction et la robustesse des programmes et systèmes devient un enjeu majeur dans une société où les applications embarquées sont de plus en plus nombreuses et où leur caractère critique ne cesse d’augmenter. C’est notamment un enjeu crucial pour le calcul basé sur l’arithmétique des nombres à virgule flottante, qui a des comportements assez inhabituels et qui est de plus en plus utilisée dans les logiciels embarqués. Notons par exemple le phénomène de “catastrophic cancellation” qui invalide la plupart des chiffres significatifs d’un résultat ou encore, des suites numériques dont le point de convergence est très différent sur les réels et sur les flottants. Un problème vient aussi de la difficulté à relier le calcul sur les flottants avec un calcul “idéalisé” qui serait effectué avec des nombres réels, la référence de fait lors de la conception du programme. Pour certaines valeurs d’entrée, le flot de contrôle lié aux réels peut ainsi passer dans une branche de la conditionnelle tandis qu’il passe par l’autre pour les flottants. S’assurer qu’un code, malgré cette divergence de flot de contrôle calcule tout ce qu’il est censé calculer, avec une erreur minimale, est l’objet de l’analyse de robustesse, ou de continuité. Le développement d’un ensemble de techniques et d’outils pour vérifier l’exactitude, la correction et la robustesse est donc un challenge important dans le domaine des logiciels embarqués critiques. L’objectif de ce projet est de contribuer à relever ce défi en explorant de nouvelles méthodes basées sur une collaboration fine entre interprétation abstraite (IA) et programmation par contraintes (PPC). Plus précisément, il s’agit de repousser les limites inhérentes à ces deux techniques, d’améliorer la précision des estimations, de permettre une vérification plus complète des programmes utilisant des calculs sur les flottants, et de rendre ainsi plus robustes les décisions critiques liées à ces calculs. Un des originalités de ce projet est de combiner les deux approches, pour permettre à la preuve de robustesse de bénéficier d’une précision accrue, par l’utilisation de techniques PPC, et le cas échéant, pour exhiber des cas non robustes. Il s’agit aussi de marier les forces des deux techniques : la PPC propose des mécaniques algorithmiques puissantes, mais chères en temps de calcul, pour atteindre des domaines d’une précision arbitraire fixée. L’IA n’offre pas de contrôle fin sur la précision atteinte, mais a développé de nombreux domaines abstraits qui capturent très rapidement des invariants de programme de formes diverses. En intégrant certains mécanismes de la PPC (arbre de recherche, heuristiques) dans des domaines abstraits, on pourra, en présence de fausses alarmes, raffiner le domaine abstrait en se basant sur une notion de précision. La première difficulté à résoudre est d’asseoir les bases théoriques d’un analyseur basé sur deux paradigmes substantiellement différents. Lorsque les interactions entre PPC et IA seront bien formalisées, le deuxième verrou que nous visons à lever est de gérer des contraintes de formes générales et des domaines abstraits potentiellement non-linéaires. Enfin, un verrou important du projet concerne l’analyse de robustesse de systèmes plus généraux que les programmes, par exemple les systèmes hybrides, qui modélisent les programmes de contrôle commande. Les résultats des recherches menées dans ce projet seront validés sur des exemples réalistes issus du monde industriel, afin d’en déterminer l’intérêt et la pertinence. L’utilisation d’exemples réels est un des points clefs de la validation des approches explorées : de par la complexité dans le pire des cas des problèmes traités, les techniques proposées ne traitent de manière acceptable que des sous classes de problèmes. Ainsi, les solutions adoptées restent souvent liées aux problèmes ciblés.

    Responsable : Eric GOUBAULT
    01/10/2015
    Plus d'informations ici
  • ASSUME - Affordable Safe And Secure Mobility Evolution

    ASSUME fournira une ingénierie homogène pour le développement de nouvelles fonctions d’assistance à la mobilité critiques dans le domaine des transports notamment, s’exécutant sur des architectures multi-/pluri-cœurs. Le problème sera traité de manière constructive (synthèse) et par analyse (vérification). Pour ce qui est de la construction efficace de systèmes embarqués, le projet produira outils, normes et méthodes nouvelles afin de répondre à la plupart des défis par conception. Par ailleurs, ASSUME fournira une solution d’analyse statique bien intégrée et sûre, visant à prouver l’absence de défauts, même dans un environnement multi-/pluri-cœurs. De nouveaux algorithmes seront intégrés dans des outils exploitables industriellement. De nouvelles normes d’interopérabilité et de formalisation faciliteront la coopération entre outils, ainsi qu’entre acteurs du marché. Le consortium d’ASSUME comprend des partenaires industriels de premier plan dans le domaine de la mobilité, des fournisseurs d’outils et de service pour le développement de systèmes embarqués ainsi que d’éminents instituts de recherche en analyse statique et synthèse, tant pour le développement traditionnel que pour celui basé sur les modèles.

    Responsable : Udo GLEICH
    01/09/2015
    Plus d'informations ici
  • GDRI-ALEA-NETWORK - ALEA-NETWORK

    ALEA-Network est un GDRI financé par le CNRS et co-signé par 4 universités européennes (Wien, Stockholm, Oxford, Munich). Ce projet regroupe des chercheurs d'Europe et d'autres pays du monde entier, intéressés par l'étude de structures aléatoires discrètes, et provenant de différents domaines: informatique, mathématiques discrètes, probabilités, physique statistique, bio-informatique. Dans ce contexte pluridisciplinaire, l'objectif est d'élaborer des méthodes de quantification de l'alea et d'analyser les propriétés statistiques des structures combinatoires fondamentales.

    Responsable : Michèle SORIA & Jean-François MARCKET
    01/01/2015
    Plus d'informations ici
Archives
 Mentions légales
Carte du site |