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 dun syst me qui
simule le fonctionnement du r seau social Facebook . Ce r seau social est repr sent sous
forme dun graphe G= (P, R) avec P est lensemble des participants (les sommets) et R
repr sente lensemble des relations damiti entre les participants (les transitions).
1. D finir les ensembles abstraits et les variables n cessaires
2. Donner lInvariant
3. D crire linitialisation
4. D crire les op rations suivantes :
a. Ajouter un participant
b. Supprimer un participant (il faut supprimer toutes les relations damiti 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 damiti pour un participant
5. Ecrire toutes les obligations de preuve et Calculer les obligations de preuve pour
linitialisation et lop ration V rifier si deux participants sont amis
Exercice 2
Publicité
Nous souhaitons sp cifier un syst me de gestion dune 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 dun certain nombre dexemplaires.
Les op rations sont :
Cr ation et suppression dun livre, dun exemplaire de livre, dun abonn
Emprunt dun exemplaire par un abonn (livre et abonn sont des param tres en
entr e)
Retour dun exemplaire emprunt (exemplaire et abonn sont des param tres en
entr e)
Recherche dun exemplaire libre dun livre (prend en entr e un livre et retourne
lexemplaire)
1. Donner un diagramme de cas dutilisation 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 quun
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.
Publicité
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 cest le producteur qui a pris le jeton,
Cons : signifie que cest 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
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
Publicité
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;
Deposer (pp, xx) =
PRE pp Processes
THEN &&&&&&&&&&&&&&&&&&.
' xx
Stock &&&&&&&&&&&.
Publicité
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 dune 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 nont deffet que si la machine est en marche :
- Lusager peut s lectionner une certaine boisson. Il y en a 3 : caf , th ou chocolat.
- Apr s la s lection, lappareil affiche la somme demand e.
- Lusager peut alors payer avec les diff rentes pi ces de monnaie.
- Lappareil affiche la somme restante.
- D s quune somme suffisante est vers e, lappareil d livre la boisson lusager.
- Lappareil 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, lusager peut annuler la commande. Lappareil doit alors rendre largent d j vers
sil 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