Détail d'une fiche   Version PDF

MOSCOVA (SR0075PR)

Mobilité, sécurité, concurrence, vérification et analyse

PARA (SR0270OR) →  MOSCOVA


Statut: Terminée

Responsable : Luc Maranget (Par intérim)

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : Aucun mot-clé.

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

Période : 01/01/2000 -> 31/12/2012
Dates d'évaluation : 22/03/2011

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria de Paris
Localisation : Rocquencourt
Code structure Inria : 021031-0

Numéro RNSR : 200018318R
N° de structure Inria: SR0075PR

Présentation

L'équipe-projet MOSCOVA développe deux axes de recherche sur les programmes concurrents : l'étude de langages pour les programmes distribués et mobiles, et l'analyse et la vérification de programmes multitâches. L'équipe-projet développe un système et un langage pour la réalisation d'applications distribuées et mobiles.


Axes de recherche

  • L'intégration fine de la concurrence à la programmation fonctionnelle, préservant le typage statique, le filtrage et la modularité.
  • Le contrôle des interactions par la portée statique des noms, réalisable par des méthodes cryptographiques classiques.
  • Une localisation hiérarchique des segments de programme, à la fois transparente pour l'application et contrôlable dynamiquement.
  • Des mécanismes permettant une gestion transparente des pannes.

Ces travaux sont fondés sur le join-calcul, une théorie de la concurrence adaptée aux systèmes répartis. L'équipe-projet poursuit plus généralement l'étude de la sémantique et de l'implantation des langages fonctionnels. Le coeur des activités de vérification de programmes concurrents est le développement d'outils d'analyse statique pouvant traiter automatiquement des codes de taille industrielle, localiser les zones d'interférence entre tâches concurrentes et détecter les risques de dépassement de borne ou de domaine de valeurs entières ou flottantes. Ces outils sont fondés sur la théorie de l'interprétation abstraite des programmes.


Relations industrielles et internationales

  • Une implémentation prototype du http://join.inria.fr est distribuée électroniquement.
  • Dans le cadre d'appel d'offre de l'agence spaciale européenne, MOSCOVA collabore avec la société danoise Terma A/S pour une étude sur une méthodologie pour la robustesse des logiciels spatiaux.
  • MOSCOVA participe au projet Esprit PEPITO Peer to Peer, Implementation and Theory), sur les applications distribuées symétriques. Ce projet regroupe des équipes de KTH (Seif Haridi, coordinateur), Cambridge (Peter Sewell), EPFL (Martin Odersky), SICS (Per Brand), UCL (Peter van Roy).
  • Plusieurs membres de Moscova sont responsables de cours à l'Ecole Polytechnique.