Programming-Testing-Proving
- Domaine
- Programming-Testing-Proving
- Domain - extra
- Runtime-Testing
- Année
- 2012
- Starting
- october
- État
- Open
- Sujet
- Random-Based Methods for Testing C Data-Structures
- Thesis advisor
- WOLFF Burkhart
- Co-advisors
- Frederic Voisin (LRI), Rukia/Auguste Toolchain
- Laboratory
- Collaborations
- Benjamin Monate (CEA) Frama-C
- Abstract
- In this Phd, the goal is to explore runtime-testing methods for a realistic subset of C. Runtime-testing means, that specifications for C code were represented by assertions which were compiled to optimized code that is injected into the running executions. A particular emphasis in this Phd is put on testing data-invariants, which were represented by an LTL like assertion language. These assertions were compiled to graphs that were examined by uniformly selected random-samples at runtime.
- Context
- The programming language C is widely used for operating system level code which is both complex (due to the need for efficiency and 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.
As verification technique, we use random-based testing techniques along the lines of the Rukia-System by Johan Oudinet, which can generate statistically uniform random-samples of graph-like structures.
So far, however, the technology has been applied on control-flow-graphs (instead of dynamic data stuctures such as linked lists) and in an entirely static context. - Objectives
- LTL data assertions can be represented by graphs which can be checked against the „real object graph“ produced at runtime in the program. Such complete checks are expensive, therefore, this Phd will check only a uniform random sample of paths in this graph. Since programs tend to do little increments on data-structures, it can be assumed that randomized checks will have an accumulating effect on accurancy while not revealing a too large penalty wrt. runtime costs. However, random-sampling methods such as Rukia require „the entire graph“ and provide a sampling for a given depth; however, this information is only known at runtime. Rukia provides methods to partially pre-compile automata-products, though, such that at least the part of the graph stemming from the specification can be treated statically. It remains to explore how the costs for re-sampling can be deminished by knowledge available at runtime in order to make the overall method effective.
- Work program
- The practical part of this Phd consists in
- Integrating AUGUSTE/RUKIA into Frama-C
- Developing an assertion language for data-structure consistency based on LTL
- Converting LTL into Automatas for which RUKIA computes
- a pre-conceived random selection
- or: a Markov Automata
- or: a function that takes a current object-graph and compiles them into test
samples turn this into code for run-time testing C data-invariants
- careful statistic exploration of large program samples.
- Extra information
- 1.G. J. Holzmann. The SPIN Model Checker : Primer and Reference Manual. Addison-Wesley Professional, September 2003.
2.D. Peled. Model checking and testing combined. In ICALP, pages 47–63, 2003
3.The Rukia Home Page: http://www.lri.fr/~oudinet/en/project.html
4.A Denise, MC Gaudel, S Gouraud, R Lassaigne, J Oudinet, et S Peyronnet. Coverage-biased random exploration of large models. Dans ETAPS, Workshop on Model Based Testing, ENTCS, pages 3-14, March 2008.
5.The FramaC Home Page: http://fra - Prerequisite
- - Good Knowledge over C as a programming language
- Good Knowledge in Compiler Construction
- Interest in Functional Programming (OCaml). - Détails
Random-based Runtime-Testing C (RRTC).pdf- Expected funding
- Institutional funding
- Status of funding
- Expected
- Candidates
- Utilisateur
- burkhart.wolff
- Créé
- Lundi 07 juin 2010 23:40:22 CEST
- dernière modif.
- Mardi 22 mai 2012 15:11:10 CEST
Connexion
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