Astrée
Herramienta de análisis estático de código fuente:
Detección de errores en tiempo de ejecución y errores de concurrencia
Cinco razones para elegir Astrée
Astrée es una herramienta de gama alta, basada en métodos formales, que garantiza que cuando no detecta errores de ejecución, la aplicación realmente no tiene errores de ejecución.
A día de hoy, únicamente existen dos herramientas en el mercado, basadas en métodos formales, que puedan dar esta garantía.
1. Funciona
Funciona para aplicaciones escritas en lenguaje C.
2. Detecta
- Errores de concurrencia en el sistema operativo OSEK y perfil ARINC 653.
- Errores de división por cero.
- Errores de acceso a arrays fuera de rango.
- Manipulaciones de punteros erróneas.
- Desbordamientos de variables de tipo entero y punto flotante.
- Errores de redondeo en cálculos de punto flotante.
- Accesos a variables no inicializadas.
- Accesos concurrentes problemáticos a variables compartidas por varios procesos.
- Errores de inconsistencia de bloqueo de variables.
3. Permite
- Permite el diagnóstico de aserciones definidas por el usuario para probar propiedades adicionales en tiempo de ejecución.
- Permite probar qué porciones de código no son ejecutables bajo ninguna circunstancia (detección de código muerto).
4. Chequea
Chequea el código fuente conforme a las siguientes normas de codificación software:
- MISRA C (2004 y 2012, incluyendo Amendment 1)
- Lenguaje C99 (Anexo J de ISO/IEC 9899:1999)
- CWE (CCR accuracies Exact, CWE-more-abstract y CWE-more-specific)
- SEI CERT C
- ISO/IEC TS 17961:2012
5. Además...
- Tiene interfaz IDE y por línea de comandos, permitiendo la ejecución en batch para facilitar las pruebas de regresión.
- Tiene integraciones con Jenkins, SCADE, TargetLink (dSPACE), SymtaVision y RT-Druid.
- Tiene un Paquete de Certificación para DO-178, ISO 26262, EN-50128 y FDA.
