Projets APR [Archives]

Équipe : APR

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 au 05/2021
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 au 09/2020
Plus d'informations ici …
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 au 06/2020
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 au 01/2019
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 au 08/2018
Plus d'informations ici …
UCF - Ubiquitous Contents Framework
Responsable : Jonathan RIVALAN
01/10/2014 au 11/2017
Plus d'informations ici …
MAGNUM - Méthodes Algorithmiques pour la Génération aléatoire Non Uniforme: Modèles et applications

Le thème central du projet MAGNUM est l'élaboration de modèles discrets complexes, ayant des applications dans plusieurs branches de l'informatique. Une des principales motivations du développement de tels modèles est la conception et l'analyse d'algorithmes efficaces dédiés à la simulation de grands systèmes discrets et à la génération aléatoire de grandes structures combinatoires. Une autre motivation importante est de revisiter la théorie de l'analyse de complexité en moyenne sous l'angle de modèles de données réalistes.
Responsable : Michèle SORIA
30/06/2010 au 06/2015
Plus d'informations ici …
CERCLES2 - La Certification Compositionnelle des Logiciels Embarqués CritiqueS et Sûrs

Le projet CERCLES est centré sur la certification des logiciels embarqués critiques et sûrs. Le but est de diminuer notablement le coût de cette opération. La certification des logiciels des systèmes embarqués critiques est une opération industrielle très difficile et fastidieuse. Elle doit respecter un processus long, rigoureux et extrêmement normé. Par exemple la norme DO178B de l'aviation civile, décrit l'ensemble des processus de spécification, conception, codage et vérification du logiciel qu'il faut satisfaire pour obtenir la certification. Le développement logiciel moderne repose sur la mise en oeuvre de composants et de leur assemblage. La norme de certification, en particulier dans son exigence de vérification reposant sur des tests, conduit concrètement à avoir à suivre deux fois le même chemin: une fois lors du développement des composants et une seconde fois lors de leur assemblage. Ce qui induit un coût. L'idée pour tenter de diminuer ce coût - et qui fait l'objet de cette proposition - est de capitaliser la certification des composants. En conséquence, le problème à résoudre est celui de l'existence de méthodes et outils d'assemblages peu coûteux et industrialisables qui permettent de construire l'architecture du système final en induisant sa certification. De telles voies ont déjà été explorées dans le cadre du développement des langages de programmation (typage, objets, modules, contrats) proposant des modèles originaux de conception ou de codage. Mais elles n'abordent pas le domaine du logiciel critique embarqué pour lequel l'exigence de certification est un préalable incontournable (normes de certification) et en particulier, l'exigence de vérification reposant sur des tests et leur analyse de couverture. Il faut obtenir que si A et B sont des composants préalablement certifiés alors on dispose du moyen de vérifier l'assemblage A-B. Ceci imposera, entre autres, qu'on sache décrire correctement les unités A et B en tant que «composants» (par opposition à une application complète) offrant certaines garanties de fonctionnement et possibilité d'assemblage; la composition A-B en tant qu'assemblage préservant les garanties établies pour ses composants et réalisant d'autres exigences de fonctionnement. Sur cette base, on peut espérer établir et la préservation de la correction des composants assemblés et la correction de l'assemblage par rapport à ses propres exigences. En particulier, que les propriétés émergentes d'un assemblage sont ou bien celles attendue ou bien telles qu'elles ne nuisent pas au fonctionnement du système dans son contexte opérationnel. Plus concrètement, nous dirions que le but du projet CERCLES est de résoudre le problème de l'intégration de tests. C'est-à-dire, comment, à partir des tests associés à chaque composant, créer une batterie de tests globaux montrant que l'assemblage réalisé respecte les exigences du système. L'automatisation escomptée de cette création de tests induira une réduction du coût de la certification de l'assemblage.
Responsable : Philippe BAUFRETON
01/04/2011 au 09/2014
Plus d'informations ici …
PWD - Programmation du Web Diffus

L’objectif principal du projet PWD, a été de développer de nouveaux langages dédiés à la programmation du nouveau Web.
Responsable : Manuel SERRANO
01/11/2009 au 10/2013
Plus d'informations ici …
OPENGPU - OPENGPU

Les GPUs (Graphics Processing Units) deviennent une solution de plus en plus prometteuse pour répondre au besoin croissant de puissance de calcul et de traitement des applications numériques, des nouvelles méthodes de conception ou des simulations numériques liées à la recherche. Depuis l'année 2005, la montée en fréquence des processeurs généralistes a laissé la place à la multiplication des cœurs (core) rendant ces solutions plus complexes à exploiter. Dans le même temps, les GPUs ont évolué vers des architectures moins spécialisées rendant leur usage pour des calculs ou des traitements de données envisageable. Cette évolution a été accompagnée par l'émergence d‘architectures unifiées des GPU et en 2008 par la finalisation du standard OpenCL offrant une perspective intéressante pour la programmation de ces architectures. La puissance et le ratio puissance/consommation des GPUs étant supérieurs à ceux des CPUs standards, l’utilisation des GPUs représente une opportunité permettant de disposer de plus de puissance à un coût moindre et pour consommation d'énergie maitrisable. Le projet OpenGPU se propose d’exploiter cette opportunité avec un triple objectif: - construire une plateforme intégrée et ouverte d'outils Open Source d'aide à la parallélisation de code existant, - expérimenter les gains de cette parallélisation au travers de grands démonstrateurs industriels et académiques - construire les architectures matérielles et logicielles adéquates pour l'exploitation de ces nouvelles puissances de calcul et l’amélioration de la consommation énergétique. Le projet Open GPU comporte donc trois grands volets qui sont à la fois complémentaires et en synergie les uns avec les autres dans un but d'augmentation réciproque de la valeur dans chacun des domaines.
Responsable : Eric MAHE
01/01/2010 au 01/2012
Plus d'informations ici …

Mentions légales

Carte du site