Master d’informatique 2008 2009
srsar
proposition de these (Toulouse)

L’équipe MACAO de l’Institut de Recherche en Informatique de Toulouse cherche des candidats d’excellence pour un sujet de thèse financé dans le domaine de l’ingénierie des modèles appliquée aux systèmes embarqués. Les candidats sont invités à envoyer un CV et lettres de recommandation, le plus rapidement possible à iulian.ober@irit.fr et bruel@irit.fr

Toutes nos excuses si vous recevez plusieurs fois ce mail.


Titre : Le raffinement dans la conception des systèmes embarqués : du système au logiciel/matériel

Directeurs de recherche :
Iulian Ober (http://www.irit.fr/ Iulian.Ober/ )
Jean-Michel Bruel ( http://jmb.c.la/ )

Description :

Les systèmes embarqués désignent des systèmes (aussi bien matériels que logiciels) intégrés dans un environnement applicatif particulier et chargés de réaliser des fonctions du type contrôle, monitoring, etc. Généralement temps réel, et communicants, ils sont souvent critiques pour le fonctionnement de l’environnement dans son ensemble. Les systèmes embarqués trouvent aujourd’hui des domaines d’application très variés : automobile, grille d’énergie, électronique grand public, aéronautique, spatial (les deux dernier domaines étant ceux qui nous intéressent plus particulièrement dans le cadre du pôle d’excellence AESE). Plus récemment, des nouveaux processus de fabrication de circuits intégrés ont rendu possibles la construction d’architectures complexes, comportant des processeurs spécialisés, de la mémoire, des contrôleurs et des périphériques fondus sur une même puce – l’on parle alors de systèmes sur puce (System-on-Chip).

Le cycle de développement généralement utilisé pour les systèmes embarqués, et en particulier les SoC, est un cycle en V, dont la phase de conception procède, à partir d’une architecture gros-grain dérivée directement des exigences du système, par décompositions et raffinements successifs pour arriver jusqu’au code des composants matériels ou logiciels (branche descendante du V), pour ensuite effectuer l’intégration des composants, avec à chaque pas des validations spécifiques (branche ascendante du V).

Le problème auquel font face les praticiens est l’absence d’un langage et d’une théorie unitaire leur permettant de modéliser le système aux différents niveaux de raffinement. Aujourd’hui, on peut exprimer en AADL l’architecture détaillée d’un système, en faisant apparaître les composants matériels et logiciels, les connexions, les flots, etc. mais le langage reste très limité pour capter les aspects fonctionnels des composants. Le langage SysML permet quant à lui de capter les aspects fonctionnels (par des diagrammes de blocs, d’états-transitions, etc.) mais sans support pour faire le lien avec l’architecture décrite en AADL. Enfin, lorsqu’une telle architecture doit être raffinée pour obtenir le code des composants matériels et logiciels (en VHDL, SystemC, Ada, SCADE, ou tout autre langage approprié), il est très difficile d’automatiser ou de valider le raffinement. Dans le cadre de cette thèse on se propose d’étudier cette problématique du passage du niveau système au niveau logiciel/matériel, en utilisant SysML comme langage pivot. Nous allons étudier les aspects méthodologiques de l’utilisation intégrée de modèles et niveaux d’abstraction variés. Nous nous intéressons au problème de combinaison des outils de simulation, d’animation et de preuves formelles, que chacune des communautés (informaticiens, systémistes) utilise ou développe de son côté. Enfin, nous nous intéressons à la formalisation de ce raffinement sous des angles précis, comme sa correction temporelle.

Contexte et pré-requis : La thèse s’inscrit dans plusieurs projets financés et labélisés AESE auxquels participe notre équipe, et se déroulera en collaboration avec des partenaires industriels et académiques. L’étudiant doit avoir des compétences dans le domaine de l’ingénierie des modèles et les méthodes formelles. Une rémunération est prévue.