Amphi H, Ensimag
13 mars 2014 - 14h00
High-level Models for Embedded Systems (HDR)
par Matthieu Moy de Verimag
Résumé : Les systèmes embarqués modernes ont atteint un niveau de complexité
qui fait qu'il n'est plus possible d'attendre les premiers
prototypes physiques pour valider les décisions sur l'intégration
des composants matériels et logiciels. Il est donc nécessaire
d'utiliser des modèles, tôt dans le flot de conception.
Les travaux présentés dans ce document contribuent à l'état de l'art
dans plusieurs domaines.
Nous présentons dans un premier temps de nouvelles techniques de
vérification de programmes écrits dans des langages généralistes
comme C, C++ ou Java.
Dans un second temps, nous utilisons des outils de vérification
formelle sur des modèles écrits en SystemC au niveau transaction
(TLM). Plusieurs approches sont présentées, la plupart d'entre elles
utilisent des techniques de compilations spécifiques à SystemC pour
transformer le programme SystemC en un format utilisable par les
outils.
La seconde partie du document s'intéresse aux propriétés
non-fonctionnelles des modèles~: performances temporelles, consommation
électrique et température. Dans le contexte de la modélisation TLM,
nous proposons plusieurs techniques pour enrichir des modèles
fonctionnels avec des informations non-fonctionnelles.
Enfin, nous présentons les contributions faites à l'analyse de
performance modulaire (MPA) avec le calcul temps-réel (RTC). Nous
proposons plusieurs connections entre ces modèles analytiques et des
formalismes plus expressifs comme les automates temporisés et le
langage de programmation Lustre. Ces connexion posent le problème
théorique de la causalité, qui est formellement défini et résolu
avec un algorithme nouveau dit de « fermeture causale ».
Composition du jury :
- Gérard Berry (Professeur au Collège de France), Rapporteur
- Rolf Drechsler (Professeur à l'Université de Brême, Allemagne), Rapporteur
- Marco Roveri (Senior Researcher, Fondazione Bruno Kessler, Italie), Rapporteur
- Samarjit Chakraborty (Professeur à l'université technique de Munich, Allemagne), Examinateur
- Benoît Dupont de Dinechin (Directeur Technique, Kalray, France), Examinateur
- Frédéric Pétrot (Professeur à Grenoble INP, France), Examinateur
