Florence Maraninchi - Professional Home Page

Laurie Lugrin, Master II R, 2008-2009

Formal models for the modeling of energy consumption in embedded systems: abstractions and verification methods.

Co-supervisor: Laurent Mounier, VERIMAG/DCS

Dans la plupart des applications de type “système embarqué” il est nécessaire de garantir certaines contraintes dites non fonctionnelles. Ces contraintes peuvent concerner l’utilisation des ressources fournies au système, comme par exemple le temps de calcul, l’allocation de mémoire, ou encore l’énergie disponible. Ce dernier paramètre est notamment crucial pour des applications devant fonctionner de manière autonome pour une durée de vie minimale donnée. Ce type de propriété pose des problèmes nouveaux en termes de conception et de validation, en particulier car elles sont généralement le résultat d’une conception globale, qui repose sur un couplage fort entre les différents composants (matériels et logiciels) du système, et non uniquement sur des optimisations propres à chaque composant. Une approche réaliste en pratique est basée sur la notion de prototypage virtuel, qui consiste à s’appuyer sur un modèle comportemental du système, permettant ainsi d’évaluer au plus tôt la pertinence d’une solution proposée. Les techniques d’analyse employées reposent alors, soit sur de la simulation de certains scénarios d’exécution, soit sur une exploration exhaustive du modèle complet. Cette deuxième technique reste toutefois limitée à des systèmes peu complexes, pour lesquels la taille de ce modèle est raisonnable. Pour améliorer les performances de ces techniques d’analyses exhaustives, une solution attractive consiste à abstraire le comportement de certains composants du modèle, tout en préservant les propriétés étudiées (comme la durée de vie minimale du système global). Nous étudions cette approche au laboratoire Verimag, notamment pour des applications de type “réseaux de capteurs”. Nous avons pour cela défini un modèle comportemental prenant en compte la comsommation énergétique. Ce modèle est basé sur la notion d’automates étendus, dans lesquels des annotations sur les états permettent de décrire la puissance (“instantanée”) consommée . L’intégration par rappport au temps de ces puissances sur une séquence d’exécution complète fournit ainsi la consommation énergétique correspondante. Nous avons alors proposé une relation de préordre entre automates étendus qui capture cette notion d’abstraction en préservant la consomation énergétique au pire cas. Nous avons pu montrer que cette relation est une pré-congruence pour l’opérateur de composition synchrone. Cette propriété garantit que l’on peut remplacer un modèle de composant par un modèle plus abstrait, tout en préservant la durée de vie minimale du système global. L’objectif de ce stage est de poursuivre ce travail dans différentes directions. Sur le plan théorique il s’agit tout d’abord de définir une procédure de décision efficace pour cette relation de préordre, par exemple en utilisant des techniques symboliques de représentation de modèles (sans énumération explicite des ensembles d’états). De même il pourra être nécessaire de formaliser le raisonnement utilisé lors de l’application de cette technique d’abstraction, notamment en raison des dépendances croisées entre les composants. On pourra par exemple s’inspirer des approches de type “assume-guarantee”). Enfin, sur le plan pratique, des études de cas fournies dans le cadre du projet Aresa permettront de valider les solutions proposées.


Attached documents

Home page | Contact | Site Map | | Statistics | visits: 87593

Follow-up of the site's activity en  Follow-up of the site's activity Students  Follow-up of the site's activity Master Students   ?

Site created with SPIP 2.1.26 + AHUNTSIC

Creative Commons License