Performances des systèmes embarqués : entre simulation informatique
et solution mathématique
4 Sujets de master II recherche / master1, 2010-2011, laboratoire Verimag
Contexte scientifique :
Contexte général. La conception des systèmes embarqués modernes
doit répondre à des exigences croissantes dans plusieurs domaines :
les systèmes sont de plus en plus complexes, mais doivent être
fabriqués à bas coût, et avec un cycle de développement de plus en
plus court.
Dans un tel contexte, il n'est plus possible d'attendre les premiers
prototypes physiques pour valider les décisions sur la conception d'un
système, il est nécessaire de passer par des modèles (une
repésentation plus abstraite du système) le plus tôt possible dans le
flot de conception.
Nous nous intéressons ici à l'étude des performances (temps de calcul,
et éventuellement énergie consommée) sur des modèles de systèmes
embarqués.
Approche par simulation. Le laboratoire a déjà une grande
expérience dans l'étude de modèles très fins, exprimés comme des
programmes que l'on peut exécuter pour simuler la totalité de la
fonctionnalité d'un système et en obtenir des informations de
performances.
Approche analytique. D'un autre côté, il existe des modèles
purement analytiques basés sur des équations mathématiques que l'on
peut résoudre. Ces modèles permettent de représenter assez simplement
une quantité d'événements à traiter et la vitesse à laquelle le
traitement s'effectue. La résolution des équations donne par exemple
les meilleur cas et pire cas possibles sur les performances.
L'approche qui nous intéresse et qui relève de ce type de modèles
s'appelle le « Real-Time Calculus » ou RTC. Elle
permet de
caractériser, en fonction de courbes représentant le flot des arrivées
sur le système, une courbe du flot des sorties. Le gros intérêt de RTC
est que pour des composants suffisamment simples, on est capable de
caractériser de manière exacte et simple les flots de sortie en
fonction des flots d'entrées. Par contre, les composants plus
complexes ne sont pas modélisables directement en RTC, et il faut donc
trouver un moyen d'utiliser d'autres techniques pour ces composants.
Combinaisons des deux approches. Nous avons commencé des
recherches sur l'utilisation de techniques classiques de vérification
formelle (interprétation abstraite, model-checking) appliquées à des
systèmes décrits en RTC. Nous disposons déjà des fondements théoriques
et d'un prototype, permettant de décrire les modèles et les objets
mathématiques issus du RTC à l'aide du langage Lustre en vue de les
analyser.
Sujets proposés dans la continuité de ces travaux :
1) Nous avons caractérisé pour les courbes RTC une forme canonique dite
"causale" : pour pouvoir jutifier notre approche, les courbes
considérées doivent être causales. Nous savons transformer
(algorithmiquement) certaines représentations de courbes simples. Il
faut maintenant étendre ces algorithmes pour pouvoir manipuler des
représentations de courbes plus complexes et adapter la chaîne d'outils
en conséquence.
2) L'analyse de performances est réalisée par connexion à des outils
d'interprétation abstraite et de model-checking. Le temps pris par
l'analyse est souvent critique, mais corrélé aux outils : nous
souhaitons utiliser un nouvel outil d'interprétation abstraite plus
adapté aux courbes RTC, nous pensons qu'il sera plus efficace et
peut-être plus précis. Ce travail n'est pas simplement une question
d'outillage, il faudra surtout adapter les modèles et les propriétés à
analyser.
3) Une approche similaire a été conduite par une équipe de l'ETH
Zurich, avec laquelle nous sommes en contact. Ils modélisent le système
à évaluer et les courbes RTC à l'aide d'automates temporisés, puis
analysent le tout à l'aide d'un outil de model-checking. Les premiers
tests que nous avons conduits montrent que les deux approches ne sont
pas directement comparables : il faudrait réaliser une étude de cas qui
permette de comparer les deux approches, afin d'observer sur quels
critères l'une ou l'autres approches est performantes.
4) Le formalisme RTC ne permet pas de modéliser des composants un peu.
Les travaux précédents visent à étendre ce formalisme en établissant
des passerelles avec des méthodes formelles (model-checking,
interprétation abstraite). Une autre piste, que nous avons commencé à
explorer, est de changer de formalisme en proposant de nouvelles
abstractions pour décrire les flots d'événements. Ce sujet se divise en
trois étapes :
- Définir un formalisme, basé sur la notion d'automates,
permettant de représenter une abstraction de flot d'événements.
-
Définir la manière de calculer l'abstraction d'un flot produit par un
module, à partir des informations sur ses entrées, et d'un modèle de
son comportement.
- Implémenter ces algorithmes et les appliquer sur
plusieurs exemples.
Dans tous les sujets, le travail attendu inclut une bibliographie sur
la modélisation de système embarqués en vue d'étudier leurs
performances (modèles simulables, RTC), des expérimentations concrètes
(donc une implémentation des algorithmes), et une comparaison de
l'approche avec RTC.
Ces sujet font un pont entre la programmation en vue de simulation de
systèmes embarqués et l'étude formelle de modèles pour ces mêmes
systèmes. Ils comportent des points théoriques et pratiques ; ils sont
adaptables fonction des motivations de l'étudiant. N'hesitez pas a
venir en discuter !
Contexte de travail :
L'étudiant s'intègrera au sein des recherches en cours sur le sujet
dans l'équipe SYNCHRONE du laboratoire Verimag.
Poursuite en thèse sur un sujet connexe possible.
Responsables :
Karine Altisen, Matthieu Moy