Prix & Distinctions
L'équipe Convecs renforce la sûreté des systèmes parallèles
Date:
Mis à jour le 23/11/2023
Quatre chercheurs de l'équipe-projet Convecs viennent de recevoir le Prix de l'innovation Inria – Académie des sciences – Dassault Systèmes. Ils contribuent au développement de la boîte à outils CADP, dédiée à la modélisation et à la vérification des systèmes parallèles et distribués. L'objectif est de détecter automatiquement les erreurs de conception dans ces systèmes très complexes.
CADP, une boîte à outils diffusée dans le monde entier
Le bâtiment-paquebot du centre Inria Grenoble – Rhône-Alpes à Montbonnot Saint-Martin, en périphérie de Grenoble, accueille la quinzaine de membres de Convecs, équipe-projet commune entre Inria Grenoble – Rhône-Alpes et le laboratoire d’informatique de Grenoble. Quatre chercheurs Inria, un professeur de l’université Grenoble Alpes, des doctorants, postdoctorants, ingénieurs experts et stagiaires, mènent ici des recherches sur la modélisation et la vérification des systèmes parallèles et interconnectés.
La boîte à outils CADP (pour "Construction and Analysis of Distributed Processes" en anglais) est issue de leurs travaux. Il s'agit d'une plate-forme modulaire, mise en route en 1986, qui comporte une cinquantaine d'outils dont l'impact est notable dans la recherche et l’enseignement : ils ont déjà donné lieu à plus de 200 publications et à plus de 100 prototypes de recherche. Plusieurs entreprises comme Airbus, Google, Bull, STMicroelectronics, Tiempo Secure, et des centres de recherche industrielle comme le CEA-Leti et l’IRT Saint-Exupéry, ont acquis des licences. « Nous travaillons aussi, par exemple, avec des industriels de l'automobile, des spécialistes des composants mécatroniques (comme Crouzet) et de grands acteurs des télécoms ou du Cloud (comme Orange et Nokia Bell Labs) », indique Wendelin Serwe, chercheur de l’équipe Convecs.
Des systèmes informatiques de plus en plus complexes
« Les recherches de Convecs portent sur la modélisation et la vérification des systèmes parallèles asynchrones », précise Radu Mateescu, en charge de cette équipe-projet lancée en 2012 dans le sillage d'une équipe-projet antérieure appelée Vasy. « Un système parallèle asynchrone repose sur plusieurs agents (ou processus) qui travaillent de façon largement indépendante, sauf quand ils doivent se synchroniser ou communiquer par le biais de messages. »
La complexité de ces systèmes provient du fait que ces interactions sont difficiles à prévoir (on parle de "non-déterminisme"). Elle s'accroît à mesure que les progrès techniques les font évoluer. « Les premiers ordinateurs fonctionnaient avec un seul processeur, qui exécutait ligne à ligne ce qui lui était imposé par le programme, rappelle le chercheur Hubert Garavel. Mais l’augmentation de performance conduit à avoir plusieurs processeurs et des programmes capables de s'exécuter en même temps, ce qui fait naître d’épineux problèmes de synchronisation et de communication. » Il faut organiser correctement les différentes tâches pour éviter des blocages ou des corruptions de données.
Sémantique du parallélisme : une théorie riche mais peu comprise
« Le parallélisme est un concept universel, souligne Hubert Garavel. Vous en trouvez dans beaucoup d’activités humaines, notamment la gestion des organisations et des groupes de travail, pour laquelle on doit mettre en place des mécanismes de concertation et de planification pour coordonner au mieux les tâches de chacun et éviter les situations bloquées ou incohérentes. Il y en a aussi dans les téléphones et les ordinateurs portables, qui comportent désormais plusieurs cœurs et des coprocesseurs afin d’exécuter simultanément des actions très diverses : tâches de l’utilisateur, opérations du système d’exploitation, affichage, communications réseau... Il est aussi présent dans les objets connectés et les bâtiments intelligents. » Pour les supercalculateurs, on parle de "parallélisme massif" : ils s'appuient sur des dizaines ou des centaines de milliers de processeurs différents.
Des méthodes à la portée des acteurs de l'industrie
La théorie du parallélisme ("concurrency theory" en anglais) propose des modèles généraux pour décrire les interactions, prédire leur comportement et vérifier leur correction. Elle rassemble les résultats des recherches menées par de grands pionniers de l’informatique, dont plusieurs ont été distingués par le prix Turing. C’est sur ce riche, mais ardu, corpus théorique que se fondent les travaux de l’équipe-projet Convecs. « On s'efforce de mettre ces méthodes à la portée des acteurs de l'industrie, en leur fournissant des langages et des outils qui peuvent être appris et maîtrisés sans avoir de connaissances pointues dans les équations mathématiques », indique Radu Mateescu. « Il s’agit de décrire le fonctionnement des systèmes parallèles asynchrones sous une forme intelligible par des humains, tout en étant suffisamment rigoureuse pour être comprise sans ambiguïté par des machines. »
La vérification peut ensuite débuter, avec l'aide d'outils de vérification compositionnelle, qui permettent de décomposer les processus les plus complexes en fragments plus simples à analyser. Un objectif majeur de Convecs est en effet « de tester et de valider la plupart des scénarios de comportement en amont, avant que les systèmes soient déployés sur le terrain », conclut Frédéric Lang, chercheur de l’équipe Convecs.
Découvrir quelques membres de l'équipe-projet Convecs
Radu Mateescu
Directeur de recherche et responsable de l'équipe-projet Convecs
« Je voulais avoir la possibilité de faire des recherches sur le long terme. C'est une opportunité qui devient assez rare. Mais c'est le cas avec Convecs, car Inria est une institution capable d’investir sur le temps long. »
Illustrations : © Inria / Artiste Designer : Aurélie Bordenave
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Radu Mateescu
Biographie expresse 1/2
1993 – Diplôme d'ingénieur à l'Université Polytechnique de Bucarest (UPB) et projet de recherche au laboratoire Verimag de l'Université Grenoble Alpes (UGA) dans le cadre d'un programme européen.
1997 – Thèse de doctorat sur la « Vérification des propriétés temporelles des programmes parallèles » à l'Université de Grenoble.
1997-1998 – Postdoctorat au CWI (Amsterdam) ;
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Radu Mateescu
Biographie expresse 2/2
1998-2011 – Chargé de recherche Inria au sein de l'équipe-projet Vasy ;
2002 - Prix « Technologies de l'information » de la Fondation Rhône-Alpes ;
2012 – Directeur de recherche et responsable de l'équipe-projet Convecs.
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Hubert Garavel
Directeur de recherche
« Pendant mes études, je me suis pris de passion pour la théorie du parallélisme, notamment les idées portées par Tony Hoare et Robin Milner, et j’ai eu la chance d’effectuer ma thèse dans l’équipe de Joseph Sifakis pour combiner les idées de ces scientifiques de renom et tenter de les mettre à la portée du plus grand nombre. »
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Hubert Garavel
Biographie expresse 1/2
1986 – Diplôme d'ingénieur en informatique à l'Ensimag (École nationale supérieure d'informatique et de mathématiques appliquées de Grenoble) ;
1989 – Thèse de doctorat (Compilation et vérification de programmes Lotos), à l'université de Grenoble, en partenariat avec Inria Paris - Rocquencourt ;
1990 – Prix IBM France du jeune chercheur en informatique ;
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Hubert Garavel
Biographie expresse 2/2
1993-2011 – Chargé de recherche, puis directeur de recherche Inria dans les équipes-projets Spectre, Vasy-RA (commune entre Inria et Bull), puis Vasy ;
2011 – Prix Gay-Lussac Humboldt ;
Depuis 2012 – Membre de l’équipe-projet Convecs et de l’équipe Depend (Université de la Sarre).
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Frédéric Lang
Chargé de recherche
« Enfant et adolescent, j'aimais beaucoup résoudre des problèmes présentés sous forme de jeu. Je retrouve cette dimension de jeu de raisonnement dans la recherche et c'est quelque chose qui me motive et me plaît énormément. »
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Frédéric Lang
Biographie expresse
1994 – Diplôme d'ingénieur en informatique à Telecom Nancy ;
1998 – Thèse de doctorat (Modèles de la bêta-réduction pour les implantations) à l'École normale supérieure de Lyon ;
1999-2000 – Post-doctorat (professeur d'informatique) à Wesleyan University (Connecticut, États-Unis) ;
2000-2001 – Ingénieur expert au sein de l'équipe-projet Vasy ;
Depuis 2001 – Chargé de recherche Inria au sein des équipes-projet Vasy, puis Convecs.
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Wendelin Serwe
Chargé de recherche
« Faire de la recherche dans une équipe comme Convecs me permet de prendre le temps d'effectuer des travaux longs, très approfondis, sur des sujets qui ont du sens pour moi et que j'ai choisis. »
<> Cliquez sur les flèches pour faire défiler leurs parcours.
Wendelin Serwe
Biographie expresse
1998 – Double diplôme de mastère (Ensimag et université de Karlsruhe en Allemagne) ;
2002 – Thèse de doctorat sur « La programmation logico-fonctionnelle concurrente » à l'Institut national polytechnique de Grenoble (Grenoble INP).
2002-2003 – Postdoctorat sur la vérification des applications Java card (exécutables sur une carte à puce) au centre Inria Rennes – Bretagne Atlantique.
Depuis 2004 – Chargé de recherche Inria au sein des équipes-projet Vasy, puis Convecs.
<> Cliquez sur les flèches pour faire défiler leurs parcours.
En savoir plus
Prix Inria 2021
Découvrez les chercheurs Inria récompensés