Validación Automática de Contratos Software

Abstract

[ES] En Ingeniería de Software, el concepto de contrato está relacionado con una descripción del comportamiento de los programas utilizando precondiciones y postcondiciones de métodos. El estado del arte actual permite generar automáticamente contratos a partir del código fuente que pueden ser usados como entrada para analizadores cada vez más potentes. Sin embargo, los contratos generados automáticamente pueden no ser completamente precisos o correctos, conteniendo algunos elementos que no están verificados. El objetivo de este proyecto es utilizar el generador automático de casos de prueba Klee para identificar y eliminar aquellos componentes de un contrato software que el proceso de validación determine que son falsos.

[EN] Software contracts can be seen as a description of the program behavior that is expressed by using method preconditions and postconditions. The current state of the art allows contracts to be automatically generated from the program source code so that they can be subsequently used by increasingly sophisticated analyzers. However, automatically generated contracts may not be completely accurate or correct, containing some components that are not verified. The goal of this project is to use the automated test case generator Klee to identify and eliminate those components of a software contract that can be proved to be false by the validation process.