UNIVERSITE DE LA MANOUBA
Matière : Génie Logiciel II
-----¤¤¤¤-----
Classes : II.2C,F
ECOLE NATIONALE DES SCIENCES DE L'INFORMATIQUE
A-U : 2017-2018
TD1 - La méthode B
Partie1 : Machines Abstraites et preuves de cohérence
Exercice 1
Nous souhaitons modéliser, avec la méthode B AMN, le comportement d’un système qui simule le fonctionnement du réseau social « Facebook ». Ce réseau social est représenté sous forme d’un graphe G= (P, R) avec P est l’ensemble des participants (les sommets) et R représente l’ensemble des relations d’amitié entre les participants (les transitions). 1. Définir les ensembles abstraits et les variables nécessaires 2. Donner l’Invariant 3. Décrire l’initialisation 4. Décrire les opérations suivantes :
a. Ajouter un participant b. Supprimer un participant (il faut supprimer toutes les relations d’amitié avec ce
participant)
c. Ajouter une relation d. Supprimer une relation e. Vérifier si deux participants sont amis f. Calculer le nombre des liens d’amitié pour un participant
5. Ecrire toutes les obligations de preuve et Calculer les obligations de preuve pour l’initialisation et l’opération « Vérifier si deux participants sont amis »
Exercice 2
Nous souhaitons spécifier un système de gestion d’une bibliothèque. Les entités traitées sont :
– des livres, des exemplaires de livre, des abonnés
Les règles (propriétés) sont :
– Un exemplaire ne peut pas être emprunté par plusieurs abonnés – Un abonné ne peut emprunter plus d’un certain nombre d’exemplaires.
Les opérations sont :
Publicité
– Création et suppression d’un livre, d’un exemplaire de livre, d’un abonné – Emprunt d’un exemplaire par un abonné (livre et abonné sont des paramètres en
entrée)
– Retour d’un exemplaire emprunté (exemplaire et abonné sont des paramètres en
entrée)
– Recherche d’un exemplaire libre d’un livre (prend en entrée un livre et retourne
l’exemplaire)
1. Donner un diagramme de cas d’utilisation UML associé à ce système. 2. Spécifier, en utilisant la méthode B, le comportement de ce système.
1/3
3. Ecrire les obligations de preuve pour la correction (cohérence) de la machine.
Exercice 3
Le couple producteur-consommateur est un exemple classique de la programmation concurrente. Le producteur est un processus chargé d'emmagasiner des données. Le consommateur est un processus chargé de les déstocker.
Un tampon est partagé entre les deux processus pour assurer la mémorisation des données produites non encore consommées. Ce tampon est borné et ne peut recevoir qu’un nombre limité (noté Maxi) de données. Ainsi, le producteur ne pourra pas déposer une information dans le tampon s'il n'y a plus de place libre. De même, le consommateur ne pourra pas retirer une information depuis le tampon s'il est vide.
Pour garantir l'intégrité des opérations d'ajout et de retrait, le tampon doit être manipulé en exclusion mutuelle. Pour ce faire, une variable (un sémaphore qui peut prendre les valeurs 0 ou 1) appelée mutex est utilisée. Cette dernière représente un jeton que le processus doit avoir pour pouvoir manipuler le tampon. Pour savoir quel processus détient le jeton mutex, une autre variable (un drapeau) appelée drap est utilisée. La valeur de cette dernière peut être :
Prod : signifie que c’est le producteur qui a pris le jeton, Cons : signifie que c’est le consommateur qui a pris le jeton, Null : signifie que le jeton est libre. Pour déposer une donnée dans le tampon, le producteur doit prendre d'abord le jeton mutex (donc drap prend la valeur Prod) et doit le relâcher une fois il a terminé (drap prend la valeur Null). De son côté, le consommateur doit prendre le jeton (donc drap prend la valeur Cons) afin de pouvoir retirer une donnée et le relâche (et drap prend la valeur Null) une fois il a terminé.
Le système qui va gérer la synchronisation entre ces deux processus doit vérifier les
propriétés suivantes :
P1 : « Absence de famine : si un processus (producteur ou consommateur) veut manipuler
le tampon, alors il finira par le faire »
P2 : « Exclusion mutuelle : pas de manipulations (dépôt ou retrait) simultanées du tampon
par les deux processus » La machine Process suivante représente un modèle abstrait pour le système de gestion de la
Publicité
synchronisation entre les processus Producteur et Consommateur.
Travail à faire : Compléter cette machine abstraite pour garantir une bonne synchronisation
entre les deux processus.
MACHINE
Process
SETS
Stock; Processes = {Producteur, Consommateur}; Drapeau = {Prod, Conso, Null}
CONSTANTS
Maxi
PROPERTIES Maxi ∈ NAT VARIABLES
tampon, mutex, drap
INVARIANT
2/3
tampon ⊆ Stock ∧ …………………………… INITIALISATION
……………………………
OPERATIONS
PrendreJeton (pp) = PRE pp ∈ Processes ∧………………… THEN ……………………………
END;
RelacherJeton (pp) = PRE pp ∈ Processes ∧……………………………… THEN ……………………………
END;
Publicité
Deposer (pp, xx) = PRE pp ∈ Processes THEN ……………………………………………….
∧ xx
∈
Stock …………………………….
END;
xx <-- Retirer (pp)= /*xx est la donnée retirée*/ PRE pp ∈ Processes ∧ …………………………… THEN ……………………………………………….
……………………………………………….
END
END
Exercice 4
On souhaite spécifier le fonctionnement d’une machine qui délivre des boissons. Le fonctionnement est décrit comme suit : La machine peut être en arrêt ou en marche. Il y a un bouton pour mettre en marche et arrêter la machine Les actions suivantes n’ont d’effet que si la machine est en marche :
- L’usager peut sélectionner une certaine boisson. Il y en a 3 : café, thé ou chocolat. - Après la sélection, l’appareil affiche la somme demandée. - L’usager peut alors payer avec les différentes pièces de monnaie. - L’appareil affiche la somme restante. - Dès qu’une somme suffisante est versée, l’appareil délivre la boisson à l’usager. - L’appareil rend éventuellement la monnaie. - On ne peut commander une nouvelle boisson que si le Goblet a été retiré de son emplacement.
- A tout moment après la sélection de la boisson et avant que le distributeur ne délivre la boisson, l’usager peut annuler la commande. L’appareil doit alors rendre l’argent déjà versé s’il y a lieu. Travail à faire : Spécifier, en utilisant la méthode B, le comportement de ce système.
Partie2 : Le raffinement et la preuve du raffinement
Pour chaque exercice de la partie 1. Il est demandé de :
1. Raffiner la machine abstraite obtenue jusqu’à aboutir à une implémentation.
2. Ecrire et calculer les obligations de preuve de chaque raffinement.
3/3