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).Industrial Perspective on Static Analysis. Software Engineering Journal Mar. 1995: 69-75Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf 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.Software Quality Objectives for Source Code. Proceedings Embedded Real Time Software and Systems 2010 Conference, ERTS2, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf
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.Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 "Static Techniques for Security," Stanford doctoral thesis, 2006. http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf 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:
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. 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.Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, http://webarchive.nationalarchives.gov.uk/20080731135436/http://www.hse.gov.uk/foi/internalops/nsd/tech_asst_guides/tast046app1.htm
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.
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
Referencias
Bibliografía Syllabus and readings for Alex Aiken’s Stanford CS295 course. Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, "Using Static Analysis to Find Bugs," IEEE Software, vol. 25, no. 5, pp. 22–29, Sep./Oct. 2008,
"Abstract interpretation and static analysis," International Winter School on Semantics and Applications 2003, by David A. Schmidt
Enlaces externos The SAMATE Project
Code Quality Improvement - Coding standards conformance checking (DDJ) Episode 59: Static Code Analysis entrevista (Podcast) en Software Engineering Radio Implementing Automated Governance for Coding Standards .NET Static Analysis (InfoQ)
Categoría:Análisis de software