Instrumentation of annotated c programs for test generation

G. Petiot 1, 2 B. Botella 1 J. Julliand 2 N. Kosmatov 1 J. Signoles 1
1 DILS - Département Ingénierie Logiciels et Systèmes
2 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
Abstract : Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool Study. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses.
Keywords : Computational linguistics Formal specification Software testing Specification languages Specifications Translation (languages) Verification C programs Deductive verification Frama-C Static and dynamic analysis Test generations C (programming language) Codes (symbols) Automatic programming
Document type :
Conference papers
Complete list of metadatas
https://hal-cea.archives-ouvertes.fr/cea-01836306
Contributor : Léna Le Roy <>
Submitted on : Thursday, July 12, 2018 - 11:27:01 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Identifiers

Collections

CEA | CNRS | UNIV-FCOMTE | UNIV-BM | UNIV-BM-THESE | DRT | FEMTO-ST | LIST

Citation

G. Petiot, B. Botella, J. Julliand, N. Kosmatov, J. Signoles. Instrumentation of annotated c programs for test generation. 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation, Sep 2014, Victoria, Canada. pp.105-114, ⟨10.1109/SCAM.2014.19⟩. ⟨cea-01836306⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

127

Contact

Informations

CCSD