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


Fabien Kuntz, Stéphanie Gaudan, Christian Sannino, Éric Laurent, Alain Griffault, et al.. Model-based diagnosis for avionics systems using minimal cuts. Martin Sachenbacher and Oskar Dressler and Michael Hofbaur. DX 2011, Oct 2011, Murnau, Germany. pp.138-145, 2011.

Alain Griffault, Gérald Point, Fabien Kuntz, Aymeric Vincent. Symbolic computation of minimal cuts for AltaRica models. 2011.

Jérôme Leroux, Gérald Point. TaPAS : The Talence Presburger Arithmetic Suite. Stefan Kowalewski and Anna Philippou. TACAS, 2009, York, United Kingdom. Springer, 5505, pp.182-185, 2009, Lecture Notes in Computer Science.

Sébastien Bardin, Jérôme Leroux, Gérald Point. FAST Extended Release. Computer Aided Verification, CAV'06, Aug 2006, Seattle, WA, United States. Springer Verlag, 4144, pp.63-66, 2006, Lecture Notes in Computer Science.

Gérald Point, Alain Griffault. On the partial translation of Lustre programs into the AltaRica language and vice versa. RR-1415-06. 2006.


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