Proposition de Travaux d'Etude et de Recherche
Maîtrise 2002-2003
Sujet :
Utilisation et interface avec une librairie de representation des contraintes
lineaires par des automates (RVA)
Responsable :
Mihaela Sighireanu
(
http://www.liafa.jussieu.fr/~sighirea)
Nature du stage :
Etude et Programmation en C++
Nombre d'étudiants dans le groupe :
de 1 à 3.
Description du sujet :
La complexité croissante des logiciels ainsi que leur plus large utilisation
dans des équipements critiques (avions, trains, voitures,...) demandent
s'assurer du bon fonctionnement de ces logiciels. Pour cela, des techniques
de vérification automatique des programmes ont été développées ces derniers
années. Ces techniques consistent à explorer tous les exécutions possibles
des logiciels afin de contrôler que ses calculs ou réactions satisfont
certaines propriétés (p.e., absence de division par 0, valeurs des variables
dans certaines bornes).
Les logiciels qui implémentent ces techniques utilisent souvent une
représentation symbolique des contraintes sur les variables.
C'est le cas du logiciel TReX, développé au LIAFA
(
www.liafa.jussieu.fr/~sighirea/trex)
qui utilisent pour le moment une représentation symbolique syntaxique de ces
contraintes (bibliothèque Foaf).
Des chercheurs de l'Université de Liège ont
développé une bibliothèque (appelée
RVA)
qui utilise une représentation basée sur les automates finis
de contraintes linéaires entre variables entières et/ou réelles.
Le travail proposé dans ce TER est d'étudier cette bibliothèque
et d'implémenter une interface entre TReX et les RVA.
Le langage de programmation sera le C++.
Connaissances préalables souhaitées :
- Programmation,
- Compilation (essentiellement l'analyse syntaxique),
- Automates.