Analyse comparative de l'évolutivité de la détection des anomalies de synchronisation basée sur un vérificateur de modèles H/F

Candidater

Le laboratoire LECA a développé un cadre [3, 4] pour identifier les anomalies temporelles (AT) au sein des programmes. Ce cadre est construit sur un modèle formel d'un pipeline de processeur représentatif Out-of-Order (OoO) décrit à l'aide du langage de haut niveau TLA+ [5]. Les spécifications du programme sont générées à partir des codes sources C d'entrée en utilisant la sortie du simulateur gem5 [6]. Des variations temporelles locales sont introduites grâce à des heuristiques ciblant les latences des instructions mémoire. Par la suite, les TA sont exprimées sous forme d'hyper-propriétés dans TLA+ et formellement vérifiées à l'aide du vérificateur de modèle TLC sur un modèle formel combiné du pipeline et d'un programme. Ce flux de travail basé sur un vérificateur de modèles s'est avéré efficace dans la détection des TA à l'aide des tests TACLe [7], mais pour un nombre limité d'instructions et de variations d'accès à la mémoire. Un premier objectif de ce stage est d'évaluer l'évolutivité de ce workflow, notamment pour identifier la durée de vie des TA mais aussi leurs schémas. Cela implique d'incorporer la notion de blocs de base, l'unité d'analyse atomique dans les analyses statiques WCET, dans la spécification formelle du programme. Cette amélioration permettra d'étudier si les TA peuvent se propager sur plusieurs blocs de base et aidera à capturer les limites du flux de travail. Ces évaluations seront effectuées sur un nombre plus élevé de codes sources des benchmarks TACLe que celui actuellement pris en charge. Un autre objectif de ce stage est ensuite d'étudier comment l'évolutivité de ce workflow peut être optimisée. Cela peut impliquer d'utiliser les résultats des analyses de cache WCET pour affiner l'ensemble des variations de latence, d'ajuster l'instant de vérification pour la détection TA, ou d'explorer l'utilisation de différents vérificateurs de modèles, tels que le vérificateur de modèle symbolique Apalache pour TLA+ [8] .

Étudiant en ingénierie informatique (dernière année) ou étudiant en master 2 avec des connaissances en architecture informatique, et méthodes formelles, notamment model verify. Compétences en communication et en rédaction, motivation pour le travail en équipe et désireux d'apprendre.

Médias associés

fr_FRFR

Contact us

We will reply as soon as possible...