Inria
Inria.fr
Inria Channel
Showroom des démos
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 :
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 :
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 :
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 :
Showroom des démos
TimeSquare : Spécifications Fonctionnelles à base de Temps Logique en Ingénierie des Modèles
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 :
Showroom des démos
Un processus de développement durable : l'expérience ATL
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 :
Edition de logiciels, systèmes embarqués
Cappucino : exploiter l'intelligence ambiante depuis la conception jusqu'à l'exécution des logiciels
Le projet montre comment un logiciel de vente en ligne est construit, déployé puis exécuté sur un téléphone. La ligne de production de logiciels et la plateforme d'exécution ont la particularité d'être sensibles au contexte. De plus, la plateforme CAPPUCINO est capable d'adapter le logiciel à chaud en fonction de l'évolution de l'environnement de l'utilisateur.»
Mots-clés :
Edition de logiciels, systèmes embarqués
Colivad : modélisation et optimisation de la chaîne logistique
La chaîne logistique globale consiste en l'optimisation des flux à tous les stades de la chaîne Fournisseur-Client : production, approvisionnement, stockage, distribution. Notre équipe s'intéresse aux méthodes d'optimisation appliquées à la chaîne logistique, au niveau opérationnel comme stratégique. Dans le projet COLIVAD, nous avons mis au point un outil d'optimisation pour la livraison de colis qui prend en compte les ressources propres à l'entreprise et à la sous-traitance.
Mots-clés :
Contact sectoriel
Vous êtes entrepreneur ? Industriel ? Vous souhaitez collaborer avec l'une de nos équipes de recherche ? Contactez notre responsable sectoriel édition de logiciels, systèmes embarqués.
Thierry Vareine
Tél. : + 33 1 39 63 51 77
