Equipe de recherche VASY

Validation de systèmes, recherche et application

Présentation de l'équipe

L'équipe-projet VASY participe à l'effort international pour produire des systèmes fiables à l'aide de méthodes formelles et d'outils logiciels adéquats. Le domaine d'application visé est large, incluant matériel, logiciel et télécommunications. Les activités de VASY concernent les techniques de description formelle et les méthodologies associées : compilation, prototypage rapide, simulation, vérification (partielle ou exhaustive) et test.

Axes de recherche

VASY a pour objectif de concevoir des méthodes et des logiciels de qualité industrielle permettant de détecter les erreurs au plus tôt et d'accroître la confiance dans les systèmes étudiés. En particulier, VASY contribue activement au développement de la boîte à outils CADP pour l'ingénierie des protocoles.

Les recherches de VASY s'orientent vers trois directions :

  • Technologie des langages et compilation.

    VASY travaille sur les langages de spécification pour la description de systèmes concurrents, en se concentrant sur les langages disposant d'une sémantique rigoureuse et de propriétés de compositionnalité adéquates, et notamment sur les algèbres de processus, qui allient une grande expressivité à de solides fondements théoriques. VASY développe des compilateurs pour le langage LOTOS (une norme ISO combinant les meilleures caractéristiques des calculs CCS de Milner et CCS de Hoare) qui sont utilisés dans de nombreuses études de cas à des fins d'exécution, de simulation, de prototypage rapide et de test.

    Outre les algèbres de processus ``classiques'', VASY explore aussi de nouveaux langages de spécification (tels que E-LOTOS et LOTOS NT) conçus pour obtenir une meilleure acceptation dans l'industrie. Ces langages combinent les caractéristiques des algèbres de processus (pour la description du parallélisme) avec les caractéristiques des langages fonctionnels et impératifs (pour la description des types de données et des calculs séquentiels). VASY contribue à la définition, à l'étude et à l'implémentation de E-LOTOS et LOTOS NT, notamment avec le compilateur TRAIAN ainsi qu'avec le modèle et les outils NTIF pour les systèmes de transitions symboliques.

  • Technologie des modèles et vérification.

    Indépendemment de tout langage, VASY travaille aussi à des méthodes pour la validation et la vérification de systèmes concurrents. Le but est de développer des modèles, des algorithmes et des composants logiciels génériques, c'est-à-dire non liées à un langage de spécification particulier. Les recherche actuelles portent sur :

    • La représentation et la manipulation efficace de très grands systèmes de transitions étiquetées ;
    • Le model-checking et la génération de diagnostics pour le mu-calcul modal avec passage de valeurs, basés sur la résolution efficace à la volée de systèmes d'équations booléennes ;
    • Le calcul efficace de la bisimulation forte et de branchement pour des systèmes de transitions non-déterministes, probabilistes et stochastiques ;
    • La vérification compositionnelle pour des systèmes de processus communicants ;
    • Le model-checking massivement parallèle sur des réseaux de stations de travail et des grappes de PC.

  • Etudes de cas et applications industrielles.

    La confrontation permanente des solutions développées par VASY à des problèmes réalistes (principalement issus de besoins industriels) permet d'identifier de futurs axes de recherche. VASY collabore avec de grandes entreprises comme Airbus, Bull et STMicroelectronics.

Relations industrielles et internationales

Mots-clés : Systèmes répartis Parallélisme Temps réel Sémantique Méthodes formelles Spécification Programmation parallèle Génération de code Logique temporelle Vérification de programme Lotos E-lotos

Equipes de recherche du même thème :

Siège et centres de recherche Inria

Accès direct

Social