Contract-based Analysis and Dynamic Verification of C code

Abstract

[EN] In Software Engineering, software contracts allow the program behavior to be specified using formal axioms such as preconditions, postconditions and invariants. The current state of the art makes it possible to derive, from the program code, concise properties that can be then used as an input for program analyzers. However, such automatically derived contracts might not be fully precise and/or correct, leading to what is known as "abstract contracts", which may contain candidate axioms. In this project we propose two methods for the refinement of automatically inferred contracts, which in our case are generated by the automatic inference tool KindSpec 2.0. iii iv The first proposed technique is based on testing by using the automatic data generation tool QuickCheck. The second proposed technique translates candidate axioms into EACSL formulas that are dynamically verified by Frama-C. By exploting the synergy of the two methods, the abstract contract can be refined into correct (and often complete) software contracts.

[ES] En Ingeniería de Software, el concepto de contrato está relacionado con la especificación del comportamiento de un programa utilizando axiomas formales como precondiciones, postcondiciones e invariantes. El estado del arte actual permite derivar propiedades concisas que pueden ser usadas como entrada para analizadores de código con funcionalidad creciente. Sin embargo, estos contratos derivados automáticamente pueden no ser completamente precisos o correctos, correspondiendo a lo que se conoce como “contratos abstractos“ que contienen axiomas candidatos. En este documento proponemos dos métodos para el refinamiento de dichos contratos, los cuales en nuestro caso están generados por la herramienta de inferencia automática de especificaciones para código C llamada KindSpec 2.0. La primera técnica propuesta se basa en la realización de pruebas con la herramienta de generación automática de juegos de datos QuickCheck. La segunda técnica propuesta traduce los axiomas candidatos a fórmulas E-ACSL que son verificadas dinámicamente por Frama-C. Gracias a la sinergia entre las dos técnicas es posible refinar contratos abstractos para derivar de ellos contratos correctos y, en muchas ocasiones, completos.

[CA] En Engiyneria de Software, el concepte de contracte està relacionat amb l’especificació del comportament d’un programa emprant termes formals com precondicions, postcondicions i invariants. L’estat de l’art actual permet derivar propietats concisses que poden ser usades com entrada per analitzadors de codi. No obstant això, aquests contractes automàticament derivats poden no ser completament concissos o correctes, el que ens porta a el que coneixem com “contractes abstractes“, que poden contindre axiomes candidats. En aquest document proposem dos mètodes per al refinament de dits contractes, els quals en el nostre cas estàn generats per la ferramenta d’inferència automàtica d’especificacions denominada KindSpec 2.0. La primera proposta es basa en la realització de proves amb la ferramenta de generació automàtica de dades QuickCheck. La segona proposta, traduix els axiomes candidats a fòmules E-ACSL que son dinàmicament verificades per Frama-C. Explotant la sinergia dels mètodes, el contracte abstracte pot ser refinat i generar contractes software correctes (i sovint complets).