Latency verification in execution traces of HW/SW partitioning model

Vérification de la latence dans les traces d'exécution de modèle de partitionnement logiciel / matériel Alors que de nombreux travaux de recherche visent à définir de nouvelles techniques de vérification (formelle) pour vérifier les exigences dans un modèle, la compréhension de la cause profonde de la violation d'une exigence reste un problème ouvert pour les plateformes complexes construites autour de composants logiciels et matériels. Par exemple, la violation d'une exigence de latence est-elle due à un ordonnancement temps réel défavorable, à des conflits sur les bus, aux caractéristiques des algorithmes fonctionnels ou des composants matériels ? Cette thèse introduit une approche d'analyse précise de la latence appelée PLAN. PLAN prend en entrée une instance d'un modèle de partitionnement HW/SW, une trace d'exécution, et une contrainte de temps exprimée sous la forme suivante : la latence entre l'opérateur A et l'opérateur B doit être inférieure à une valeur de latence maximale. PLAN vérifie d'abord si la condition de latence est satisfaite. Si ce n'est pas le cas, l'intérêt principal de PLAN est de fournir la cause première de la non satisfaction en classant les transactions d'exécution en fonction de leur impact sur la latence : transaction obligatoire, transaction induisant une contention, transaction n'ayant aucun impact, etc. Une première version de PLAN suppose une exécution pour laquelle il existe une exécution unique de l'opérateur A et une exécution unique de l'opérateur B. Une seconde version de PLAN peut calculer, pour chaque opérateur A exécuté, l'opérateur B correspondant. Pour cela, notre approche s'appuie sur des techniques de tainting. La thèse formalise les deux versions de PLAN et les illustre par des exemples ludiques. Ensuite, nous montrons comment PLAN a été intégré dans un Framework Dirigé par le Modèle (TTool). Les deux versions de PLAN sont illustrées par deux études de cas tirées du projet H2020 AQUAS. En particulier, nous montrons comment l'altération peut traiter efficacement les multiples et occurrences concurrentes du même opérateur.