Statische Binärcode-Analyse-Tools
Berechnung der Worst-Case-Ausführungszeit (WCET)
Werkzeug: aiT
Wozu dient es?
1.
Es berechnet sehr genaue WCET-Grenzwerte und kann zum Nachweis der Zertifizierung dieses Ziels verwendet werden.
2.
Es verfügt über ein Qualifizierungspaket, wie es die Normen für funktionale Sicherheit vorschreiben.
3.
Es ermittelt den Ausführungspfad mit der schlechtesten Ausführungszeit und berücksichtigt dabei Low-Level-Aspekte wie Pipeline und Cache des jeweils verwendeten Prozessors. Zu diesem Zweck verwendet es die formale Methode"Abstrakte Interpretation" zusammen mit formalen Pipeline- und Cachemodellen.
4.
Für die Analyse wird nur der ausführbare Objektcode benötigt. Wenn der Quellcode zur Verfügung gestellt wird, ist er zusammen mit dem generierten Assemblercode in der Ausgabe enthalten.
5.
Sie berechnet die Ausführungszeit jedes Pfades eines Programms oder einer Aufgabe und markiert den kritischen Pfad, der der WCET entspricht, rot.
6.
Es verwendet Anmerkungsdateien, die sich auf die Prozessorarchitektur, die Taktfrequenz und andere für die Berechnung der Ausführungszeit erforderliche Parameter beziehen.
7.
Es ermöglicht einen grafischen Vergleich der Ergebnisse verschiedener Durchläufe des Tools, um die Entwicklung der WCET zu überwachen.
8.
Es kann über eine XML-basierte API mit Codegeneratoren von Modellierungswerkzeugen und Planungswerkzeugen auf Systemebene verwendet werden.
9.
Die heutigen Mehrkernprozessoren sind jedoch so komplex, dass es schwierig ist, Pipeline- und Cache-Effekte in komplexen Ausführungsumgebungen zu analysieren, in denen verschiedene Kerne miteinander interagieren. Die Interferenz zwischen den Kernen kann in aiT nicht formal modelliert werden.
10.
Für Multi-Core-Prozessoren ist das Tool TimeWeaver erforderlich.
Unterstützte Prozessorfamilien und Compiler
- ARM-Compiler
- GCC-Compiler
- Diab C oder Ada
- Green Hills C/C++ oder Ada
- IAR
- Keil ARM
- HighTec LLVM/Clang
- Aufgabenstellung
- Texas Instrumente
- CompCert (INRIA, AbsInt)
- Diab C
- Grüne Hügel C/C
- GCC-Compiler
- Diab C
- Green Hills C/C++ oder Ada
- HighTec GCC
- Aufgabenstellung
- Code Warrior Compiler
- GCC Compiler
- GNAT Pro C++ oder Ada
- Diab C oder Ada
- Grünhügel C/C++ oder Ada
- HighTec GCC
- Keil ARM
- CompCert (INRIA, AbsInt)
- GCC Compiler
- GNAT Pro C++ oder Ada
- Diab C oder Ada
- Grünhügel C/C++ oder Ada
- HighTec GCC
- Keil ARM
- CompCert (INRIA, AbsInt)
Andere Verarbeiter
- ERC32
- Leon2, Leon3
- Am486, IntelDX4
- i386DX
- C16x, ST10
- HCS 12
- C28X
- C33
- M68020, MCF5307, M68020, MCF5307
