sécurité - Inria

Showroom des démos

Frama-C, une boîte à outils pour la vérification de logiciels en C

Frama-C fait collaborer de nombreuses techniques d'analyse statique, de la vérification de règles de codage à l'analyse par interprétation abstraite et la vérification de spécifications fonctionnelles grâce aux principes de l’approche déductive de la vérification de programmes. Les domaines visés sont le logiciel embarqué critique, les implémentations de bibliothèques cryptographiques, et la sécurité.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Frama-C, une boîte à outils pour la vérification de logiciels en C

Showroom des démos

Tom : une extension de Java permettant de transformer plus facilement des structures arborescentes et des modèles

Tom est un langage de programmation qui permet d'étendre d'autres langages, et en particulier Java, pour intégrer des constructions de filtrage telles que "match" (construction également présente dans le langage Caml par exemple). Le "filtrage" est une opération qui consiste à rechercher des motifs dans une donnée. Tom permet ainsi de manipuler facilement des structures arborescentes, ce qui en fait un outil adapté pour la transformation de modèles. Il est actuellement utilisé dans le projet QUARTEFT projet financé par la FRAE dans lequel le Laas, l'Irit, l'Onera, Airbus et Ellydis sont impliqués. Notre objectif à long terme est de proposer des outils certifiés de transformation de modèles.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Tom : une extension de Java

Showroom des démos

Recherche par le contenu d'objets 3D

Les technologies récentes de numérisation et de modélisation 3D permettent de disposer de bases de modèles 3D de grande taille. Ces modèles sont très utilisés dans les domaines tels que la CAO, la synthèse d'images et la production audiovisuelle. La recherche par le contenu est une solution nécessaire pour structurer, gérer ces données multimédia, et pour naviguer dans ces bases. Dans ce contexte, notre système permet de retrouver automatiquement les modèles 3D visuellement similaires à un objet 3D requête.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Recherche par le contenu d'objets 3D

Showroom des démos

L’exploration d’architecture dans le domaine aéronautique et spatial par la technologie synchrone

Application de gestion des modes de distribution d'énergie d'un satellite en orbite avec optimisation de sa charge en mode survie. Evaluation de performance des systèmes embarqués distribués via la technologie synchrone.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > L’exploration d’architecture

Showroom des démos

L'outil SynDEx pour l'implantation distribuée optimisée sous contraintes temps réel d'applications embarquées critiques

Les applications embarquées critiques sont généralement modélisées et simulées avec des outils utilisant des schémas-blocs. D'une part on présentera l'outil SynDEx qui permet de lire de tels modèles d'applications, de spécifier des contraintes et des caractéristiques temporelles, de spécifier des architectures matérielles distribuées hétérogènes puis, après avoir effectué automatiquement une analyse d'ordonnançabilité temps réel et des optimisations, de générer du code correct par construction pour ces architectures embarquées. On présentera aussi une passerelle entre l'outil Scicos de modélisation et de simulation pour les systèmes de contrôle-commande et l'outil SynDEx.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > L'outil SynDEx

Showroom des démos

Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Astrée est un analyseur statique permettant la preuve d'absence d'erreurs à l'exécution dans des programmes C critiques embarqués. Cette preuve est entièrement automatique, et est effectuée au niveau du code source, vis à vis de la sémantique du langage. Astrée a analysé avec succès des applications de taille industrielle dans le domaine aéronautique et spatial. L'analyseur Astrée a été conçu et développé au sein de l'équipe Abstraction. Il est actuellement diffusé par l'entreprise Absint Angewandte Informatik.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Showroom des démos

L'outil SynDEx pour l'implantation distribuée optimisée sous contraintes temps réel d'applications embarquées critiques

Les applications embarquées critiques sont généralement modélisées et simulées avec des outils utilisant des schémas-blocs. D'une part on présentera l'outil SynDEx qui permet de lire de tels modèles d'applications, de spécifier des contraintes et des caractéristiques temporelles, de spécifier des architectures matérielles distribuées hétérogènes puis, après avoir effectué automatiquement une analyse d'ordonnançabilité temps réel et des optimisations, de générer du code correct par construction pour ces architectures embarquées. On présentera aussi une passerelle entre l'outil Scicos de modélisation et de simulation pour les systèmes de contrôle-commande et l'outil SynDEx.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Edition de logiciels, systèmes embarqués > Démos > L'outil SynDEx

Showroom des démos

L’exploration d’architecture dans le domaine aéronautique et spatial par la technologie synchrone

Application de gestion des modes de distribution d'énergie d'un satellite en orbite avec optimisation de sa charge en mode survie. Evaluation de performance des systèmes embarqués distribués via la technologie synchrone.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Edition de logiciels, systèmes embarqués > Démos > L’exploration d’architecture

Showroom des démos

Alt-Ergo, preuve automatique pour la certification de code critique

Alt-Ergo est un logiciel pour la démonstration automatique de théorèmes. Il est dédié à la preuve déductive de programmes, qui réduit la correction d'un programme par rapport à sa spécification à la validité d'une formule logique. En particulier, Alt-ergo est situé en bout de chaîne de plate-formes de preuve utilisées dans l'avionique. Selon la complexité des codes analysés, ce sont des milliers de formules qu'il faut prouver. Parce qu'il n'est pas envisageable de faire toutes ces preuves à la main, l'utilisation d'un outil comme Alt-Ergo est cruciale pour le passage à l'échelle de cette approche."

Mots-clés :

Accueil > Innovation > Secteurs industriels > Edition de logiciels, systèmes embarqués > Démos > Alt-Ergo, preuve automatique pour la certification de code critique

Showroom des démos

Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Astrée est un analyseur statique permettant la preuve d'absence d'erreurs à l'exécution dans des programmes C critiques embarqués. Cette preuve est entièrement automatique, et est effectuée au niveau du code source, vis à vis de la sémantique du langage. Astrée a analysé avec succès des applications de taille industrielle dans le domaine aéronautique et spatial. L'analyseur Astrée a été conçu et développé au sein de l'équipe Abstraction. Il est actuellement diffusé par l'entreprise Absint Angewandte Informatik.