Inria
Inria.fr
Inria Channel
PrécédentShowroom des démos
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 :
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 :
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
Optimisation de la planification des opérations
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.
Mots-clés :
Showroom des démos
Vérification des contraintes temporelles dans les systèmes embarqués critiques
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 :
Showroom des démos
Model Driven Language Engineering using Kermeta
Dans de nombreux secteurs tels que l’industrie aérospatiale et automobile, les ingénieurs s’appuient sur les langages de modélisation dédiés afin de résoudre les problèmes posés par le développement de logiciels critiques. Ce tutoriel a pour objectif de démontrer de quelle manière l’ingénierie dirigée par les modèles peut contribuer à l’obtention aisée d’un environnement complet adapté à un tel langage, y compris l’interprète, le compilateur, les outils de vérification et de validation, le programme de pretty-print (mise en forme), ou encore les éditeurs personnalisables. Nous illustrerons l'élégance et la simplicité conceptuelles de cette approche en nous appuyant sur l’exemple récurrent du célèbre langage de programmation LOGO, développé dans l’environnement Kermeta.
Mots-clés :
Showroom des démos
Vérification de systèmes embarqués critiques avec CADP 2009
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 :
Contact sectoriel
Vous êtes entrepreneur ? Industriel ? Vous souhaitez collaborer avec l'une de nos équipes de recherche ? Contactez notre responsable sectoriel aéronautique, défense, spatial, sécurité.
Brigitte Duême
Tél. : +33 1 39 63 53 04
