Guía para la verificación de software con Frama-C: Componentes básicos, usos y aplicaciones

Título original:

Guide to Software Verification with Frama-C: Core Components, Usages, and Applications

Contenido del libro:

Frama-C es un popular conjunto de herramientas de código abierto para el análisis y la verificación de programas en C, muy utilizado en la enseñanza, la investigación experimental y las aplicaciones industriales.

Con la creciente complejidad y ubicuidad del software moderno, aumenta el interés por las herramientas de análisis de código en varios niveles de formalización para garantizar la seguridad de los productos de software. Reconociendo el hecho de que ninguna técnica podrá satisfacer por sí sola todas las necesidades de verificación del software, la plataforma Frama-C presenta un amplio conjunto de plug-ins que pueden utilizarse o combinarse para resolver tareas específicas de verificación.

Esta guía presenta un amplio panorama de usos básicos, resultados de investigación y aplicaciones concretas de Frama-C desde la primera versión de código abierto de la plataforma en 2008. Abarca el lenguaje de especificación ACSL, los principales plug-ins de verificación, los análisis avanzados y sus combinaciones, los ingredientes clave para el desarrollo de nuevos plug-ins, así como casos prácticos industriales de éxito en los que Frama-C ha ayudado a los ingenieros a verificar propiedades de seguridad cruciales.

Temas y características:

* Guía paso a paso para desarrollar su propio análisis a medida sobre la plataforma* Casos de éxito inspiradores de la implementación de Frama-C en código industrial* Más de 15 años de I+D en análisis y verificación de código C

Este libro está firmemente arraigado en la práctica del análisis de software, con numerosos ejemplos, ejercicios y directrices de aplicación. Como tal, es especialmente adecuado para los profesionales de la verificación de software que deseen implementar la verificación en su código, así como para estudiantes universitarios con poca o ninguna experiencia en técnicas de análisis de código. Las secciones más avanzadas sobre los fundamentos teóricos de los analizadores serán de interés para estudiantes de posgrado e investigadores.

Nikolai Kosmatov es investigador principal en Thales Research & Technology, Francia. Virgile Prevosto es investigadora principal y Julien Signoles es director de investigación, ambos en la Université Paris-Saclay, CEA, List, Francia.