LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » News » PhD students

BRAUNSTEIN Cécile

PhD graduated
Team : ALSOC
Associate Professor
Supervision : Emmanuelle ENCRENAZ
Co-supervision : MUNIER Alix

Conception Incrémentale, Vérification de Composants Matériels et Méthode d'Abstraction pour Vérification de Systèmes Intégrés sur Puce

Cette thèse traite de la vérification formelle par model checking de systèmes intégrés sur puce. Nous proposons d'abord une méthode de conception incrémentale pour la vérification d'un composant matériel. Cette méthode est un cadre de conception par ajouts successifs de nouveaux comportements. Nous avons montré que cette méthode assure la non-régression d'un composant tout au long de sa conception. D'autre part, cette méthode permet aussi de faire évoluer la spécification d'un composant en prenant en compte les différentes fonctionnalités ajoutées au cours de la conception. Nous avons ensuite particularisé cette approche pour la conception et la vérification d'architectures pipelines. Cette méthode a été utilisée avec succès pour la conception de convertisseurs de protocole. La vérification par model-checking d'un système intégré sur puce se confronte au problème d'explosion combinatoire. Les techniques d'abstractions sont des méthodes efficaces pour alléger ce problème. Nous exposons un algorithme d'abstraction basé sur la spécification de chaque composant. Cet algorithme construit une structure de Kripke représentant un sous-ensemble des formules CTL tirées de la spécification. Cette construction se place dans un contexte de raffinement d'abstraction guidé par l'étude du contre-exemple produit par le model checker. Les premières expérimentations que nous avons réalisées montrent un gain considérable en temps de vérification et un accroissement conséquent de la taille du système vérifié. Ces résultats nous confortent sur l'intérêt de cette méthode d'abstraction.
Defence : 05/14/2007 - 16h30 - Site Jussieu - Amphi Chouard
Jury members :
BERARD Béatrice, UNIV Paris Dauphine, Rapporteur
ENEKING Hans, TUD Darmstradt Allemagne, Rapporteur
GREINER Alain, UPMC/LIP6, Examinateur
ENCRENAZ Emmanuelle,UPMC/LIP6, Examinateur
MUNIER-KORDON Alix,UPMC/LIP6, Examinateur
BORRIONE Dominique, TIMA Grenoble, Examinateur/Président

1 PhD graduated 2013

2004-2013 Publications

 Mentions légales
Site map |