Titre du projet :
Méthodes de représentation des types abstraits algébriques en vue de la vérification de protocoles

Projet préparé à : INRIA projet SPECTRE / VERIMAG
Responsable de projet : Hubert Garavel
Mots-clés :
	compilation, génération de code, LOTOS, langages fonctionnels,
        méthodes formelles, réécriture de termes, spécification
        algébrique, traduction, type abstraits algébriques,
        vérification de programmes.



Résumé :
La vérification des logiciels fait actuellement l'objet de nombreuses recherches, dont le but ultime vise la qualité zéro défaut pour les logiciels complexes utilisés dans des applications critiques du point de vue de la sécurité.
Il est aujourd'hui admis que la fiabilité des logiciels passe par l'emploi de ``méthodes formelles'', au nombre desquelles figure le langage LOTOS. Ce langage est une norme ISO pour la description des systèmes parallèles. C'est un langage moderne qui se compose de deux parties distinctes~: une algèbre de processus et des types abstraits algébriques.
En Lotos, les données manipulées dans les programmes sont décrites par des types de données abstraits (inspirés du langage ACT-ONE). Les domaines de valeurs sont décrits par des sortes, les fonctions sur ces domaines sont décrites par des équations algébriques avec filtrage.
Dans le cadre du projet SPECTRE un compilateur efficace a été développé qui permet de traduire en langage C les types abstraits LOTOS. Toutefois, à l'heure actuelle, il existe des spécifications LOTOS que l'on n'est pas traiter, soit parce que le code engendré épuise, à l'exécution, toute la mémoire disponible, soit parce que ces spécifications comportent des sortes et fonctions génériques qui ne sont pas acceptées par le compilateur.
Pour le premier problème, nous étudions trois approches orthogonales~: l'intégration d'un ramasse-miettes, la représentation des termes sous une forme canonique et le compactage des structures de données engendrées. Nous présentons les résultats expérimentaux obtenus sur un ensemble de programmes LOTOS de taille significative.
Pour le second problème, nous étudions les questions liées à la compilation de la généricité et nous proposons un algorithme de ``mise à plat'' permettant de traiter les spécifications LOTOS comportant des types abstraits génériques.

BibTeX entry:

@dea{Sighireanu-95,

author =        {Mihaela Sighireanu},
title =         {M\'ethodes de repr\'esentation des types abstraits
                alg\'ebriques en vue de la v\'erification de protocoles},
school =        {Universit\'e Joseph Fourier (Grenoble)},
year =          {1995},

month =         jun,
annote =        {}
}

Please contact Mihaela Sighireanu for more details.



Back to Mihaela Sighireanu home page