![]() |
Nantes B Libraries Page
(Etude de cas : Video shop en B) sdssssssscbvcbvsssslhkhhkjhkjhkjhkhkjkjhkssssssdsdsdsdsdsdsdsdsdssd |
|
---|
|
Project : N-Tiers
Etude de la spécification en B des app;ications à architecture n-tiers |
Participants : Audel, Sezestre
Pineau, Perruchas |
status :
en cours |
Dans le cadre du mini-projet du DESS, on va s'appuyer sur l'étude de cas "video shop", déjà traité en $Z$ dans le module D2.
Bref rappel du cahier de charges
Un club vidéo a des membres qui
peuvent louer des vidéos et des employés qui sont responsables
de l'enregistrement des transactions du club.
Les membres peuvent louer des vidéos
s'ils ont l'âge requis. Pour cette raison le club a besoin d'enregistrer
leur date de naissance. Il enregistre aussi les adresses des membres de
façon à engager des actions appropriées lorsque des
vidéos louées ne sont pas rendues.
Les employés du club peuvent aussi
louer des vidéos. Les vidéos sont classés sur
les étagères selon les sujets (horreur, comédie, X,
etc). Chaque vidéo a un tarif de location qui dépend de sa
popularité (courante) et du fait qu'il soit récent.
Il n'y a que très peu de tarifs
qui s'appliquent à tout moment.
Modélisation en $B$ du système
de location
Le cahier de charges sera analysé
et précisé au fur et à mesures.
On donnera une spécification $B$
complète et on analysera formellement cette spécification
en utilisant l'$Atelie B$. Certaines parties doivent être raffinées
jusqu'à la génération de code en C.
Références
Z in Practice, R. Bardin,
S. Stepney, D. Cooper, Prentice Hall.
Contact : email
LINA- COLOSS Méthodes et Spécifications Formelles |
Addresse
IRIN - Faculté des sciences 2, rue de la Houssinière BP 92298 44 322 Nantes Cedex 3 |