Up : Sommaire Previous : Documentation de Projet

Click here for English.

Matrice de Traçabilité

L'objet de ce document est de tracer la prise en compte des exigences depuis le Cahier des Charges jusqu'au modèle B obtenu. Pour chaque exigence, cette matrice de traçabilité précise les informations suivantes :

• la référence de l'exigence; cette référence apparaît également dans le dossier de spécification fonctionnelle (planches SADT) et dans les modules B.

• le libellé associé à l'exigence analysée; ce libellé est issu du Cahier des Charges.

• la planche SADT du dossier de Spécification Fonctionnelle où est introduite cette exigence,

• le module B (machine abstraite ou implantation) qui modélise cette exigence soit dans la clause INVARIANT du composant (exigence globale), soit dans une opération sous la forme d'une post-condition (exigence locale).

CAHIER DES CHARGES SADT B

E1 Déclencher sa mise hors service lorsque sa caisse comporte un solde inférieur à 900 M2 Main : '(caisse-vde = TRUE panne-dst = TRUE) (etat-dab = Hors-service)'

E2 Déclencher sa mise hors service, lorsqu'il détecte une anomalie M2 Main : '(caisse-vde = TRUE panne-dst = TRUE) (etat-dab = Hors-service)'

E3 Mis hors service, il interdit l'insertion de carte M6.2 Fonctions-imp : autoriser-mise-hors-service

E4 La mise en service est faite manuellement M Main-imp : main : 'avnc montant-avance'

E5 L'opérateur est chargé du rechargement de la caisse M Main-imp : main : 'avnc montant-avance'

E6 En service et non sollicité par un client, il se trouve en mode veille M5.1 Controleur : determiner-nouvel-etat : 'courant = Veille (rslt = Hors-delai etat = Veille)

E7 Toute sollicitation d'un client entraîne une commutation en mode transaction M5.1 Controleur : determiner-nouvel-etat : 'courant = Veille (rslt = Valide etat = Traitement-carte)'

E8 Il revient en mode veille après la fin de la transaction M6 Controleur : determiner-nouvel-etat : 'courant = Confiscation-carte etat = Veille' 'courant = Restitution-carte (rslt = Valide etat = Veille)'

E9 Distribue les billets en fonction de la somme demandée M5 Fonctions-imp : controler-distribution-billets

E10 Vérifie, après chaque transaction, que la caisse comporte un solde supérieur à 900 M M2 Main-imp : main Dab-imp : tester-disposifs

E11 La corbeille reçoit les billets rejetés suite à un incident M5.4 Fonctions-imp : controler-distribution-billets

E12 La corbeille reçoit les billets non retirés par le client dans les 30 s M5.4 Fonctions-imp : controler-distribution-billets

E13 Vérification de la lisibilité des informations des cartes présentées M5.1 Lecteur : charger-carte : 'lisible : BOOL'

E14 Lecture des cartes présentées M5.1 Controleur : determiner-nouvel-etat : 'courant = Veille (rslt = Valide etat = Traitement-carte)'

E15 Vérification de la date de péremption par rapport à la date du jour M5.1 Lecteur-imp : validation-infos-carte

E16 Restitution des cartes bancaires M6 Lecteur : rendre-carte : 'carte := KO'

E17 Vérification du code saisi par le client par rapport à celui enregistré sur la carte M5.2 Clavier-code-imp : validation-code

E18 Demande de reconnaissance de la carte M5.1 B-Site-central : b-interroger-carte : 'val := bool(crt : b-no-clients)'

E19 Demande d'autorisation de la carte, ainsi que le solde du compte correspondant M5.1 B-Site-central : b-interroger-carte

E20 Calcul du montant maximum du retrait auquel le client a droit M5.3 Fonctions-imp : autoriser-saisie-somme

E21 Distribution des billets par le distributeur mécanique M5.4 B-Distributeur : b-distribuer-billets : 'b-presentoir := sld'

E22 Billets extraits de la caisse M5.4 B-Distributeur : b-distribuer-billets : 'caisse := caisse - sld'

E23 Rejets des billets dans la corbeille M5.4 B-Distributeur : b-jeter-billets : 'b-corbeille := b-corbeille + b-presentoir'

E24 Détection des anomalies sur ses éléments M Fonctions : tester-dab : 'tst-dab : BOOL'

E25 Mise hors service M Dab-imp : fermer-dab

E26 Signaler au client que le DAB est disponible M5.1 Fonctions : autoriser-entree-carte : 'message := Entrez-votre-carte'

E27 Signaler au DAB l'introduction d'une carte M5.1 B-Lecteur : b-test-carte-presente : 'pre : BOOL' b-charger-carte : 'charger := pre'

E28 Transmettre au DAB les informations contenues sur la carte M5.1 B-Lecteur : b-charger-carte : 'crt := nro-carte' 'cdd : 0..9999' 'lmt : Dmin..Dmax'

E29 Signaler au client que le DAB attend qu'il saisisse son code M5.2 Fonctions-imp : autoriser-saisie-code

E30 Transmettre au DAB le code saisi M5.2 B-Clavier-code : b-code-saisi : 'code := cde'

E31 Signaler au client de saisir sa somme M5.3 Fonctions : autoriser-saisie-somme : 'message := Entrez-somme'

E32 Transmettre au DAB la somme saisie M5.3 B-Clavier-somme : b-somme-saisie : 'somme := som'

E33 Signaler au client que sa carte est rendue M6 Fonctions-imp : autoriser-restitution-carte

E34 Signaler au client que sa carte est confisquée M6 Fonctions-imp : autoriser-confiscation-carte

E35 Signaler au client que les billets sont disponibles M5.4 Fonctions : autoriser-distribution-billets : 'message := Prenez-vos-billets'

E36 Signaler au DAB que les billets sont pris M5.4 B-Distributeur : b-retraits-billets : 'rslt := TRUE'

E37 Signaler au client que les billets sont confisqués M5.4 Ecran : message-restitution-carte : 'etat = Distribution-billets (rslt = Hors-delai n-msg = Billets-confisques)'

E38 Signaler au DAB qu'un de ses éléments est en panne M Main-imp : main : 'oper ordre-operateur'

E39 Signaler au DAB sa remise en service M Main-imp : main : 'initialiser-dab (avnc)'

E40 Autorise ou non la transaction selon la reconnaissance de la carte, son autorisation et sa date de péremption M5 Controleur : determiner-nouvel-etat : 'courant =Traitement-carte (rslt = Valide etat = Traitement-code)'

E41 Autorise ou non la transaction selon le code saisi M5 Controleur : determiner-nouvel-etat : 'courant = Traitement-code (rslt = Valide etat = Traitement-somme)'

E42 Autorise ou non la transaction selon la somme demandée M5 Controleur : determiner-nouvel-etat : 'courant = Traitement-somme (rslt = Valide etat : Distribution-billets)'

E43 Autorise ou non la transaction selon le nombre d'essais de code ayant échoués M5 Controleur : determiner-nouvel-etat : 'courant = Traitement-code (rslt = Invalide etat = Confiscation-carte) '

E44 Redemande le code, s'il est erroné et si le nombre d'essais est inférieur ou égal à 2 M5 Controleur : determiner-nouvel-etat : 'courant = Traitement-code (rslt = Nouvel etat = Traitement-code) (rslt = Dernier etat = Traitement-code)'

E45 Restitue la carte si la date de péremption est dépassée M5.1 Controleur : determiner-nouvel-etat : 'courant = Traitement-carte (rslt = Perimee etat = Restitution-carte)'

E46 Restitue la carte si elle est inconnue du Site Central M5.1 Controleur : determiner-nouvel-etat : 'courant = Traitement-carte (rslt = Invalide etat = Restitution-carte)'

E47 Restitue la carte si elle est illisible M5.15 Controleur : determiner-nouvel-etat : 'courant = Traitement-carte (rslt = Illisible etat = Restitution-carte)'

E48 Restitue la carte en cas d'incident M6 Dab-imp : fermer-dab Controleur : determiner-nouvel-etat : 'courant = Traitement-code (rslt = Incident etat = Restitution-carte)' 'courant = Traitement-somme (rslt = Incident etat = Restitution-carte)' 'courant = Distribution-billets (rslt = Incident etat = Restitution-carte)'

E49 Restitue la carte si le montant maximum du retrait est inférieur à 100 strictement M5 Controleur : determiner-nouvel-etat : 'courant = Traitement-carte (rslt = Epuisee etat = Restitution-carte)'

E50 Confisque la carte en cas d'interdiction M6 Controleur : determiner-nouvel-etat : 'courant = Traitement-carte (rslt = Interdite etat = Confiscation-carte)'

E51 Confisque la carte au bout de la 3ème tentative de saisi de code avec la même carte M6 Controleur : determiner-nouvel-etat : 'courant = Traitement-code (rslt = Invalide etat = Confiscation-carte)'

E52 Confisque la carte si elle n'est pas reprise par le client dans les 30 s M6 Controleur : determiner-nouvel-etat : 'courant = Restitution-carte (rslt = Hors-delai etat = confiscation-carte)'

E53 Demande le débit du compte au S.C. M5.4 B-Site-central : b-debiter-carte : 'b-solde(crt) := b-solde(crt) - som'

E54 Informe le client que son code est erroné M5.2 Ecran : message-controler-code : 'etat = Traitement-code (rslt = Nouvel n-msg = Nouvel-essai) (rslt = Dernier n-msg = Dernier-essai)' message-confiscation-carte : 'etat = Traitement-code (rslt = Invalide n-msg = Code-invalide)'

E55 Informe le client que le DAB est hors service M6 Fonctions : autoriser-mise-hors-service : 'message := En-panne'