Nous travaillons sur le problème de la conception sûre de systèmes embarqués temps-réels. Les domaines d'application typpiques sont les systèmes à sûreté critique, tels que dans les transports (avionique, automobile, rail), la santé, les usines d'assemblage, et la production d'énergie. Les principales contraintes associées aux systèmes embarqués sont le temps d'exécution borné, l'empreinte mémoire bornée, la bande passante limitée, la tolérance aux fautes, la très haute fiabilité, et la puissance électrique limitée.

La conception et la mise en oeuvre correcte de systèmes embarqués à sûreté critique requiert à la fois des méthodes de conception formelles et des modèles formels, ainsi que leur mise en oeuvre dans des outils de conception assistée par ordinateur, dédiés aux spécialistes des domaines d'application. Nous contribuons à ce domaine en proposant des solutions tout au long de la chaîne de conception, de la spécification jusqu'à l'implémentation. Nous développons des techniques de spécification et de génération automatique de code embarqué pour systèmes embarqués à sûreté critiques, garantissant par construction des propriétés clés (telles que le temps d'exécution borné, l'absence d'inter-blocage, la tolérance aux fautes, ...). Nous développons aussi des techniques d'analyse statique afin de vérifier des propriétés additionnelles des systèmes générés. Nos axes de recherche spécifiques sont :

• Conception à base de composants. Les techniques de conception à base de composants sont cruciales pour surmonter la complexité des systèmes embarqués. Cependant, deux obstacles majeurs doivent être traités: la nature hétérogène des modèles et l'absence de résultats pour guarantir la correction du système composé. L'hétérogénéité provient du besoin d'intégrer des composants utilisant des modèles de calcul, de communication et d'exécution différents, à différents niveaux d'abstraction et à différentes échelles de temps. Le cadre BIP de conception à base de composants a été conçu, en collaboration avec VERIMAG, afin de supporter cette hétérogénéité. Nous nous concentrons sur les analyses sous-jacentes et sur les algorithmes de construction, en particulier sur les techniques compositionnelles et les approches permettant d'obtenir des garanties par construction (synthèse d'adapteurs, strategy mapping). Enfin, nous travaillons sur la conception à base de contrats, afin de raisonner formellement sur ce qu'un composant suppose de son environnement et sur ce qu'il garantit à propos de son propre comportement: nous proposons deux variantes de contrats, avec des modalités may-must et avec de probabilités.

• Programmation des systèmes embarqués. Nous attaquons ce problème avec une forte approche langage. Notre première contribution concerne les langages de programmation synchrone; en particulier, nous travaillons sur la répartition modulaire de Lucid Synchrone, sur l'extension dynamique du langage globalement asynchrone localement synchrone SystemJ, et sur l'exécution prédictive de PRET-C, une extension synchrone de C. Notre deuxième contribution concerne la programmation orientée-aspects, pour spécifier les propriétés non-fonctionnelles séparémment du programme principal; en particulier, nous travaillons sur la formalisation des catégories d'aspects. Notre troisième contribution concerne les méthodes d'analyse statique pour garantir, à la compilation, des propriétés se sûreté sur les programmes; en particulier, nous travaillons sur des systèmes de types et sur l'interprétation abstraite afin de vérifier des propriétés logico-numériques.

• Sûreté de fonctionnement. La sûreté de fonctionnement est une propriété cruciale que les systèmes embarqués critiques doivent satisfaire. Nous traitons deux questions liées à la sûreté de fonctionnement: la tolérance aux fautes et la fiabilité. Nous concevons des heuristiques multi-critères d'ordonnancement sur arhcitectures multi-processeurs, dans le but d'optimiser le temps d'exécution (période et latence), la fiabilité, et la puissance électrique consommée. Nous travaillons également sur des transformations automatiques de programmes (et, plus tard, sur le tissage d'aspects) afin de transformer un programme non tolérant aux fautes en un programme sémantiquement équivalent et tolérant aux fautes, basé sur les techniques de heartbeating et de point de reprise/retour arrière. Enfin, nous proposons un cadre de travail formel général, fondé sur la synthèse de contrôleurs discrets (à la Ramadge et Wonham), pour automatiser l'addition de la tolérance aux fautes.

Logiciels

• APRON
• NBAC

• Réseau d'excellence européen FP7 ARTIST-DESIGN sur les systèmes embarqués.
• Projet européen STREP FP7 COMBEST sur les techniques de conceptions à base de composants pour les systèmes embarqués.
• Projet européen Artemisia CESAR sur les méthodes et process efficace pour les systèmes embarqués à sûreté critique.
• Projet français ANR VEDECY sur la vérification et la conception de système cyber-physiques.
• Projet français ANR ASOPT sur l'analyse statique et l'optimisation.
• Projet français ANR AUTOCHEM sur la programmation efficace de la machine chimique.
• Projet sur pôle de compétivité Minalogic OpenTLM sur la programmation au niveau TLM de systèmes sur puces.
• Action d'envergure INRIA SYNCHRONICS sur une plateforme langage pour la conception des systèmes embarqués.
• Equipe associée INRIA AFMES sur les méthodes formelles avancées pour les systèmes embarqués, avec l'Université d'Auckland (Nouvelle Zélande).
• Contrats industriels avec ST Microelectronics et Dassault Systèmes.