Proposition de Travaux de Recherche Encadres
Master 1 2005-2006


Etude et implementation d'une librairie de representation des contraintes
de type intervalle parametré

Organisation

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/trex) qui utilise plusieurs representations symboliaues (PDBM, arbres syntaxiques,etc).

Recemment, des travaux (voir bibliographie) ont ete effectuer pour y ajouter une nouvelle representation symbolique pour les contraintes de type intervalle ( l &less; x &grt; u) ou les bornes des intervalles sont des termes symboliques. Il a ete montre l'interet de cette representation pour la verification des protocoles, comme par exemple le protocole PGM.

Le travail proposé dans ce TRE est d'étudier cette representation, de l'implementer et puis de l'appliquer a la verification du protocole PGM. Le travail d'implementation sera effectue en C++ et C sous la forme d'une bibliotheque de TReX.

Connaissances préalables souhaitées :

Bibliographie