Hispanopedia WikiECLAIR es una herramienta comercial de análisis estático de código desarrollada por BUGSENG para el análisis, la verificación, las pruebas y la transformación automáticas de programas en C y C++ .
Capacidades
ECLAIR es una reingeniería completa de una serie de prototipos [ 2 ] desarrollados en el Laboratorio de Métodos Formales Aplicados de la Universidad de Parma . Utiliza técnicas de análisis de código estático basadas en métodos formales, como la interpretación abstracta y la verificación de modelos, combinadas con técnicas de satisfacción de restricciones para detectar o demostrar la ausencia de ciertos errores de tiempo de ejecución en el código fuente , y proporciona soporte para el análisis y la verificación de programas, la generación de pruebas de programas y la transformación de programas.
En cuanto al análisis y verificación de programas, ECLAIR puede detectar estáticamente o demostrar la ausencia de anomalías en tiempo de ejecución, así como comprobar automáticamente la conformidad con respecto a varios estándares de codificación, como MISRA C , MISRA C++, CERT C Secure Coding Standard, CERT C++ Secure Coding Standard, [ 3 ] High-Integrity C++, NASA / JPL C, ESA /BSSC C/C++, JSF C++, EC--, [ 4 ] Netrino Embedded C, [ 5 ] The Power of Ten (C), [ 6 ] Industrial Strength C++. [ 7 ]
Para las pruebas de programas, ECLAIR puede sintetizar automáticamente conjuntos de entradas de pruebas unitarias que alcancen un criterio de cobertura especificado por el usuario, advirtiéndole cuando, debido a condiciones inviables en el programa, no se pueda alcanzar dicha cobertura.
En lo que respecta a la transformación de programas, ECLAIR puede utilizarse para realizar transformaciones complejas: estas se especifican mediante criterios sintácticos y semánticos; las regiones del programa en el código fuente que coinciden con estos criterios pueden sustituirse opcionalmente por una sustitución parametrizada.
Véase también
Referencias
- ↑ "Noticias BUGSENG" . bugseng.com . Consultado el 4 de abril de 2021 .
- ↑ R. Bagnara; PM Hill; E. Zaffanella (2007). "Un entorno basado en Prolog para razonar sobre lenguajes de programación". arXiv : 0711.0345 [ cs.PL ].
- ↑ Seacord, Robert C. (2013). Codificación segura en C y C++ . Serie SEI en Ingeniería de Software (2.ª ed.). Addison-Wesley Professional. ISBN 978-0-321-82213-0.
- ↑ Hatton, L. (2005). "EC: un subconjunto más seguro de ISO C basado en mediciones, adecuado para el desarrollo de sistemas embebidos". Information and Software Technology . 47 (3): 181– 695. CiteSeerX 10.1.1.101.7828 . doi : 10.1016/j.infsof.2004.08.001 .
- ↑ Barr, Michael (2008). Estándar de codificación C embebido . Barr Group. ISBN 978-1442164826.
- ↑ Gerald, J. (2006). "El poder de 10: reglas para desarrollar código crítico para la seguridad". Computer . 39 (6): 95– 97. Bibcode : 2006Compr..39f..95H . doi : 10.1109/MC.2006.212 . S2CID 7334261 .
- ↑ Henricson, Mats; Nyquist, Erik (1997). Industrial Strength C++ . Prentice-Hall PTR. ISBN 978-0131209657.
Enlaces externos
- Sitio web oficial de ECLAIR
- Herramientas de análisis estático de programas
- Herramientas de prueba de software