Le projet a comme objectif la modélisation des systèmes réactifs,
parallèles et communicants. Il étudie aussi la définition et l’implémentation de
langages et de méthodes formelles de vérification basés sur ces modèles.
La classe de modèles adoptée est celle des calculs de processus, formalismes
algébriques simples pour la représentation des systèmes distribués et des processus
concurrents.
Une autre classe de modèles
importante est celle des formalismes réactifs synchrones, dont font
partie les langages Esterel et RC.
Ce type de programmation est particulièrement
adapté aux systèmes temps réel, manipulant des événements logiques avec préemption.
Les principaux domaines d’application visés couvrent les protocoles, les
systèmes et algorithmes répartis dans le cas asynchrone, les contrôleurs
logiciels ou matériels et les systèmes embarqués dans le cas synchrone.
Meije est un projet commun avec le Centre de mathématiques appliquées (CMA) de
l’École des mines de Paris (ENSMP) à Sophia Antipolis.
Axes de recherche
L’étude fondamentale des systèmes communicants s’oriente désormais plus particulièrement
vers la combinaison des paradigmes de la modélisation
parallèle avec ceux de la programmation fonctionnelle
(communication de processus ou de leurs adresses en
arguments, processus mobiles).
Pour Esterel, deux technologies distinctes de compilation permettent la
production de code basé au choix sur des machines à états finis ou sur des
systèmes d’équations booléennes. Dans le second cas, des nouvelles techniques
d’analyse permettent désormais la caractérisation exacte de la causalité
constructive entre événements. Le système est alors également interfacé avec
des systèmes de synthèse de circuits matériels.
Les systèmes de vérification Auto/Graph et Fc2Tools
(analyse par réduction/abstraction de systèmes de transitions et de réseaux)
disposent de nouveaux modules
algorithmiques efficaces basés sur des représentations symboliques de
données (BDD). Ces systèmes sont en particulier interfacés avec Esterel
dans un environnement graphique Xeve et
exploitent donc des modèles tant synchrones qu’asynchrones.
L’extension Reactive C du langage C sert d’assembleur réactif pour la
définition d’autres formalismes de programmation, comme les objets ou les
scripts réactifs. Ceux-ci permettent l’animation comportementale
d’object brokers en particulier.
Relations internationales et industrielles
Le compilateur Esterel
(version binaire) est disponible par ftp avec son environnement de
simulation graphique Xes. Une version industrielle est commercialisée
par la société Simulog.
Les outils de vérification Fc2 Tools et les
développements logiciels autour du langage RC sont également
disponibles par ftp sur le site
http://www.inria.fr/meije/meije-fra.html.
Participation au projet Esprit LTR Syrf, ainsi qu’à plusieurs CTI du Cnet.
Au niveau national, participation au PRC " PRS " du CNRS, au groupement
" C2A Synchrone " et à l’action de développement
Génie 2.
Relations contractuelles avec Dassault Aviation, Thomson, Alcatel et autres
industriels utilisateurs d’Esterel. Des développements importants
autour du langage RC sont effectués par Soft Mountain,
société de technologie de l’INRIA.
Collaborations académiques avec les universités de Berkeley, d’Édimbourg, de
Pise, du Sussex, d’Aalborg et avec le CWI ; participation au laboratoire franco-chinois
cofondé par l’INRIA.
