Université de la Manouba
Ecole Nationale des Sciences de
l’Informatique
Année Universitaire 2013-2014
Date : 03-04-2014
Module : Génie Logiciel II
Durée : 2h
Classe : II2
Doc : non autorisés
Publicité
Devoir surveillé
Exercice 1. (2+2+2+2+2)
Nous souhaitons modéliser le comportement d’un système de contrôle d’accès d’étudiants à un centre
de calcul ayant N postes:
- Le centre informatique ne peut pas supporter plus de N étudiants à la fois.
- Un étudiant accédant au centre doit avoir une carte d’accès.
- Un étudiant ne peut pas avoir accès à deux machines différentes
On souhaite élaborer un modèle B pour le comportement de ce système :
1) Donner informellement les propriétés que doit vérifier le système
2) Définir les ensembles abstraits, les constantes et les variables du système
3) Donner les Invariants correspondants aux exigences
Publicité
4) Décrire l’initialisation
5) Décrire les opérations du modèle B élaboré
Exercice 2. (2+2+2+4)
1) Expliquer comment est ce que les méthodes formelles jouent un rôle important dans le cycle
de développement d’un logiciel.
2) Donner les rôles du test et de la vérification formelle de programmes dans le cycle de
développement d’un logiciel en donnant l’avantage et les limites de chaque.
3) Peut-on avoir des variables sans initialisation dans une machine B ? justifier votre réponse.
4) Considérons le fragment de programme suivant :
Publicité
int maxint , int value1, int value2, int result ;
read(maxint) ;
read(value1) ;
read(value2);
if (value1value2 <= maxint && value1value2>0)
{
result = value1*value2;
printf(result);
}
Publicité
else
printf (0) ;
Traduire ce fragment de code en machine abstraite B en précisant l’invariant que vous définissez.
Bon Travail
1/1