Bull INRIA

Rapport d'activité Dyade/FormalCard 2001

Sommaire

Introduction

Cette page est un extrait du rapport d'activité complet du projet VASY, pour l'année 2001. Elle est composée des parties qui concernent l'action FORMALCARD.

Équipe

Projets INRIA VERTECS (Rennes)
VASY (Grenoble)
Personnels INRIA Hubert Garavel (Chargé de Recherche)
Thierry Jéron (Chargé de Recherche)
Frédéric Lang (Chargé de Recherche, à partir du 1er septembre 2001)
Vlad Rusu (Chargé de Recherche)
Ingénieurs Experts Dunkan Clarke (jusqu'au 31 mai 2001)
Frédéric Lang (jusqu'au 31 août 2001)
Chercheur Doctorant Elena Zinovieva, bourse INRIA
Personnels BULL/SCHLUMBERGER Jean-Michel Ravon
Kafia Zemirli (depuis mars 2001)

Programme de travail

La collaboration engagée en 1999 avec BULL SC&T (Smart Cards and Terminals), puis formalisée en juillet 2000 par le lancement de l'action FORMALCARD du GIE BULL-INRIA DYADE, s'est poursuivie en 2001 en dépit des changements liés au rachat de BULL SC&T par la société SCHLUMBERGER, à la fin du GIE DYADE et à l'arrêt du projet PAMPA (Rennes). Participent désormais à cette collaboration, à laquelle nous conservons le nom de FORMALCARD, les projets VASY et VERTECS de l'INRIA et la société SCHLUMBERGER.

FORMALCARD vise à réaliser des outils formels pour le développement des logiciels embarqués sur cartes à puces en vue de permettre leur certification. Cette certification répond à une demande croissante dans l'industrie, en raison de l'apparition de nouvelles normes (critères communs) qui préconisent, à partir d'un certain niveau de sécurité, l'utilisation de méthodes formelles. FORMALCARD comporte trois objectifs dont les deux premiers sont pris en charge par le projet VASY, le troisième étant confié au projet VERTECS :

État d'avancement

Les applications embarquées sur cartes à puces pouvant être représentées sous forme d'automates étendus avec des variables, nos travaux se sont donc focalisés sur les processus séquentiels présents dans les langages E-LOTOS et LOTOS NT. Pour les modéliser, nous avons conçu un formalisme appelé NTIF (New Technology Intermediate Form) destiné à servir de langage intermédiaire dans la compilation des processus E-LOTOS et LOTOS NT.

Dans son principe, NTIF permet de spécifier des automates définis par un ensemble d'états et de transitions et paramétrés par des variables d'état typées. A chaque transition sont attachés une action (permettant la communication avec l'environnement selon la sémantique du rendez-vous propre aux algèbres de processus) ainsi qu'un fragment de code séquentiel permettant de consulter et/ou de modifier la valeur des variables d'états ; ce fragment de code est exprimé avec les structures de contrôle usuelles des langages algorithmiques et fonctionnels.

Nous avons défini la syntaxe et la sémantique du langage NTIF, puis montré que NTIF était suffisamment expressif pour généraliser un grand nombre de formalismes pré-existants pour la spécification des automates étendus.

Nous avons ensuite conçu deux logiciels (appelés NT2IF et NT2DOT) pour traiter les descriptions NTIF modélisant des applications embarquées sur cartes à puces. Développés à l'aide du générateur de compilateurs SYNTAX et du compilateur TRAIAN, ces deux logiciels (6500 lignes de code) ont en commun les analyseurs lexicaux et syntaxiques, ainsi que les différentes phases de construction, de vérification et de transformation d'arbres abstraits. Leurs fonctionnalités sont les suivantes :

Dans le cadre de FORMALCARD, le langage NTIF et les outils associés ont été utilisés pour deux études de cas significatives portant sur les cartes à puces :


Back to the VASY Home Page