Accueil > Axes > FETLAS > Emplois et stages

[Master 2R 2014-2015] Évaluation de performances pour les systèmes embarqués avec des méthodes formelles

Sommaire

Contexte Scientifique

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.

Ils doivent être fiables, non-seulement au niveau de la fonctionnalité (i.e. calculer le résultat attendu), mais aussi en terme de performances (i.e. calculer le résultat dans les temps). Pour ces systèmes dits « temps-réel », il n’est pas suffisant d’optimiser le code pour obtenir des performances rapides, mais il faut également être capable de donner des bornes sur les temps d’exécutions.

Pour des applications multimédia, par exemple, il est important d’assurer qu’une application puisse encoder/décoder un flux à la vitesse à laquelle il est reçu. Plus important : dans les systèmes critiques (automobile, aviation, ...), rater une échéance (deadline) peut causer des dégâts importants, donc il est nécessaire d’avoir des garanties formelles sur les temps d’exécution. Par ailleurs, ces systèmes sont souvent contraints en mémoire, donc des files d’attentes (buffers) non-bornées ne peuvent pas être utilisées pour faire communiquer les composants d’un système. Par exemple, dans une application flot de donnée typique comme un encodeur JPEG, si un bloc (par exemple, le bloc DCT) fournit une grande quantité de données sur une période de temps réduite (i.e. une rafale), alors le bloc de traitement suivant (la quantification dans notre exemple) ne pourra pas les traiter immédiatement et les données vont devoir être stockées dans une file d’attente, de taille limitée. La taille de la file d’attente dépend de la vitesse à laquelle les données sont produites, et de celle à laquelle elles vont pouvoir être consommées.

Étant données le cycle de vie court dû à la pression du « time-to-market » dans l’industrie, 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 représentation plus abstraite du système) le plus tôt possible dans le flot de conception. Pour utiliser ces modèles pour valider des systèmes temps-réels, plusieurs approches sont possibles :

Simulation. Les modèles les plus fins sont exprimés comme des programmes, écrits dans des langages de programmations usuels comme C ou C++ (et éventuellement des bibliothèques comme SystemC). Ces programmes peuvent être exécutés pour simuler le comportement complet du système, et obtenir des informations sur les performances. Comme pour le test, ces méthodes permettent d’avoir une bonne confiance dans les résultats, mais pas de garantie formelle.

Méthodes formelles et exploration de l’espace d’état. Une alternative aux langages de programmation usuels est l’utilisation de langages formels (comme Lustre, Uppaal, …), qui décrivent essentiellement des machines d’états. Ces langages sont en général moins expressifs que les langages de programmation usuels, mais permettent des raisonnements formels et l’exploration exhaustive de l’espace d’état. Par exemple, le model-checking ou l’interprétation abstraite peuvent être utilisés pour vérifier formellement et automatiquement des propriétés comme « le système ne prendra jamais plus de X unités de temps pour traiter un événement ». Ces analyses fournissent des garanties fortes, mais se heurtent au problème de l’explosion d’états sur des systèmes de grande taille : l’analyse peut prendre un temps et une quantité de mémoire déraisonnable, et ne peut pas toujours être appliquée telle quelle en pratique.

Analyse de performance modulaire (Modular Performance Analysis) et Calcul Temps-Réel (Real-Time Calculus). Une solution au problème d’explosion d’états est de réaliser l’analyse sur des petites portions du système (i.e. les composants) un par un. Cette catégorie d’approches est appelée « analyse compositionnelle », ou « analyse modulaire ». Une approche existante est le « Real-Time Calculus » (RTC), qui représente les interfaces des composants avec des courbes. Les composants simples peuvent être analysés avec des méthodes analytiques (i.e. en résolvant des équations mathématiques avec des algorithmes efficaces) et les composants plus complexes peuvent être analysés avec les techniques d’interprétation abstraite et de model-checking mentionnées plus haut. Des études de cas préliminaires réalisées à Verimag et dans d’autres laboratoires comme l’ETH de Zurich ont montré que cette approche était à la fois intéressante et limitée par la faible expressivité de RTC.

Sujet

Le but du projet est de rechercher une nouvelle approche d’analyse de performance modulaire. Cette analyse devra fournir des bornes formelles sur les performances du système (délai maximum de bout en bout, taille maximum des files d’attentes, etc.). Au lieu de décrire les interfaces des composants avec des courbes, on utilisera un formalise basé sur la notion d’état (automate à compteur, ou éventuellement automates temporisés).

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. Les exemples pourront inclure des études de cas existantes comme le système à 2 processeurs et 3 tâches publié dans Emsoft09, ou l’étude de cas FlexRay (utilisé dans l’automobile) publié dans DAC07 et EUC2010.

Le travail attendu inclut une bibliographie sur la modélisation de systèmes 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 sujets 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 !