Détail d'une fiche   Version PDF

CONVECS (SR0619CR)

Construction de systèmes concurrents vérifiés

CONVECS (SR0494HR) →  CONVECS


Statut: Décision signée

Responsable : Radu Mateescu

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : A1.3.5. Cloud , A2.1.1. Sémantique des langages de programmation , A2.1.6. Programmation concurrente , A2.1.7. Programmation distribuée , A2.4.1. Analyse , A2.4.2. Model-checking , A2.5. Génie logiciel , A2.5.1. Architecture, conception , A2.5.4. Maintenance, évolution , A2.5.5. Test logiciel , A6.1.3. Modélisation discrete (multi-agent, individus centrés) , A7.1.1. Algorithmique distribuée , A7.1.3. Algorithmique des graphes , A7.2. Logique , A8.9. Evaluation de performances

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : B5.1. Usine du futur , B5.4. Microélectronique , B6.1.1. Génie logiciel , B6.3.2. Protocoles , B6.4. Internet des objets , B6.5. Systèmes d'information , B6.6. Systèmes embarqués , B7.2.1. Véhicules intelligents

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/01/2014 -> 31/12/2024
Dates d'évaluation : 24/03/2016 , 20/03/2019 ,

Etablissement(s) de rattachement : UGA
Laboratoire(s) partenaire(s) : LIG (UMR5217)

CRI : Centre Inria de l'Université Grenoble Alpes
Localisation : Centre de recherche Inria de l'Université Grenoble Alpes
Code structure Inria : 071106-1

Numéro RNSR : 201221019Z
N° de structure Inria: SR0619CR

Présentation

CONVECS est une équipe de recherche travaillant sur la modélisation et la vérification formelle de systèmes concurrents asynchrones, qui s'instancient dans de nombreux domaines (protocoles de communication, algorithmes distribués, nuages de calcul, systèmes Globalement Asynchrones et Localement Synchrones - GALS, etc.). A ce titre, CONVECS propose de nouveaux langages formels pour spécifier le comportement et les propriétés des systèmes concurrents, et conçoit des algorithmes de vérification et des outils efficaces pour des machines séquentielles et des infrastructures de calcul distribuées.


Axes de recherche

Le parallélisme asynchrone devient omniprésent, allant de l'échelle microscopique des systèmes embarqués et processeurs multicoeur à l'échelle macroscopique des grilles et nuages de calcul. Dans la course pour augmenter la performance tout en diminuant la consommation énergétique, les constructeurs d'équipements de calcul s'orientent vers le modèle asynchrone, dans lequel plusieurs entités opèrent de manière concurrente à des vitesses différentes, communiquent et se synchronisent. Le prix à payer pour augmenter la performance est une conception plus complexe, qui ne peut être traitée qu'en utilisant la vérification formelle.

Pour améliorer l'état de l'art dans la conception et l'analyse des systèmes parallèles asynchrones, CONVECS suit un programme de recherche consistant en cinq axes de recherche interdépendants :

  1. Aller des langages formels de haut niveau vers des implémentations parallèles.
  2. Algorithmes de vérification parallèles et distribués.
  3. Prise en compte des aspects temporisés, probabilistes et stochastiques.
  4. Architectures à base de composants pour la vérification à la volée.
  5. Etudes de cas et applications réalistes.

Relations industrielles et internationales

L'équipe CONVECS est impliquée dans plusieurs groupes de travail internationaux exerçant leur activité dans le domaine des méthodes formelles et de la vérification :

  • FMICS ERCIM Working Group on Formal Methods for Industrial Critical Systems
  • IFIP Working Group 1.8 on Concurrency Theory
  • AVACS consortium on Automatic Verification and Analysis of Complex Systems
    (implication de Hubert Garavel en collaboration avec l'Université de la Sarre)

Les membres de CONVECS développent et maintiennent la boîte à outils CADP, un environnement de haut niveau pour la vérification des systèmes parallèles asynchrones. CADP est largement utilisée à la fois en milieu industriel et académique. CONVECS collabore avec plusieurs industriels intéressés par la vérification formelle, comme Orange Labs, Nokia et Innovista Sensors.