Stimuler la conception des systèmes embarqués - 6 février 2018

Petits-Déjeuners Persyval-Minalogic Mieux comprendre les problématiques de R&D

• découvrir les problématiques et les avancées de la recherche dans un secteur à la pointe de l’actualité
• appréhender le potentiel pour le développement innovant d’applications
• échanger sur des projets R&D avec des spécialistes du domaine

Seconde rencontre :

Stimuler la conception des systèmes embarqués :
modélisation, virtualisation, méthodes formelles

Mardi 6 février 2018 (8h15-10h30) - Campus de Saint Martin d’Hères

Dans tous les domaines d'application, la conception des systèmes embarqués fait face à la pression croissante de nombreux enjeux et contraintes : complexité, hétérogénéité, évolutivité, temps réel, fiabilité…, et bien sûr time to market. 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

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
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
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

10:00-10:30 : Temps d'échange
(pouvant se prolonger jusqu'à 11h pour ceux qui le souhaiteront)

Infos pratiques et inscription :

Mardi 6 février 2018, de 8h15 à 10h30

IMAG, 700 avenue centrale, Domaine universitaire, 38401 Saint-Martin d’Hères 
- Venir au bâtiment IMAG

L'inscription en ligne est fermée.