Análisis estático de software es un tipo de análisis de software que se realiza sin ejecutar el programa (el análisis realizado sobre los programas en ejecución se conoce como análisis dinámico de software).^[1]​ En la mayoría de los casos, el análisis se realiza en alguna versión del código fuente y en otros casos se realiza en el código objeto. El término se aplica generalmente a los análisis realizados por una herramienta automática, el análisis realizado por un humano es llamado comprensión de programas (o entendimiento de programas) como también revisión de código.

Motivación

La sofisticación de los análisis realizados por las herramientas varía de aquellos que sólo tienen en cuenta el comportamiento de instrucciones y declaraciones individuales, a los que se incluye el código fuente completo de un programa en su análisis. Los usos de la información obtenida de un análisis varían desde indicar posibles errores de codificación hasta demostrar matemáticamente con métodos formales ciertas propiedades acerca de un programa dado (por ejemplo, que su comportamiento coincide con el de su especificación) dependiendo de que programa se utilice para el análisis.

Las métricas del software y la ingeniería inversa pueden ser descritas como forma de análisis estático de software. El análisis estático y las métricas del software se han comenzado a desarrollar a la par, sobre todo en sistemas embebidos donde se definen lo que se llama objetivos del software de calidad.^[2]​

Un uso comercial creciente del análisis estático es la verificación de las propiedades de software utilizadas en los sistemas informáticos críticos para la seguridad y la localización de código potencialmente vulnerable.^[3]​ Por ejemplo las siguientes industrias han identificado el uso de análisis de código estático como un medio de mejorar la calidad de software cada vez más sofisticado y complejo:

1. Software médico: La Administración de Alimentos y Medicamentos (FDA) de Estados Unidos ha identificado al análisis estático como un servicio médico.^[4]​
2. Software nuclear: En el Reino Unido el Ejecutivo de Salud y Seguridad recomendó el uso de análisis estático para los sistemas de protección de reactores.^[5]​

En 2012, un estudio de VDC Research informó que el 28,7% de los ingenieros de software de sistemas embebidos encuestados utilizaban herramientas de análisis estático y que un 39,7% esperaban utilizarlas próximamente.^[6]​

Herramientas

Métodos formales

Los métodos formales es un análisis de software (y hardware), cuyos resultados se obtienen exclusivamente mediante el uso de métodos matemáticos rigurosos. Las técnicas matemáticas utilizadas incluyen semántica formal, semántica axiomática, semántica operacional e interpretación abstracta.

Por una simplificación del problema de la parada es posible probar que (para cualquier lenguaje turing completo) encontrar todos los posibles errores en tiempo de ejecución de un programa arbitrario (o más generalmente, cualquier tipo de violación de especificación en el programa final) es indecidible: no existe un método mecánico que siempre pueda contestar con la verdad si un determinado programa puede o no tener errores de ejecución. Este resultado se remonta a los trabajos de Alonzo Church, Kurt Gödel y Alan Turing de 1930 (Problema de la parada y teorema de Rice). Al igual que con muchas cuestiones indecidibles, todavía se puede intentar dar soluciones útiles aproximados.

Algunas de las técnicas de análisis estático formal incluyen:

• Model checking
• Interpretación abstracta
• Uso de aserciones en el código del programa, fue sugerido por la lógica de Hoare

Tipos de análisis estáticos

• Análisis de alias
• Análisis de punteros
• Análisis de figuras
• Análisis de escape
• Análisis de acceso a vectores
• Análisis de dependencia
• Análisis de control del flujo
• Análisis de flujo de datos
• Análisis de variable viva
• Análisis de expresiones disponibles
• Análisis de uso definido de cadena

Véase también

• Análisis de software
• Revisión de código
• Métrica del software
• Generador de documentación
• Verificación formal