Inferencia de especificaciones para programas C

Abstract

[EN] Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this Master Thesis we propose a technique for automatically discovering specifications from real code. The proposed methodology relies on the symbolic execution capabilities recently provided by the K framework that we exploit to automatically infer formal specifications from programs that are written in a non-trivial fragment of C, called KernelC. Roughly speaking, our symbolic analysis of KernelC programs explains the execution of a (modifier) function by using other (observer) routines in the program. We implemented our technique in the automated tool KindSpec 2.0, which generates axioms that describe the precise input/output behavior of C routines that handle pointer-based structures (i.e., result values and state change). We describe the implementation of our system and discuss the differences w.r.t. previous work on inferring specifications from C code.

[ES] A pesar de los abundantes beneficios que ofrecen, las especificaciones formales no acostumbran a emplearse en el desarrollo industrial de software. Con la finalidad de reducir el tiempo y el esfuerzo requerido para escribir especificaciones formales, en la presente Tesis de Máster se propone una técnica que obtiene de manera automática especificaciones a partir de código real. La metodología propuesta se basa en explotar las capacidades de ejecución simbólica recientemente proporcionadas por el marco K para inferir automáticamente especificaciones formales de programas escritos en un fragmento no trivial de C, denominado KernelC. En términos generales, el análisis simbólico de programas KernelC explica la ejecución de una función (modificadora) a través de otras rutinas (observadoras) del programa. Esta técnica ha sido implementada en la herramienta automática KindSpec 2.0, la cual genera axiomas que describen el comportamiento de entrada/salida de rutinas C que gestionan estructuras basadas en punteros (es decir, valores resultado y cambios de estado). En esta disertación se describe la implementación de dicho sistema y se analizan las diferencias respecto de trabajos previos relacionados con la inferencia de especificaciones sobre código C.