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 :
- Aller des langages formels de haut niveau vers des implémentations parallèles.
- Algorithmes de vérification parallèles et distribués.
- Prise en compte des aspects temporisés, probabilistes et stochastiques.
- Architectures à base de composants pour la vérification à la volée.
- 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 :
- Groupe de travail FMICS (Formal Methods for Industrial Critical Systems) d'ERCIM
- Groupe de travail 1.8 d'IFIP sur la Concurrency Theory
- Consortium AVACS (Automatic Verification and Analysis of Complex Systems)
- Forum Méthodes Formelles
Mots-clés : Algèbre de processus; logique temporelle; méthodes formelles; model checking; vérification parallèle et distribuée