Outils d'analyse statique du code binaire
Calcul du pire temps d'exécution (WCET)
Outil : aiT
À quoi cela sert-il ?
1.
Il calcule des limites WCET très précises et peut être utilisé pour produire des preuves de certification de cet objectif.
2.
Il dispose d'un ensemble de qualifications, comme l'exigent les normes de sécurité fonctionnelle.
3.
Il détermine le chemin d'exécution avec le pire temps d'exécution et prend en compte les aspects de bas niveau tels que le pipeline et la mémoire cache du processeur utilisé. À cette fin, il utilise la méthode formelle"Interprétation abstraite" ainsi que des modèles formels de pipeline et de cache.
4.
Il ne nécessite que le code objet exécutable pour effectuer l'analyse, bien que si le code source est fourni, il est inclus dans le résultat avec le code d'assemblage généré.
5.
Il calcule le temps d'exécution de chacun des chemins d'un programme ou d'une tâche et marque en rouge le chemin critique correspondant au WCET.
6.
Il utilise des fichiers d'annotation relatifs à l'architecture du processeur, à la fréquence d'horloge et à d'autres paramètres nécessaires au calcul du temps d'exécution.
7.
Il permet de comparer graphiquement les résultats de différentes exécutions de l'outil afin de suivre l'évolution du WCET.
8.
Il peut être utilisé avec des générateurs de code d'outils de modélisation et des outils de planification au niveau du système via une API basée sur XML.
9.
Cependant, les processeurs multicœurs actuels ont un niveau de complexité qui rend difficile l'analyse des effets de pipeline et de cache dans des environnements d'exécution complexes où différents cœurs interagissent les uns avec les autres. L'interférence entre les cœurs ne peut pas être modélisée formellement dans le cadre de l'aiT.
10.
Pour les processeurs multicœurs, l'outil TimeWeaver est nécessaire.
Familles de processeurs et de compilateurs prises en charge
- Compilateur ARM
- Compilateur GCC
- Diab C ou Ada
- Green Hills C/C++ ou Ada
- IAR
- Keil ARM
- HighTec LLVM/Clang
- Tâches
- Texas Instruments
- CompCert (INRIA, AbsInt)
- Diab C
- Green Hills C/C
- Compilateur GCC
- Diab C
- Green Hills C/C++ ou Ada
- HighTec GCC
- Tâches
- Compilateur Code Warrior
- Compilateur GCC
- GNAT Pro C++ ou Ada
- Diab C ou Ada
- Green Hills C/C++ ou Ada
- HighTec GCC
- Keil ARM
- CompCert (INRIA, AbsInt)
- Compilateur GCC
- GNAT Pro C++ ou Ada
- Diab C ou Ada
- Green Hills C/C++ ou Ada
- HighTec GCC
- Keil ARM
- CompCert (INRIA, AbsInt)
Autres transformateurs
- ERC32
- Leon2, Leon3
- Am486, IntelDX4
- i386DX
- C16x, ST10
- HCS 12
- C28X
- C33
- M68020, MCF5307, M68020, MCF5307
