Chargement...
 

Programming-Testing-Proving

Domaine
Programming-Testing-Proving
Domain - extra
Program-based Tests
Année
2011
Starting
1.10.2010
État
Open
Sujet
Random-Based Methods for Test-Case-Generation of C Programs
Thesis advisor
WOLFF Burkhart
Co-advisors
Frederic Voisin (LRI)
Marie-Claude Gaudel (LRI)
Laboratory
Collaborations
CEA (Frama C ?)

Abstract
In this Phd, the goal is to explore static testing methods for a realistic subset of C, i.e. test-data are generated according certain criteria and techniques and run against „the real code“. A particular emphasis in this Phd is put on testing data-invariants of pointer structures, but also classical control-flow based test-case coverage criteria are considered, which were represented both by an LTL like assertion language. Such assertions can be compiled to graphs; instead of exploring them exhaustively, uniform random selection methods were applied to statically
generate constraints for object graphs and control-flow-graphs (path-conditions) as well. By finding effective means to approximate feasible paths (by invariant generation, abstract interpretation as well as code-slicing techniques), the effectivity of the overall method should be improved.
Context
The programming language C is widely used for operating system level code which is both complex (due to the need for efficiency and the proximity to hardware) and safety critical. Building environments to verify C code has therefore attracted the interest of many research groups, leading to environments such as Frama-C or Visualstudio/VCC.

Besides classical proof-based code analysis methods, there is the possibility to generate tests along control-flow graphs for programs. In the ForTesSE-group, a prototype called Auguste has been developed generates tests for a small fragment of C based on Johan Oudinets Rukia system that generates uniformly distributed random samples for such graphs.
Objectives
A major challenge is therefore to find a combination of:
- a „reasonably realistic“ memory model for C
- a combination of invariant-construction, abstract interpretation and code-slicing
- ... in order to get a good approximation of feasible paths before performing random-selection.
Work program
The practical part of this Phd consists in
- Integrating pre-existing AUGUSTE/RUKIA into Frama-C
- Developing an assertion language for data-structure consistency based on LTL
and the pre-existing ADCL2 (Frama C Jessie Plugin)
- implementing new invariant-construction, abstract interpretation and other techniques
(such as Dekkers Algorithm) in order to perform code-slicing before control-flow-graph
construction.

- careful statistic exploration of larger program samples.
Extra information
1.Sascha Böhme, Michal Moskal, Wolfram Schulte, Burkhart Wolff: HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler. J. Autom. Reasoning 44(1-2): 111-144 (2010)
2.G. J. Holzmann. The SPIN Model Checker : Primer and Reference Manual. Addison-Wesley Professional, September 2003.
3.D. Peled. Model checking and testing combined. In ICALP, pages 47–63, 2003
4.The Rukia Home Page: http://www.lri.fr/~oudinet/en/project.html

Prerequisite
- Knowledge or interest in functional programming in OCaml
- Knowledge over elementary logic and program analysis
Détails
Télécharger Random-based Test-Case Generation for C (RTGC).pdf
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Utilisateur
Créé
Mardi 08 juin 2010 00:08:27 CEST
dernière modif.
Vendredi 03 juin 2011 10:12:06 CEST

Fichiers joints

 filenamecrééhitsfilesize 
Random-based Test-Case Generation for C (RTGC).pdf 08 Jun 2010 00:081999108.10 Kb


Ecole Doctorale Informatique Paris-Sud


Directrice
Nicole Bidoit
Assistante
Stéphanie Druetta
Conseiller aux thèses
Dominique Gouyou-Beauchamps

ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr