Gérald POINT
Gérald Point Ingénieur de Recherches (CNRS)

Équipe LaBRI : Méthodes formelles
Fonction administrative :
Page personnelle : http://dept-info.labri.fr/~point
Courrier électronique : gerald.pointarobaselabri.fr
Bureau : 260
Tél : +33 (0)5 40 00 38 76


Recherche

Rattaché au thème Modélisation et Vérification de l'équipe MF mes activités portent actuellement sur deux axes de recherche: le projet AltaRica et la représentation symbolique de systèmes infinis.

Le projet AltaRica: Ce projet a pour objectif le développement d'outils d'analyse et de compilateurs pour le langage de modélisation AltaRica. Sur ce thème mon rôle est d'intégrer au logiciel ARC les techniques développées dans MV afin de proposer à nos partenaires industriels un outil stable. Principales caractéristiques de ARC:
. Langage AltaRica étendu aux propositions de l'ACI Persée
. mu-calcul modal pour la spécification des propriétés calculées
. Représentation exhautive ou symbolique des espaces d'états des modèles AltaRica
. Compilation vers d'autres langages (p.ex. Scade/Lustre dans le cadre du projet européen ISAAC).

La logique de Presburger et les systèmes infinis: La logique de Presburger permet de décrire facilement des systèmes comportant un nombre infini d'états. Les ensembles d'états décrits dans cette logique peuvent être représentés symboliquement par des automates reconnaissant des mots binaires. Nous développons une suite d'outils autour cette logique et de la manipulation des automates binaires:
. API générique pour la manipulation d'ensembles définissables en logique de Presburger
. Définition/compilation d'un langage de haut-niveau, Armoise, pour la description d'ensembles
. Implementation des Automates Partagés
Un résultat important sur ce thème est l'implémentation du résultat de J. Leroux sur la synthèse de formules de Presburger à partir d'un automate binaire.

Extrait de publications













Page mise à jour le 13/08/2010 à 10:56