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.
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:
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]
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: