Spécification du noyau JavaCard2.0

Proposition de stage de DEA

Sujet:

Le noyau Javacard est un sous-ensemble du langage Java sans les threads ni les flottants dont le domaine d'application est le commerce électronique via des cartes à puces. Il s'agit dans ce stage de définir formellement ce noyau à partir de la spécification informelle: syntaxe et sémantique. Cette spécification servira de base à des outils de vérification qui assureront que les programmes écrits sont surs. Un environnement de programmation pour Java est par ailleurs en cours de définition à partir d'une sémantique opérationnelle via le système Centaur.

Ces travaux seront menés en collaboration avec un partenaire industriel et pourront être poursuivis en Thèse de Doctorat.

Encadrement: Isabelle Attali - Denis Caromel

Contact: Isabelle Attali

Tel : 04 93 65 79 10

E-mail : ia@sophia.inria.fr

Laboratoire d'accueil:

Projets CROAP et SLOOP, INRIA Sophia Antipolis

Objectifs:

  • étude de Java Card 2.0 (langage [1], API [2], exemples [3])
  • définition syntaxique de JavaCard
  • définition sémantique de JavaCard
  • identification et spécification des propriétés de sureté

    • Prérequis: langages à objets, sémantique des langages de programmation, Java

    Matériel: Station de travail

    Bibliographie:

    [1] Java Card 2.0 Language Subset and Virtual Machine Specification http://java.sun.com/products/javacard/
    [2] Java Card 2.0 Applications Programming Interfaces http://java.sun.com/products/javacard/
    [3] Java Card 2.0 Programming Concepts http://java.sun.com/products/javacard/
    [4] M. Russo ``Sémantique formelle pour le langage Java'', Rapport de stage DEA MDFI, Marseille, juin 97.

    Retour à la page du projet :

    Retour aux autres stages proposés dans le projet :

    Isabelle Attali
    Last modified: Mon Nov 3 11:53:53 MET