Minalogic

Minalogic : Parlez-nous de VERIMAG...

Nicolas Halbwachs : Verimag est un laboratoire de recherche publique, commun au CNRS, à l'Université Joseph Fourier et à Grenoble INP. C'est un laboratoire de taille moyenne, avec un effectif d'une quarantaine de permanents et d'une cinquantaine de doctorants, post-doctorants et ingénieurs contractuels.

Verimag a été fondé il y a vingt ans, sur la base de deux « success stories » :
• l'invention du « model-checking », méthode de vérification des systèmes informatiques qui a valu à Joseph Sifakis, fondateur du laboratoire, le Prix Turing 2007, équivalent du Prix Nobel en informatique.
• la conception, par Paul Caspi et moi-même, du langage synchrone Lustre, qui forme le socle de l'atelier industriel Scade, développé par la Société Esterel-Technologies ; Scade est devenu un standard de fait au niveau international en matière de conception de logiciel embarqué critique, notamment dans l'avionique et le ferroviaire.
Depuis sa création, Verimag a largement diversifié ses domaines de recherche, tout en gardant une cohérence thématique globale autour des méthodes de conception de systèmes embarqués, privilégiant une approche formelle. Le laboratoire est constitué de 3 équipes, qui collaborent étroitement entre-elles :

L'équipe SYNCHRONE a poursuivi les recherches et développements sur les langages synchrones, en élargissant leur domaine d'application. L'équipe étudie les techniques et outils de validation de programmes et de systèmes, basées sur le model-checking, l'interprétation abstraite, le test automatique, le prototypage virtuel et la simulation. Les activités de l'équipe dépassent le cadre des langages synchrones et des systèmes de contrôle, pour couvrir les principaux aspects de la conception, de l'implémentation, et de la validation des systèmes embarqués, en prenant en compte leurs propriétés non fonctionnelles, comme le temps d'exécution, la consommation énergétique, et les spécificités des plates-formes matérielles. Les principaux domaines d'application actuellement considérés sont les systèmes de contrôle embarqués, les systèmes sur puce (et, plus généralement, les systèmes combinant étroitement le logiciel et un matériel spécifique), et les réseaux de capteurs (et, plus généralement, les réseaux de systèmes embarqués).

L'équipe DCS est spécialisée dans les systèmes distribués complexes, c'est-à-dire les applications temps-réel, logicielles et matérielles, les protocoles et applications de sécurité. Tous ces systèmes présentent des comportements complexes et doivent satisfaire des propriétés fonctionnelles et non fonctionnelles (contraintes de temps, de performances, de sûreté et de sécurité ...). L'équipe développe des langages et des méthodes pour résoudre les problèmes fondamentaux soulevés par les applications, dans le but d'aboutir à des solutions rigoureuses et de fournir des outils. Les activités de DCS sont organisées autour de 4 thèmes :
• Les méthodes formelles pour la sécurité informatique, c'est-à-dire la résistance des systèmes informatiques aux attaques malveillantes. Les aspects mathématiques de la sécurité sont étudiés (cryptographie, modèles formels, preuves et vérification assistée). Des domaines d'application importants sont les protocoles de sécurité et les cartes à puce.
• Le développement rigoureux de systèmes à base de composants. La complexité croissante des systèmes embarqués ne peut être maîtrisée que par des méthodes de conception modulaires, consistant à concevoir et valider des composants, puis à les combiner dans les applications. Pour assurer la correction par construction des systèmes ainsi conçus, l'équipe développe le formalisme BIP (« Behaviour-Interaction-Priorities ») et des outils de génération automatique de code (notamment sur multicoeur) et de validation associés.
• Les langages pour la spécification et la validation : l'équipe a défini le formalisme IF, représentation intermédiaire pour les systèmes distribués temps-réel. Son pouvoir d'expression permet d'utiliser IF pour traduire les langages de modélisation standard comme SDL et UML, ainsi que les aspects liés au temps réel, aux performances et à l'ordonnancement.
• La vérification de programmes : l'application des techniques de model-checking au logiciel nécessite l'usage d'abstractions appropriées. Par ailleurs, l'extension de ces techniques pour prendre en compte les structures de données complexes omniprésentes dans le logiciel pose un réel défi. L'équipe étudie des techniques exactes ou approchées pour résoudre ces problèmes, et les implémente dans des outils (INVEST, IF, BIP).

L'équipe TEMPO s'intéresse aux systèmes temporisés et hybrides, qui combinent des aspects discrets et continus. Ce type de système doit être pris en compte lorsqu'on considère un système embarqué dans son environnement physique et que l'on s'intéresse à ses propriétés globales. Le domaine se situe donc à la frontière de l'informatique et de l'automatique. La première « variable » continue à prendre en compte, est évidemment le temps, et l'équipe a étudié l'usage des automates temporisés, formalisme exprimant le fonctionnement d'un système discret en temps continu. Un des premiers outils d'analyse des ces automates, Kronos, a été développé dans l'équipe. Plus généralement, TEMPO étudie les formalismes et outils de simulation et d'analyse des systèmes hybrides, combinant des aspects discrets (programmes ou automates) et continus (équations différentielles). Nous avons proposé dès 1990 le formalisme des automates hybrides, devenu classique, et nous produisons et diffusons des outils de validation et de simulation de ces automates. Les applications considérées récemment incluent les circuits asynchrones et la bio-informatique.

Verimag a participé à la création des conférences internationales « Computer-Aided Verification » (CAV) et « Embedded Software » (EMSOFT), et a coordonné les réseaux d'excellence européens ARTIST, ce qui a fortement contribué à sa visibilité internationale. Verimag est également fortement impliqué dans les structures locales, comme l'Institut Carnot LSI, le Centre de Recherches Intégratives (CRI), et, évidemment, Minalogic. Notons que deux membres de Verimag, Joseph Sifakis et Florence Maraninchi, se sont succédé comme membres du Comité Opérationnel de Minalogic.

Minalogic : Dans quel(s) projet(s) du pôle êtes-vous impliqués ? Quelles compétences y apportez-vous?

N. H. : Malgré sa taille modeste, Verimag a une participation considérable dans les projets du pôle, depuis sa création :

• Le projet openTLM (2006-2010) regroupait les sociétés STMicroelectronics, Orange IT&L@bs, Safetronix, ainsi que les laboratoires CEA-LETI, INRIA, TIMA et VERIMAG. Le projet portait sur le développement d'outils pour la modélisation de systèmes sur puce au niveau transactionnel (TLM). La contribution de Verimag a porté sur les techniques de validation formelle applicables aux modèles TLM écrits en SystemC, le standard industriel du domaine. Les outils développés ont été intégrés dans un environnement de modélisation commun. Le projet a été l'occasion de consolider les relations de Verimag avec STMicrolectronics, démarrées en 2002 par une thèse CIFRE. Le projet a également eu un impact sur les filières de formation : les étudiants de la filière « Systèmes et Logiciels Embarqués » de Grenoble INP ont maintenant un cours de modélisation transactionnelle. Enfin les rencontres avec les industriels locaux dans le cadre de Minalogic ont permis de rassembler des partenaires pour le montage du projet ANR HELP (2009-2012), porté par Verimag.

• Dans le projet ATHOLE (2007-11), nous avons collaboré avec STMicroeletronics, le CEA-LETI, Thales et CWS sur le sujet brûlant du déploiement efficace de programmes d'application sur une architecture multiprocesseur, et en particulier la plate-forme P2012 développée par ST et le CEA. La contribution de Verimag a été (1) le développement de nouveaux algorithmes d'optimisation multi-critères, et leur application au placement et à l'ordonnancement sous contrainte de ressources ; (2) de nouveaux résultats sur la granularité optimale des appels DMA pour les applications à parallélisme de données ; (3) un outil d'évaluation de performance à haut niveau et d'exploration de l'espace de conception.

• Le projet MIND (2008-10) visait au développement d'une technologie industrielle pour la construction des systèmes embarqués basée sur les composants logiciels. Dans ce projet, nous avons étudié des approches amont dans le but d'assurer plus de confiance dans l'exécution du logiciel. Nous avons apporté nos compétences en matière de modélisation et de vérification des systèmes, avec par exemple l'utilisation de l'outil de vérification D-Finder développé à Verimag.

• Le projet SHIVA (2009-2011) a réuni des acteurs grenoblois de la sécurité informatique (CS, CEA-LETI, EASII IC, INRIA, NETHEOS, UJF-IF, UJF-LJK, VERIMAG, TIMA, IWALL). Son objectif était de fournir un module matériel programmable et reconfigurable, avec un haut niveau de sécurité évaluable au sens des critères communs à un niveau EAL4/5. Dans ce cadre nous avons contribué à la validation des solutions retenues et proposé des outils d'aide à leur conception.

• Dans le projet COMON (2010-12), nous collaborons avec les industriels grenoblois de la filière nucléaire (Atos Origin, Rolls-Royce Civil Nuclear, Corys TESS) à l'élaboration d'une méthodologie de conception des systèmes de contrôle-commande de centrales nucléaires. La contribution de Verimag concerne essentiellement l'application de nos méthodes de spécification et de test automatisé de systèmes synchrones. Une démonstration d'exécution intégrée des ateliers des trois partenaires industriels avec nos outils de test, sur une étude de cas réaliste, a été donnée à la dernière revue du projet.

Minalogic : Plus généralement, quels types de partenariats recherchez-vous ?

N. H. : Verimag a toujours été fortement impliqué dans des projets avec des partenaires industriels. L'intérêt pour nous n'est évidemment pas qu'économique. C'est très souvent dans de tels projets qu'émergent nos nouvelles problématiques de recherche. Cette confrontation avec les applications est pour nous garante de la pertinence des sujets abordés et des solutions proposées. Le contenu des projets va de la simple étude de cas pour confronter des solutions existantes à de nouveaux domaines, jusqu'à de véritables projets de recherche collaboratifs sur le moyen ou le long terme. La collaboration peut prendre diverses formes : partenariat direct, thèses CIFRE, projets ANR ou Minalogic, projets européens. Nous avons eu aussi des laboratoires communs avec des entreprises (avec la société toulousaine Vérilog, avec STMicroelectronics).

Pour plus d'informations sur Verimag : www-verimag.imag.fr