Cartes à puces

Le développement de nouveaux composants plus puissants va permettre l’installation de plusieurs applications sur une même carte à puce. Elles pourront contenir des données aussi disparates que de la monnaie électronique, des crédits téléphoniques ou des informations médicales utiles en cas d’accident. L’apparition d’un nouveau langage de haut niveau adapté aux standards 7816 de la carte à puce, Java Card (sous-ensemble de Java), offre de nouvelles possibilités en matière de portabilité et de sécurité. Nous étudions la sémantique du langage Java Card afin de construire un environnement de développement et de vérification de programmes Java Card.