|
|
|
|
|
|
|
|
 
|
|
 
|
Evaluation de la robustesse des circuits embarqués par les approches formelles
Emmanuelle Encrenaz et Jean-Michel Ilié Université P. & M. Curie, LIP6 - CNRS UMR 7606 – 4 Place Jussieu, Paris, France emmanuelle.encrenaz(at)lip6(.)fr,
Contexte et positionnement
Le projet ANR FME3 est un projet national, développé entre l'université de Grenoble et le LIP6. Nous nous intéressons aux systèmes embarqués critiques qui sont soumis aux perturbations magnétiques de l'espace. Ces perturbations occasionnent des erreurs logiques dans les circuits pouvant conduire le système embarqué à des dysfonctionnements irréparables. Les erreurs sont vus comme des erreurs de bits dans les registres du système. L'objectif général du projet est de construire une plateforme technique permettant d'évaluer la prédisposition des circuits à refonctionner normalement après une période de perturbations, ce que l'on peut comprendre comme une reconfiguration évoluée et compatible avec les spécifications de fonctionnement du système embarqué. Nous préconisons d'exploiter la logique temporelle pour évaluer différents critères de robustesse, l'évaluation étant réalisée pendant la phase de conception, sur le modèle du système. La conception d'une telle plateforme nécessite de se confronter aux réalités suivantes : - les circuits embarqués sont composés de centaines de registres ; - les perturbations agissent dynamiquement sur les registres, temporellement (en séquence) et spatialement (plusieurs bits sont concernés) ; - les erreurs occasionnées à un moment dans des registres peuvent se propager vers d'autres registres lors des cycles d’exécution subséquents Chaque erreur peut donc générer une explosion d'états erronés à partir desquels il faudra évaluer une possibilité de "réparation". Cela constitue actuellement un verrou scientifique et technologique, même si des solutions partielles existent, consistant principalement à restreindre arbitrairement le nombre d'études de cas d'erreur à traiter [GSD09]. L'ambition de notre projet est de traiter les fautes multiples, de quelque endroit qu'elles viennent, et pour toute considération d'incidence, qu'elle soit spatiale ou temporelle [L05][BB+09]. Nous avons développé un algorithme pour cela et préconisons d'exploiter des structures de données aptes à représenter et parcourir de façon ensembliste des espaces d'états très larges, comme 10100 états [BDD & SAT solvers]. La gestion ensembliste est directement liée à une représentation interne du système de transition d'un circuit sous forme de variables booléennes, d'où le nom de système de transition symboliques. La plateforme de vérification VIS permet automatiquement d'implanter des spécifications de circuits sous cette forme et en donne une évaluation en construisant l'espace d'états ou en résolvant des propriétés de logiques temporelles LTL et CTL. De nombreux exemples sont mis à la disposition de l'utilisateur, dans un format très lisible [VIS].
Finalité du stage Le travail demandé consiste à développer de nouvelles fonctionnalités dans la plateforme VIS concernant la robustesse des circuits embarqués. Il s'agira de définir une méthodologie de test permettant de tester un circuit soumis à des fautes en comparant son fonctionnement à celui du circuit original non soumis aux fautes (dit golden model).
1. Dans un premier temps, vous exploiterez toutes les fonctionnalités existantes dans VIS pour évaluer la robustesse du circuit fauté. Vous exploiterez notamment l'éditeur de spécification de VIS pour réaliser votre environnement de test et chercherez à tirer partie au mieux du jeu d'algorithmes proposés pour élaborer une analyse comportementale. Votre premier résultat permettra d'évaluer les capacités intrinsèques de la plateforme VIS à évaluer des critères de robustesse de façon symbolique. 2. Puis, en fonction des limites rencontrées, vous proposerez une évolution à ce travail soit pour améliorer les critères testables dans le cadre de la robustesse, soit pour améliorer encore le passage à l'échelle (en temps et en espace). Cette deuxième phase vous permettra d'approfondir votre expérience de VIS et des approches symboliques sous-jacentes.
Prérequis et apports du stage Nous vous demandons: - un sens de la bonne programmation en C. - une bonne intuition des comportements dans les systèmes concurrents. - la validation d’un module d’enseignement niveau M2 sur les bases de vérification par model-checking (module SAR : MSR / VFSR ou module SESI : VERIF). Vous aurez l'occasion: - d'aborder la programmation efficace des ensembles, - d'appliquer vos connaissances en techniques de vérification.
Une poursuite en thèse est possible dans le domaine de l'embarqué.
Références bibliographiques [BB+09] 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", 24th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, DFT 2009, Chicago, Illinois, USA. [BDD & SAT] Des tutoriaux seront mis à votre disposition. [VIS] The vis home page, http://vlsi.colorado.edu/~vis/ [GSD09] F. Görschwin, A. Sülflow et R. Drechsler, "Computing bounds for fault tolerance using formal techniques", 46th ACM Design Automation Conference - DAC, San Francisco, CA, USA, 2009. [FD08] G. Fey et R. Drechsler, "A Basis for Formal Robustness Checking", IEEE International Symposium on Quality Electronic Design - QED, 2008. [BCNTW06] H. Bar-El, H. Choukri, D. Naccache, M. Tunstall, C. Whelan, "The sorcerer's apprentice guide to fault attacks", Revue IEEE, vol.94-2, 2006. [L05] R. Leveugle, "A new approach for early dependability evaluation based on formal property checking and controlled mutation", 11th IEEE International On-Line Testing Symposium - OLTS, 2005. |
