Speaker
Mr
Jérôme Hugues
(ISAE)
Description
Activity: Lab Investment
ESA TO: Maxime Perrotin - Software Systems Division
TASTE relies on code generation since its inception. As part of the TASTE process, code generation aims at automating tedious and error prone software engineering activities, so as to leverage models to synthesize the corresponding source-level artefacts. A current research challenge lies in the quality of the generated code. Peer-review is not sufficient: one needs to ensure preservation of semantics, absence of runtime errors, etc. ISAE led an effort to evaluate the applicability of theorem proving applied to the TASTE runtimes. The objective is to demonstrate formally the code generated, and its associated runtimes are free of typical runtime errors (buffer overflows, off-by-one, numerical errors). To do so, we rely on the ACSL annotations to define formal contracts associated to each function, and use Frama-C to show the implementation conforms to those formal contracts. At the end of the study, we could demonstrate a significant part of the TASTE runtime is free of runtime errors, increasing the confidence in the whole TASTE toolchain.
