Sites Inria

English version

Rencontres Inria - Industrie

Les industries de l'aéronautique et de l'espace - Partie 2 : Conférenciers

Au cours de cette journée vous avez pu assister aux exposés de plusieurs spécialistes du domaine de l'aéronautique et de l'espace. Ils vous ont présenté une synthèse des travaux menés pour Inria et ses partenaires autour de ce type d'activité.

Roberto di Cosmo : logiciel libre/ouvert : défis scientifiques et technologiques pour les systemes d'ingénierie complexe

Roberto Di Cosmo

Bio expresse :  Roberto Di Cosmo est professeur d'Informatique à l'université Paris Diderot, où il travaille sur les aspects formels des logiciels libres, en particulier dans le cadre du projet européen Mancoosi, qu'il coordonne; il a été le fondateur et premier président du Groupe Thématique Logiciel Libre du pôle de compétitivité Systematic; en délégation à l'institut depuis septembre 2009, il travaille à la création d'un centre de recherche et innovation en Informatique sur les Logiciels Libres.

Résumé de l'intervention :  L'essor des logiciels libres croît sans arrêt, et porte avec soi son lot de problèmes scientifiques nouveaux, auxquels il faut apporter rapidement une réponse en utilisant des résultats de la recherche fondamentale; dans cet exposé on présente deux "success stories" dans cette ligne : le projet Coccinelle et le projet Mancoosi. On abordera aussi les questions liées à l'impact que le Logiciel Libre a sur la formation d'ingénieurs en Informatique, et sur les modèles économiques industriels.

Mots clés :  logiciel Libre, systèmes complexes, ingénierie, génie logiciel, vérification, méthodes formelles.


Robert de Simone : modèles et code à la fois : bénéfices et exigences du temps logique multiforme pour la conception de systèmes temps réel embarqués critiques

Robert de Simone

Bio expresse : Robert de Simone est Directeur de Recherche Inria et responsable scientifique de l'équipe-projet Aoste. Ses principaux centres d’intérêt couvrent la Sémantique du Parallélisme (algèbres de processus, langages réactifs synchrones, vérification automatique et model-checking ), puis l'approche formelle de la conception de systèmes embarqués par l'Ingénierie des Modèles, et l'ordonnancement statique dans les Réseaux de Processus. Il a coordonné pour Inria de nombreux projets collaboratifs sur ces thèmes, dont certains ont mené au profil officiel OMG UML MARTE pour la modélisation et l'analyse de systèmes temps réel embarqués.

Résumé de l'intervention :  Le cycle de conception actuel des systèmes temps réel embarqués critiques s'appuie de plus en plus sur l'ingénierie des modèles. Ces derniers induisent fréquemment du parallélisme et de la concurrence tant au niveau des applications et des architectures d'exécution qu'au niveau des équipes de conception et de leur coopération. Ces modèles peuvent être d'une part exécutables pour permettre leur analyse par simulation, ils peuvent d'autre part être formels pour autoriser des analyses plus mathématiques. Ils sont rarement les deux à la fois. Nous allons illustrer comment l'approche fondée sur le temps multiforme et les les horloges logiques vise à réconcilier ces deux qualités (exécutable, formelle) et à les propager tout au long du cycle de conception.

Mots clés :  système embarqué, système critique, temp réel, ordonnancement, ingénierie des modèles, temps logique multiforme, calcul d'horloge.


Xavier Leroy : une introduction à la vérification formelle de codes critiques

Xavier Leroy

Bio expresse :  Xavier Leroy est directeur de recherche Inria et responsable scientifique de l'équipe-projet Inria Gallium. C'est l'un des principaux auteurs du langage fonctionnel de programmation OCaml. Il a également travaillé sur la sécurité logicielle, avec applications aux cartes à puces. Ses travaux en cours portent sur la preuve formelle de compilateurs et autres outils de vérification et de transformation de programmes.

Résumé de l'intervention :  Que faire lorsque le test ne suffit plus (ou devient trop coûteux) pour qualifier un logiciel critique? Une solution est la vérification formelle, assistée par des outils, des codes en question - une pratique qui commence à percer dans l'industrie aéronautique. Pour illustrer cette approche, je présenterai rapidement quelques outils de vérification, basés sur l'analyse statique ou sur la vérification déductive de programmes, et leurs utilisations dans l'aéronautique. J'aborderai ensuite le problème des compilateurs et autres générateurs automatiques de code : leur vérification formelle permet d'étendre au code exécutable les garanties obtenues par vérification du programme source.


Marc Pouzet : action d'Envergure Inria SYCHRONICS "Langages de programmation synchrones pour les systèmes embarqués"

Marc Pouzet

Bio expresse :  Marc Pouzet est Professeur d'Informatique à l'ENS. Il coordonne, avec Alain Girault, l'action d'envergure Inria Synchronics. Son activité de recherche porte sur la conception et l'implémentation de langages de programmation pour l'embarqué. Plusieurs de ses travaux sont intégrés à l'environnement industriel SCADE 6 développé par la société Esterel-Technologies.

Résumé de l'intervention :  L'exposé fera un point sur les développements menés dans l'action d'envergure Inria. Il détaillera les travaux en cours autour de ReactiveML qui marie les principes de la programmation fonctionnelle de Ocaml et de la programmation réactive à la Esterel.

Haut de page

Suivez Inria