Laboratoire: Verimag (http://www-verimag.imag.fr/)
Équipe: SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE)
Encadrants: David Monniaux <David.Monniaux@imag.fr>, Claire Maïza <Claire.Maiza@imag.fr>.
Contexte Scientifique
Dans les parties critiques des avions et des voitures, les programmes ne doivent pas seulement s’exécuter sans bug mais ils doivent aussi terminer leur exécution dans un temps imparti. Imaginez, par exemple, les dégâts causés si l’ABS ne réagissait pas à temps, ou si la sortie du train d’atterrissage n’était pas garantie avant l’atterrissage. Pour pouvoir garantir que les programmes s’exécutent suffisamment vite, il est primordial d’estimer une borne supérieure du temps d’exécution de ces programmes. Cette estimation du pire cas , worst case execution time (WCET) en anglais, doit être garantie supérieure ou égale à la borne supérieure réelle du temps d’exécution. Malheureusement, il n’est pas possible de mesurer cette borne car le nombre de cas à tester est bien trop important. Pour cette raison, l’estimation du temps d’exécution pire cas se fait de manière statique (sans exécuter le code).
Le model-checking est un ensemble de techniques permettant de vérifier qu’un système (par exemple un microprocesseur) respecte certaines propriétés. Des outils de model-checking très performants sont disponibles.
Sujet
- Comprendre les analyses temporelles de mémoires caches existantes et le principe du model-checking.
- Encoder le comportement des caches du processeur dans un outil de model-checking (SAT/SMT ou NuSMV) et en déduire des bornes de temps des informations ainsi calculées. Attention, les encodages naïfs seront probablement inefficaces, il faudra donc réfléchir à des techniques astucieuses.
Compétences Attendues
- De bonnes bases en algorithmique et en logique propositionnelle
- Des notions d’architecture
Contexte de Travail
Le stagiaire sera encadré par David Monniaux et Claire Maïza (permanents du laboratoire).
