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.

Un docteur (2013) à Sorbonne Université

Publications 2004-2013

• 2013
  • S.‑H. Syed‑Alwi, C. Braunstein, E. Encrenaz : “Efficient Refinement Strategy Exploiting Component Properties in a CEGAR Process”, chapter in Models, Methods and Tools for Complex Chip Design, selected contributions from FDL 2012, vol. 265, Lecture Notes in Electrical Engineering, pp. 17-36, (Springer) (2013)
• 2012
  • S.‑H. Syed‑Alwi, C. Braunstein, E. Encrenaz : “AN EFFICIENT REFINEMENT STRATEGY EXPLOITING COMPONENT PROPERTIES IN A CEGAR PROCESS”, Forum on specification & Design Languages (FDL 2012), Vienne, Austria, pp. 27-34 (2012)
• 2011
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, I. Mounier, D. Poitrenaud, S. Younes : “Feasibility Analysis for Robustness Quantification by Symbolic Model Checking”, Formal Methods in System Design, vol. 39 (2), pp. 165-184, (Springer Verlag) (2011)
• 2010
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes : “Quantifying Robustness by Symbolic Model checking”, 1^st Hardware Verification Workshop (CAV workshop), Edinburgh, United Kingdom, pp. 1-12 (2010)
• 2009
  • A. Suelflow, G. Fey, C. Braunstein, U. Kuehne, R. Drechsler : “Increasing the Accuracy of SAT-Based Debugging”, DATE Design Automation and Test in Europe Conference, Nice, France, pp. 1326-1331, (IEEE) (2009)
  • S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.‑M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud : “Complementary formal approaches for dependability analysis”, The 24^th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Chicago, Illinois, United States, pp. 331-339, (IEEE Computer Society) (2009)
• 2007
  • C. Braunstein : “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”, soutenance de thèse, soutenance 14/05/2007, direction de recherche Encrenaz, Emmanuelle, co-encadrement : Munier, Alix (2007)
  • C. Braunstein, E. Encrenaz : “Using CTL formulae as component abstraction in a design and verification flow”, ACSD IEEE International Conference on Application of Concurrency to System Design, Bratislava, Slovakia, pp. 80-89, (IEEE) (2007)
  • C. Braunstein, E. Encrenaz : “CTL-property Transformations along an Incremental Design Process”, International Journal on Software Tools for Technology Transfer, vol. 9 (1), pp. 77-88, (Springer Verlag) (2007)
• 2006
  • C. Braunstein, E. Encrenaz : “A Further Step in the Incremental Design Process: Incorporation of an Increment Specification”, LPAR IEEE International Conference on Logic for Programming Artificial Intelligence and Reasoning, Phnom Penh, Cambodia, pp. short paper (2006)
  • C. Braunstein, E. Encrenaz : “Formalizing the incremental design and verification process of a pipelined protocol converter”, RSP International Workshop on Rapid System Prototyping, Chania, Crete, Greece, pp. 103-109, (IEEE) (2006)
• 2005
  • C. Braunstein, E. Encrenaz : “CTL-property transformations along an incremental design process”, (2005)
• 2004
  • C. Braunstein, E. Encrenaz : “CTL-Property Transformations along an Incremental Design Process”, AVOCS 2004 - 4^th International Workshop on Automated Verification of Critical Systems, London, United Kingdom, pp. 263-278 (2004)