Stimuler la conception des systèmes embarqués / Petits-Déjeuners PERSYVAL-Minalogic

Ce contexte rend indispensable la possibilité de modéliser rigoureusement le système matériel/logiciel dès les plus hauts niveaux du flot de conception et de procéder à des vérifications de bonne conception tout au long de ce flot. Deux grandes familles de méthodes participent à ce challenge : la vérification en exécution via la simulation et le raisonnement symbolique au moyen de méthodes formelles. Ces deux domaines, en constante évolution, offrent une panoplie de solutions riches et complémentaires.

L'objectif de cette rencontre est de dresser un panorama de leurs apports respectifs : d'une part sur les dernières avancées quant à l'efficacité de la simulation de systèmes à base de processeurs grâce aux techniques de virtualisation, et d'autre part sur la variété des vérifications et analyses pouvant être réalisées au moyen d'outils basés sur du raisonnement formel.

Programme et présentations

• 08:15-08:30 : Accueil
• 08:30-08:45 : Exposé introductif
  Positionnement Simulation/Méthodes formelles en bref
  Laurence Pierre, Université Grenoble Alpes, laboratoire TIMA et UFR IM2AG
  Télécharger la présentation
• 08:45-09:45 : Exposés spécialisés
  • Plateformes virtuelles : simulation matériel/logiciel efficace et nouvelles techniques de virtualisation
    Frédéric Pétrot, Grenoble INP, Laboratoire TIMA
    Télécharger la présentation
    Le prototypage virtuel a pour objectif de simuler le comportement d'un système numérique complet constitué d'un modèle virtuel de la plateforme matérielle incluant des processeurs, et le logiciel qui s'exécute sur ces processeurs. Cette approche s'appuie sur des techniques de modélisation spécifiques et est réalisable à différents niveaux d'abstraction, de sorte que des compromis entre vitesse et précision puissent être faits. Cette présentation détaille les défis posés aux méthodes de prototypage virtuel et introduit les niveaux d'abstraction communément admis. Nous insisterons en particulier sur les techniques exploitant la traduction binaire dynamique et son intégration au sein de SystemC, le standard de modélisation des composants numériques actuel.
  • Apport des méthodes formelles  
    David Monniaux, CNRS, Laboratoire VERIMAG
    Télécharger la présentation
    En complément aux analyses en simulation, de nombreuses méthodes donnent la possibilité de raisonner formellement, sur un modèle du système, afin de vérifier des propriétés variées (correction fonctionnelle, absence d'interblocages, respect de contraintes temps-réel, rigueur des accès mémoire, …). Ces méthodes s'appuient sur des techniques diverses (model checking, analyse statique, assistants de preuve, …). L'objectif de cet exposé sera de fournir un panorama des vérifications réalisables, et de l'état courant des méthodes et outils associés.
• 09:45-10:00 : Conclusion
  Résumé des moyens de collaboration, des équipes LabEx et des masters concernés par ce thème
  Télécharger la présentation
• 10:00-10:30 : Temps d'échange (pouvant se prolonger jusqu'à 11h pour ceux qui le souhaiteront)