BRAUNSTEIN Cécile

Docteur
Équipe : ALSOC
Date de départ : 30/09/2007
https://lip6.fr/Cecile.Braunstein

Direction de recherche : Emmanuelle ENCRENAZ

Co-encadrement : 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.

Soutenance : 14/05/2007

Membres du jury :

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

Maître de Conférences

1 Docteur 2013

Publications 2004-2013

Mentions légales
Carte du site