Nous décrivons ici un exemple, issu du milieu de la carte à puce, décrivant le contrôle d'accès. Nous présentons la spécification informelle, le modèle fonctionnel B qui lui est associé, le noyau de sécurité généré par l'outil MECA, et les tests produits par Leirios Test Generator. Nous donnons également une implantation de l'exemple, et les tests produits au format Java ainsi que le pilote de test.
L'application décrit un porte-monnaie électronique qui est destiné à être embarqué sur une carte à puce. Ce porte-monnaie est composé de deux codes PIN, permettant d'identifier la banque ou le porteur de la carte.
Le cycle de vie de la carte est composé de trois modes : personnalisation, utilisation, invalide.
Avant de commencer quoi que ce soit avec la carte, il faut démarrer une session à partir d'un terminal donné (méthode beginSession(Terminal)).
La phase de personnalisation correspond aux réglages, par un terminal administratif (assimilé à un fabricant de carte), des codes PIN (setBpc, setHpc). Dès que les deux codes PIN sont fixés, la carte passe en mode utilisation.
Lorsque l'utilisateur bloque son code PIN, au bout de trois essais, la banque doit s'authentifier (authBank) pour pouvoir ensuite réinitialiser le code PIN de l'utilisateur (setHpc). Si la banque échoue son identification après trois essais également, la carte repasse en mode personnalisation. C'est le constructeur (terminal administratif) qui devra refaire la procédure de personnalisation.
Une session qui se termine annule toutes les authentifications précédemment réalisées sur la carte.
Le crédit est autorisé si le porteur s'est authentifié au préalable, sur un terminal bancaire (on supposera que le crédit sur la carte effectue un débit sur un compte bancaire non représenté ici). Pour le paiement en lui-même ou la consultation du solde, il n'est pas nécessaire que le porteur se soit authentifié. Le plafond du porte-monnaie est fixé à 3000 unités (centimes). Il n'est pas possible d'effectuer un paiement si le solde du porte-monnaie est insuffisant.
La classe de l'objet est la classe "Bankcardkernel". Les méthodes de l'objet sont :
La classe Terminal contient les 4 constantes statiques de type Terminal : ADMIN, BANK, PDA et NONE.
La politique de sécurité décrit les permissions d'exécution des opérations pour chacun des terminaux.
Tous les terminaux (BANK, ADMIN ou PDA) peuvent démarrer et fermer une session. Il n'est possible de fixer le code PIN de la banque qu'en étant un terminal administratif et si la carte est en phase de personnalisation. Le code PIN du porteur peut etre fixé soit par un terminal administratif lorsque la carte est en phase de personnalisation, ou alors par un terminal bancaire préalablement authentifié lorsque la carte est bloquée. Un terminal bancaire est autorisé à s'authentifier lorsque la carte n'est pas en phase de personnalisation, ni en phase d'utilisation. Il est possible de vérifier le code PIN du porteur à partir d'un terminal bancaire, lorsque la carte est en phase d'utilisation. Le crédit ne peut s'effectuer que sur un terminal bancaire. Le débit ou la consultation peuvent s'effectuer depuis un terminal bancaire ou un PDA.
On commence par les deux fichiers donnés en entrée de MECA :
MECA produit le noyau de sécurité suivant :
Pour utiliser ces 3 fichiers, après les avoir placés dans un même répertoire, il faut les compiler :
javac *.javaet lancer le fichier "e_purse_kernel.java" :
java e_purse_kernelOn obtient à l'écran la liste des tests ayant réussi et deux ayant échoué.