Sites Inria

English version

Rencontres Inria - Industrie

Les industries de l'aéronautique et de l'espace - Partie 2 : Démos

GOLAEM

Au cours de la journée du 17 mai vous avez pu assister aux démonstrations de technologies issues d'Inria et de ses partenaires industriels.

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

Équipe-projet : ABSTRACTION

Équipe-projet commune avec l'Ecole Normale Supérieure de Paris et le CNRS

Résumé : 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 : analyse statique, vérification, qualitification, sûreté, systèmes critiques embarqués

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

Équipe-projet : AOSTE

Équipe-projet commune avec le laboratoire I3S (UNSA et CNRS)

Résumé :  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 : Ordonnançabilité, distribué, temps réel, embarqué, implantation

TimeSquare : Spécifications Fonctionnelles à base de Temps Logique en Ingénierie des Modèles

Équipe-projet :  AOSTE

Équipe-projet commune avec le laboratoire I3S (UNSA et CNRS)

Résumé : TimeSquare est basé sur le formalisme CCSL (Clock Constraint Specification Language), partie du profil OMG UML MARTE (modélisation et l'analyse de systèmes temps-réel embarqués). L'outil permet de spécifier des horloges logiques et de les associer à des activations et rythmes comportementaux au sein d'un système embarqué (par exemple modélisé en UML ou SysML). TimeSquare permet l'analyse et l'unification des horloges logiques et de leurs temps hétérogènes, dans une perspective de placement/ordonnancement d'applications sur des plates-formes d'exécution.

Mots clés : systèmes Embarqués, UML/SysML, horloges logiques, langages polychrones, ordonnancement par contraintes

Un processus de développement durable : l'expérience ATL

Équipe-projet : ATLANMOD

Équipe-projet commune avec l'Ecole des Mines de Nantes.

Partenaire industriel :  Obeo

Résumé :  L'Ingénierie Dirigée par les Modèles consiste en la définition d’éléments logiciels par des modèles précis. La transformation de modèles permet alors d’en automatiser L’exploitation. Elle est notamment utilisée pour le développement logiciel, pour la rétro-ingénierie, ou encore en tant qu’élément du système logiciel (modèles à l’exécution). L’équipe AtlanMod travaille en collaboration avec Obeo sur ATL : un outil de transformation de modèles.

Mots clés :  transformation de modèles

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

Équipe-projet :  ESPRESSO

Équipe-projet commune avec le CNRS, l'INSA de Rennes, l'université de Rennes 1

Partenaire industriel : Geensoft

Résumé :  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 : synchrone, SIGNAL, RT-Builder, polychrony, temps réel

Recherche par le contenu d'objets 3D

Équipe-Projet :  IMEDIA

Résumé : 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  : recherche par le contenu d’objets 3D, indexation 3D

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

Équipe-projet :  PAREO

Équipe du LORIA commune avec le CNRS, les universités Henri Poincaré, Nancy 2 et INPL

Résumé  : 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  : Java, transformations, modèles, arbres, certification

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

Équipe-projet : PROVAL

Équipe-Projet commune avec l'université Paris-Sud 11 et le CNRS (LRI)

Partenaire industriel : AdacoreRésumé : 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 : analyse statique, vérification, logique de Hoare, interprétation abstraite

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

Equipe-projet : PROVAL

Équipe-Projet commune avec l'université Paris-Sud 11 et le CNRS (LRI)

Résumé :  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 :  démonstration automatique, preuve de programme

Optimisation de la planification des opérations

Équipe-Projet :  REALOPT

Équipe-Projet commune avec l'université Bordeaux 1, l'université Bordeaux 2, l'ENSEIRB et le CNRS.

Partenaires industriels : Exeo et eurodecision

Résumé :  Nous présentons les problématiques de planification de la production, de l’optimisation combinée des tournées de livraison liée à la gestion d’inventaires, de l’optimisation de la collecte des déchets, de la construction du programme de vol et rotation d’équipage, et de l’optimisation de la conception. Notre équipe Inria, RealOpt, et nos partenaires industriels Synoptis eXEO Solutions et Eurodecision développent des méthodes de résolution et des logiciels pour de telles applications. La démonstration inclut la présentation du progiciel Synoptis (de eXEO Solutions) et OptiFleet (de Eurodecision).

Mots clés :  optimisation combinatoire, logistique, planification, conception, rotation

Vérification des contraintes temporelles dans les systèmes embarqués critiques

Équipe-projet :  TRIO

Équipe-projet du LORIA commune avec le CNRS, les universités Henri Poincaré, Nancy 2 et l'INPL et l'ENS Lyon.

Partenaire industriel :  Rtaw

Résumé :  Certains systèmes embarqués critiques dans l’avionique ou l’automobile sont aujourd’hui constitués de dizaines de calculateurs qui exécutent du logiciel ayant de fortes contraintes temps réel et échangent des milliers de flux de données. Nous présentons une suite de logiciels d’analyse et de simulation qui permettent de donner des garanties sur le comportement temporel des systèmes embarqués et d’optimiser leur dimensionnement matériel.

Mots clés :  système embarqué, sûreté de fonctionnement, garanties temporelles, ordonnancement, certification

Model Driven Language Engineering using Kermeta

Équipe-Projet Inria : TRISKELL

Équipe-projet commune avec le CNRS, l'INSA de Rennes, l'université de Rennes 1

Résumé :  In many domains such as aerospace and automotive industries, engineers rely on Domain Specific Modeling Languages to solve the complex issues of engineering safety critical software. This tutorial aims at showing how Model Driven Engineering can help to easily obtain a complete environment for such a language, including interpreter, compiler, V&V tools, pretty-printer and customizable editors. We illustrate the conceptual simplicity and elegance of this approach using the running example of the well known LOGO programming language, developed within the Kermeta environment.

Mots clés :  model-based development, domain specific language, model driven engineering, executable modelling, V&V

Vérification de systèmes embarqués critiques avec CADP 2009

Équipe-Projet :  VASY

Résumé :  Le développement de systèmes embarqués critiques nécessite des outils permettant d'en assurer la fiabilité dès les premières phases de leur conception. La boîte à outils logiciels CADP permet la modélisation et la vérification formelle de ces systèmes. Nous illustrons l'utilisation de CADP dans le cadre de plusieurs études de cas avioniques.

Mots clés : Fiabilité, méthodes formelles, odel-checking, validation

Application Java Multitouch/Webserver/HRTJ sur cibles bas-coût

Société :  IS2T

Résumé : Capacités Multi-Touch sur ARM7-LPC2478 à 67Mhz ; Gestion des capteurs d'une carte à partir d'un serveur web embarqué sur AVR32 EVK1100 ; Mise en oeuvre des principes du HRT sur une machine virtuelle Java sur ARM9

Mots clés :  Multi-Touch, Java, HRTJ, DO178C, Web server

Haut de page

Suivez Inria