Astrée

¿Qué es Astrée?

Astrée es un analizador de código estático que demuestra la ausencia de errores de tiempo de ejecución y un comportamiento concurrente no válido en el software de seguridad crítico escrito o generado en C.

Astrée se centra principalmente en aplicaciones integradas, como se encuentra en la aeronáutica, el transporte terrestre, la instrumentación médica, la energía nuclear y los vuelos espaciales. Sin embargo, también se puede usar para analizar cualquier programa C estructurado, escrito a mano o generado con usos complejos de memoria, asignación dinámica de memoria y recursión.

¿Qué propiedades del software Astrée?

Astrée analiza si el lenguaje de programación C se utiliza correctamente y si puede haber errores de tiempo de ejecución durante cualquier ejecución en cualquier entorno. Esto cubre cualquier uso de C que, de acuerdo con el estándar C99, se comporte indefinido o viole aspectos específicos del hardware.

Además, Astrée informa de un comportamiento simultáneo no válido, infracciones de las directrices de programación especificadas por el usuario y varias propiedades del programa relevantes para la seguridad funcional.

Astrée detecta

• División por cero,
• Indexación de matrices fuera de los límites,
• Manipulación incorrecta de punteros y referencias (NULL, sin inicializar y punteros pendientes),
• Exceso aritmético de enteros y coma flotante,
• Acceso de lectura a variables no inicializadas,
• Ejecuciones de datos (accesos simultáneos de lectura/escritura o escritura/escritura por dos subprocesos a la misma ubicación de memoria sin el bloqueo mutex adecuado),
• Bloqueo inconsistente (problemas de bloqueo/desbloqueo),
• Llamadas no válidas a servicios del sistema operativo (por ejemplo, llamadas OSEK a la tarea Terminar tarea con recursos no publicados),
• Infracción de aserciones opcionales definidas por el usuario para probar propiedades de tiempo de ejecución adicionales (similar a los diagnósticos de afirmación),
• El código puede resultar inaccesible bajo cualquier circunstancia.

Adáptalo a tus propias necesidades

Astrée ofrece potentes mecanismos de anotación para proporcionar conocimiento externo y mejorar la precisión del análisis para bucles individuales o estructuras de datos. Mensajes detallados y una GUI intuitiva que lo guía a la causa exacta de cada posible error de tiempo de ejecución. Los errores reales se pueden corregir y, en el caso de una falsa alarma, el analizador se puede ajustar para evitarlo. Esto permite el análisis con pocas o incluso cero falsas alarmas.

Requisitos de sistema

Windows: Windows 7 SP1 de 64 bits o posterior

Linux: CentOS / RHEL 6 de 64 bits o compatible

4 GB de RAM (se recomiendan 16 GB)

4 GB de espacio en disco