Herramientas de Análisis Estático de Código Binario
Cálculo de Worst Case Execution Time (WCET)
Herramienta: aiT
¿Para qué sirve?
1.
Calcula límites de WCET muy precisos y puede ser utilizada para generar evidencias de certificación de este objetivo.
2.
Cuenta con un paquete de cualificación conforme a lo requerido por los estándares de seguridad funcional.
3.
Determina el camino de ejecución con el peor tiempo de ejecución y tiene en cuenta los aspectos de bajo nivel como pipeline y cache del procesador concreto usado. Para ello, utiliza el método formal “Abstract Interpretation” junto con modelos formales de pipeline y cache.
4.
Requiere únicamente el código objeto ejecutable para realizar el análisis, aunque si se proporciona el código fuente se incluye en el resultado junto con el código ensamblador generado.
5.
Calcula el tiempo de ejecución de cada uno de los caminos de un programa o tarea y marca en rojo el camino crítico correspondiente al WCET.
6.
Utiliza unos ficheros de anotaciones relativos a la arquitectura del procesador, frecuencia de reloj y otros parámetros requeridos para el cálculo del tiempo de ejecución.
7.
Permite comparar gráficamente el resultado de diferentes ejecuciones de la herramienta para monitorizar la evolución del WCET.
8.
Puede ser utilizada con generadores de código de herramientas de modelado y con herramientas de planificación a nivel de sistemas mediante un API basada en XML.
9.
Sin embargo, los procesadores multi-core actuales tienen un nivel de complejidad que dificulta el análisis de los efectos de pipeline y cache en ámbitos de ejecución complejos donde los distintos cores interactúan entre ellos. La interferencia entre cores no puede ser modelada formalmente dentro de aiT.
10.
Para procesadores multi-core se requiere la herramienta TimeWeaver.
Familias de Procesadores y Compiladores Soportados
- ARM Compiler
- GCC Compiler
- Diab C or Ada
- Green Hills C/C++ or Ada
- IAR
- Keil ARM
- HighTec LLVM/Clang
- Tasking
- Texas Instruments
- CompCert (INRIA, AbsInt)
- Diab C
- Green Hills C/C
- GCC Compiler
- Diab C
- Green Hills C/C++ or Ada
- HighTec GCC
- Tasking
• Code Warrior Compiler
• GCC Compiler
• GNAT Pro C++ or Ada
• Diab C or Ada
• Green Hills C/C++ or Ada
• HighTec GCC
• Keil ARM
• CompCert (INRIA, AbsInt)
• GCC Compiler
• GNAT Pro C++ or Ada
• Diab C or Ada
• Green Hills C/C++ or Ada
• HighTec GCC
• Keil ARM
• CompCert (INRIA, AbsInt)
Otros procesadores
- ERC32
- Leon2, Leon3
- Am486, IntelDX4
- i386DX
- C16x, ST10
- HCS 12
- C28X
- C33
- M68020, MCF5307
