ENCRENAZ Emmanuelle

Contributions pour la conception et la vérification de systèmes matériels embarqués

Les travaux décrits ici se placent dans le cadre de l'utilisation des méthodes formelles pour la conception et la vérification de (parties de) systèmes intégrés sur puce. Une première contribution concerne la définition d'une méthode de conception de composants incrémentale. Celle-ci procède par ajouts successifs de nouveaux comportements à un composant initial. Elle garantit par construction la non-régression. De plus, les ajouts effectués sur le composant peuvent être transposés automatiquement dans la spécification du composant, permettant ainsi de garantir l'évolution conjointe de la spécification et du composant. Différents types d'ajouts, ainsi que les transformations de la spécification associées ont été définis; ils ont permis de concevoir et vérifier un ensemble de convertisseurs entre le protocole VCI (Virtual Component Interface) et les protocoles de bus PI et AMBA. Par ailleurs, un sous-ensemble des propriétés formant la spécification d'un composant peut également être utilisé pour réaliser une abstraction du composant, et ainsi limiter le problème d'explosion combinatoire rencontré lors de la vérification de propriétés faisant intervenir plusieurs composants. Une seconde contribution concerne le développement de méthodes et outils algorithmiques pour améliorer les techniques de vérification existantes. Nous proposons d'utiliser des diagrammes de données hiérarchiques pour repousser les limites du model-checking pour des systèmes très fortement concurrents, décrits à un haut niveau d'abstraction et communiquant de façon asynchrone. L'outil HaDDock, un model-checker pour analyser des systèmes statiques décrits en {em promela}, permet l'analyse de propriétés temporelles de tels systèmes. Par ailleurs, en nous focalisant sur l'analyse des interblocages dans les réseaux sur puce, nous proposons un algorithme original déterminant si une fonction de routage, appliquée à un réseau de topologie donnée, est exempt d'interblocage. Une troisième contribution concerne l'analyse temporelle de circuits asynchrones. Nous définissons une méthode de résolution du problème inverse de ``Time Separation of Events'', permettant de construire des ensemble des contraintes liant les paramètres temporels du circuit, et garantissant des plages de bon fonctionnement dudit circuit. Cette méthode a été appliquée avec succès sur la mémoire embarquée SPSMALL, conçue et commercialisée par STMicroelectronics, et a permis de fournir une justification formelle à la réduction des temps de setup des signaux d'entrée.

Soutenance : 18/06/2007

Membres du jury :

BORRIONE Dominique, professeur à l'Université Joseph Fourier, Grenoble, Rapporteur
JARD Claude, , Professeur à l'ENS-Cachan, Rennes, Rapporteur
FEAUTRIER Paul, professeur à l'ENS-Lyon, Examinateur, Président du Jury
FRBOURG Laurent Fribourg, , Directeur de recherche CNRS au LSV, Cachan, Examinateur
GREINER Alain, professeur à l'Université Pierre et Marie Curie,Paris, Examinateur
MALER Oded, Directeur de recherche CNRS au VERIMAG, Grenoble, Examinateur