Université Bordeaux I D.E.S.S. de Génie Logiciel U.F.R. Mathématiques et Informatique Année 1996-1997

Spécifications et vérifications formelles Examen de janvier 1997. (André Arnold & Alain Griffault)

1 Introduction

Cet exercice est inspiré de la thèse de François Laroussinie [?]. Il consiste, en partant d’une spécification informelle d’un ascenseur, d’une part à traduire cette spécification en terme de propriétés logiques, d’autre part à construire un modèle d’ascenseur qui satisfait cet ensemble de propriétés.

2 Spécifications informelles d’un ascenseur

L’ascenseur que nous allons étudier dessert n étages. La cabine comporte n boutons lumineux (ie lorsqu’un bouton est allumé, il témoigne de l’existence d’une requête pour cet étage) qui permettent de choisir la (ou les) destination(s). De plus, à chaque étage se trouve un bouton de même type qui permet d’appeler l’ascenseur. Lorsque la cabine s’arrête à un étage, la porte s’ouvre alors automatiquement.

Le comportement de cet ascenseur est contrôlé par logiciel. Les changements d’états du contrôleur sont liés aux actions sur les boutons lumineux. Le donneur d’ordre choisira le constructeur qui pourra lui prouver que les comportements suivants sont ”vrais”.

1. • Quand un bouton est enfoncé, le voyant correspondant s’allume.

• Quand la requête correspondante est satisfaite, le voyant s’éteint.

2. A chaque étage, la porte n’est jamais ouverte si la cabine n’est pas là.

3. Chaque requête doit être satisfaite ”un jour”.

4. L’ascenseur ne dessert que les étages pour lesquels existe une requête.

5. Lorsqu’il n’y a pas de requête, la cabine reste à l’étage où elle se trouve.

6. Lorsque la cabine se déplace, elle doit s’arrêter aux étages par lesquels elle passe si une requête les concerne.

7. Lorsqu’il existe plusieurs requêtes, l’ascenseur doit traiter prioritairement celle(s) permettant de continuer dans la même direction que le dernier déplacement.

3 Le premier modèle

Le premier modèle est obtenu par description des trois objets physiques utilisés : le bouton, la porte et la cabine, et de leurs interactions ”naturelles”.

[figure: Figure 1: Un bouton lumineux.; eteint; allume; e Nobody service; e requete appuyer incontrolable2; appuyer incontrolable1; service]

[figure: Figure 2: Une porte.; fermee; ouverte; e isFermee; e isOuverte; ouvrir; fermer]

[figure: Figure 3: La cabine.; 0; 1; 2; 3; {e \atop is0}; {e \atop is1}; {e \atop is2}; {e \atop is3}; i monte; d descend; i monte; d descend; i monte; d descend]
bouton porte bouton porte bouton porte bouton porte cabine1 bouton bouton bouton bouton
appuyer  e  e  e  e  e  e  e  e  e  e  e  e
e  e  appuyer  e  e  e  e  e  e  e  e  e  e
e  e  e  e  appuyer  e  e  e  e  e  e  e  e
e  e  e  e  e  e  appuyer  e  e  e  e  e  e
e  e  e  e  e  e  e  e  e appuyer e  e  e
e  e  e  e  e  e  e  e  e  e appuyer e  e
e  e  e  e  e  e  e  e  e  e  e appuyer e
e  e  e  e  e  e  e  e  e  e  e  e appuyer
service fermer  e  e  e  e  e  e  is0 service  e  e  e
e  e  service fermer  e  e  e  e  is1  e  service  e  e
e  e  e  e  service fermer  e  e  is2  e  e  service  e
e  e  e  e  e  e  service fermer is3  e  e  e  service
requete ouvrir  e  e  e  e  e  e  is0  e  e  e  e
e  ouvrir  e  e  e  e  e  e  is0 requete  e  e  e
e  e  requete ouvrir  e  e  e  e  is1  e  e  e  e
e  e  e  ouvrir  e  e  e  e  is1  e  requete  e  e
e  e  e  e  requete ouvrir  e  e  is2  e  e  e  e
e  e  e  e  e  ouvrir  e  e  is2  e  e  requete  e
e  e  e  e  e  e  requete ouvrir is3  e  e  e  e
e  e  e  e  e  e  e  ouvrir is3  e  e  e  requete
e isFermee e isFermee e isFermee e isFermee i  e  e  e  e
e isFermee e isFermee e isFermee e isFermee d  e  e  e  e

Question 1 L’ascenseur modélisé dessert 4 étages. Pensez-vous que 4 soit nécessaire et/ou suffisant pour pouvoir convaincre le donneur d’ordre ?

⊤ Deux étages ne sont pas suffisant, car le comportement de l’ascenseur sera obligatoirement équitable. Il passera autant de fois à chacun des étages. Trois étages sont peut-être suffisant, mais avec trois étages, tout déplacement a pour départ ou pour arrivée, une extrémité. Cette particularité risque de perturber les résultats pour les propriétés d’équité. Quatre étages semblent suffisant. Cinq ne semblent pas nécessaires. Si l’on groupe les étages de la manière suivante ({1},1), ({2},2), ({3,4},3), ({5},4), il semble que toutes les propriétés que l’on veut vérifier sur un ascenseur ayant 5 étages, peuvent l’être sur un ascenseur ayant 4 étages. Les points précédents ne sont pas des preuves, mais seulement des remarques de bon sens.

⊥

Question 2 L’environnement (les personnes) n’a pas été modélisé. Pourquoi ?

⊤ L’environnement d’un ascenseur est composé d’un nombre illimité de personnes utilisatrices. Dans le modèle, cet environnement ne peut donc pas être décrit, car il faudrait alors borné le nombre d’utilisateurs. Paradoxalement, ne pas représenter l’environnement (c’est à dire modéliser les requêtes par des actions incontrôlables dont l’emetteur (la personne) est ignorée) permet de représenter les comportements d’un nombre illimité de personnes.

⊥

Question 3 Calculer le comportement global de ce premier modèle. Combien d’états et de transitions comprend t-il ?

⊤ Le système de transition du premier modèle comprend 1792 états et 17664 transitions. ⊥

4 La validation du premier modèle

Pour convaincre le donneur d’ordre que les objets manipulés définissent bien un ascenseur, les propriétés suivantes sont calculées.

dead := *-src(*);
boucle := loop(*,*);
deadlock := inevitable(*,dead);
proj_state(1,tous,*);
proj_trans(1,toutes,*);
dts(bouton);
wts(src(*-toutes),*-toutes);
src_incont1 := src(incontrolable1);
src_incont2 := src(incontrolable2);
dts(nom);
proj_state(2,tous,*);
proj_trans(2,toutes,*);
dts(porte);
wts(src(*-toutes),*-toutes);
dts(nom);
proj_state(9,tous,*);
proj_trans(9,toutes,*);
dts(cabine);
wts(src(*-toutes),*-toutes);
dts(nom);
proj_state(10,tous,*);
proj_trans(10,toutes,*);
dts(bouton);
dts(nom);
PbAppuyer1 := src_incont1[1] - src(incontrolable1[1]);
PbAppuyer2 := src_incont2[1] - src(incontrolable2[1]);

Question 4 Le premier modèle est-il valide ?

⊤ La table suivante donne une interprétation des résultats des calculs précédents.

bouton  Les propriétés d’état
total  2
initial  1
tous  2 bon

Les propriétés de transition

total  8

toutes 7 l’action ”nobody” n’apparait pas dans les synchronisations.

Ceci ne remet donc pas en cause la validité de ce modèle.

cabine1  Les propriétés d’état
total  4
initial  1
tous  4 bon

Les propriétés de transition

total  14
toutes  14 bon
porte  Les propriétés d’état
total  2
initial  1
tous  2 bon

Les propriétés de transition

total  6

toutes 5 l’action ”isOuverte” n’apparait pas dans les synchronisations.

Ceci ne remet donc pas en cause la validité de ce modèle.

ascenseur V1 Les propriétés d’état
total  1792
initial  1
dead  0 bon
deadlock  0 bon

Les propriétés de transition

total  17664
boucle  17664 bon

Ce premier modèle semble donc valide. ⊥

Question 5 Les actions incontrôlables sont-elles correctement modélisées ?

⊤

ascenseur V1 Les propriétés d’état
total  1792
PbAppuyer1  0 bon
PbAppuyer2  0 bon

Les actions incontrôlables sur le bouton de l’étage 0 sont correctement modélisées. Pour plus de rigueur, il faudrait faire ce calcul sur les huit boutons.

⊥

5 La vérification du premier modèle

Dans le but de vérifier si les spécifications sont satisfaites ou non par ce modèle, les pré-calculs suivants sont effectués.

AppelEtage0 := incontrolable1[1];
AppelEtage1 := incontrolable1[3];
AppelEtage2 := incontrolable1[5];
AppelEtage3 := incontrolable1[7];
AppelCabine0 := incontrolable1[10];
AppelCabine1 := incontrolable1[11];
AppelCabine2 := incontrolable1[12];
AppelCabine3 := incontrolable1[13];
Appel0 := AppelEtage0 \/ AppelCabine0;

Appel1 := AppelEtage1 \/ AppelCabine1;
Appel2 := AppelEtage2 \/ AppelCabine2;
Appel3 := AppelEtage3 \/ AppelCabine3;
Appels := (Appel0 \/ Appel1) \/ (Appel2 \/ Appel3);
RappelEtage0 := incontrolable2[1];
RappelEtage1 := incontrolable2[3];
RappelEtage2 := incontrolable2[5];
RappelEtage3 := incontrolable2[7];
RappelCabine0 := incontrolable2[10];
RappelCabine1 := incontrolable2[11];
RappelCabine2 := incontrolable2[12];
RappelCabine3 := incontrolable2[13];
Ouvrir0 := !label[2] = "ouvrir";
Ouvrir1 := !label[4] = "ouvrir";
Ouvrir2 := !label[6] = "ouvrir";
Ouvrir3 := !label[8] = "ouvrir";
Service0 := !label[2] = "fermer";
Service1 := !label[4] = "fermer";
Service2 := !label[6] = "fermer";
Service3 := !label[8] = "fermer";
AllumeEtage0 := !state[1] = "allume";
AllumeEtage1 := !state[3] = "allume";
AllumeEtage2 := !state[5] = "allume";
AllumeEtage3 := !state[7] = "allume";
AllumeCabine0 := !state[10] = "allume";
AllumeCabine1 := !state[11] = "allume";
AllumeCabine2 := !state[12] = "allume";
AllumeCabine3 := !state[13] = "allume";
EteintEtage0 := !state[1] = "eteint";
EteintEtage1 := !state[3] = "eteint";
EteintEtage2 := !state[5] = "eteint";
EteintEtage3 := !state[7] = "eteint";
EteintCabine0 := !state[10] = "eteint";
EteintCabine1 := !state[11] = "eteint";
EteintCabine2 := !state[12] = "eteint";
EteintCabine3 := !state[13] = "eteint";
PorteOuverte0 := !state[2] = 'ouverte';
PorteOuverte1 := !state[4] = 'ouverte';
PorteOuverte2 := !state[6] = 'ouverte';
PorteOuverte3 := !state[8] = 'ouverte';
Cabine0 := !state[9] = '0';
Cabine1 := !state[9] = '1';
Cabine2 := !state[9] = '2';
Cabine3 := !state[9] = '3';
CabineNon0 := !state[9] # '0';
CabineNon1 := !state[9] # '1';
CabineNon2 := !state[9] # '2';
CabineNon3 := !state[9] # '3';
Monte := monte[9];
Descend := descend[9];
NoRequete := !state # "*allume*";
ApresAppuyer0 := reach(tgt(Appel0),* - (Appel0 \/ Service0));
AvantService0 := coreach(src(Service0),* - (Appel0 \/ Service0));
ApresAppuyer1 := reach(tgt(Appel1),* - (Appel1 \/ Service1));
AvantService1 := coreach(src(Service1),* - (Appel1 \/ Service1));

Question 6 A l’aide de ces marques, donner les expressions des propriétés 1, 2, 4, 5 et 6.

⊤ La plus-part des propriétés suivantes est de type : A ⇒ B. Avec Mec, elle se vérifie soit en calculant A − B, soit en calculant A ∧ ¬B, puis en comparant le résultat avec l’ensemble vide.

1. (a) Quand un bouton est enfoncé, le voyant correspondant s’allume.

Il suffit de calculer, pour les huit boutons, les états buts d’un appui qui ne sont pas allumés :

propriete1a := ((tgt(AppelEtage0 \/ RappelEtage0) - AllumeEtage0)
\/  (tgt(AppelCabine0 \/ RappelCabine0) - AllumeCabine0))
\/ (((tgt(AppelEtage1 \/ RappelEtage1) - AllumeEtage1)
\/   (tgt(AppelCabine1 \/ RappelCabine1) - AllumeCabine1))
\/  (((tgt(AppelEtage2 \/ RappelEtage2) - AllumeEtage2)
\/    (tgt(AppelCabine2 \/ RappelCabine2) - AllumeCabine2))
\/   ((tgt(AppelEtage3 \/ RappelEtage3) - AllumeEtage3)
\/    (tgt(AppelCabine3 \/ RappelCabine3) - AllumeCabine3))));

(b) Quand la requête correspondante est satisfaite, le voyant s’éteint. Il suffit de calculer, pour les quatre requêtes, les états buts d’un service qui ne sont pas éteints :

propriete1b := (tgt(Service0) - (EteintEtage0 \/ EteintCabine0))
\/ ((tgt(Service1) - (EteintEtage1 \/ EteintCabine1))
\/  ((tgt(Service2) - (EteintEtage2 \/ EteintCabine2))
\/   (tgt(Service3) - (EteintEtage3 \/ EteintCabine3))));

2. A chaque étage, la porte n’est jamais ouverte si la cabine n’est pas là.

Il suffit de calculer, pour chaque étage, les états dans lesquels la porte est ouverte et la cabine absente.

propriete2 := (PorteOuverte0 /\ CabineNon0)
\/ ((PorteOuverte1 /\ CabineNon1)
\/  ((PorteOuverte2 /\ CabineNon2)
\/   (PorteOuverte3 /\ CabineNon3)));

4. L’ascenseur ne dessert que les étages pour lesquels existe une requête.

Il suffit de calculer, pour chaque étage, les états dans lesquels il est possible d’ouvrir la porte sans qu’il y ait une requête pour cet étage.

propriete4 := (src(Ouvrir0) - (AllumeEtage0 \/ AllumeCabine0))
\/ ((src(Ouvrir1) - (AllumeEtage1 \/ AllumeCabine1))
\/  ((src(Ouvrir2) - (AllumeEtage2 \/ AllumeCabine2))
\/   (src(Ouvrir3) - (AllumeEtage3 \/ AllumeCabine3))));

5. Lorsqu’il n’y a pas de requête, la cabine reste à l’étage où elle se trouve.

Il suffir de calculer les états à partir desquels un mouvement est possible, sans qu’il y ait de requêtes.

propriete5 := src(Monte \/ Descend) /\ NoRequete;

6. Lorsque la cabine se déplace, elle doit s’arrêter aux étages par lesquels elle passe si une requête les concerne. Il suffit de calculer, pour chaque étage, s’il est possible d’en partir malgré l’existence d’une requête pour cet étage.

propriete6 := (rsrc((AllumeEtage0 \/ AllumeCabine0) /\ Cabine0) /\ (Monte \/ Descend))
\/ ((rsrc((AllumeEtage1 \/ AllumeCabine1) /\ Cabine1) /\ (Monte \/ Descend))
\/  ((rsrc((AllumeEtage2 \/ AllumeCabine2) /\ Cabine2) /\ (Monte \/ Descend))
\/   (rsrc((AllumeEtage3 \/ AllumeCabine3) /\ Cabine3) /\ (Monte \/ Descend))));

⊥ Les propriétés 3 et 7 sont des propriétés dites de vivacité. Pour les vérifier, nous calculons :

propriete3A0 := loop(*, rsrc(ApresAppuyer0) /\ rtgt(AvantService0));
propriete3A1 := loop(*, rsrc(ApresAppuyer1) /\ rtgt(AvantService1));
propriete3B0 := loop(Monte \/ Descend, rsrc(ApresAppuyer0) /\ rtgt(AvantService0));
propriete3B1 := loop(Monte \/ Descend, rsrc(ApresAppuyer1) /\ rtgt(AvantService1));
ApresMonte := reach(tgt(Monte),* - Appels);
ApresMonteDescend := reach(tgt(Descend) /\ ApresMonte, * - Appels);
propriete7 := ApresMonteDescend /\ src(Monte);

Question 7 Expliquer en quoi diffèrent les propriétés 3A et 3B. Donnez en une description informelle (en français), puis dites laquelle des deux est certainement celle que le donneur d’ordre désire.

⊤ L’expression T1=loop(T2,T3) calcule les transitions T1 des composantes fortements connexes inclues dans T3 et ayant une intersection non vide avec T2.

ApresAppuyer0 := reach(tgt(Appel0),* - (Appel0 \/ Service0)) donne toutes les possibilités d’évolution après

une requête, et avant qu’elle ne soit satisfaite (l’ouverture de la porte).

AvantService0 := coreach(src(Service0),* - (Appel0 \/ Service0)) donne toutes les origines possibles d’un

service, depuis la dernière requête. Monte \/ Descend représente les mouvements de la cabine.

• propriete3A correspond aux boucles possibles dans le graphe entre une requête et son service.

• propriete3B correspond aux boucles possibles dans le graphe entre une requête et son service, et dans laquelle, la cabine a bougé au moins une fois.

Le donneur d’ordre veut un comportement équitable, mais certainement avec l’hypothèse d’une utilisation ”normale”. Le comportement suivant :

1. La cabine présente à l’étage 0.

2. Une personne appuie sur le bouton 0 du palier.

3. La porte s’ouvre.

4. La personne entre dans la cabine (ou non, cela n’a pas d’importance).

5. La porte se ferme.

6. La même personne (ou une autre) appuie sur le bouton 0 du palier (ou sur le bouton 0 de la cabine).

7….

qui est autorisé (et qui doit l’être) va provoquer une boucle dans le graphe. Cette boucle peut faire attendre indéfiniment une personne située à un autre étage. Le donneur d’ordre veut donc un comportement équitable, avec l’hypothèse que la boucle précédente ne puisse se reproduire à l’infini. Une façon simple de traduire cette hypothèse est de supposer que la cabine se déplace de temps en temps. Les boucles parasites apparaissent dans propriete3A et n’apparaissent pas dans propriete3B : c’est donc cette dernière qui correspond probablement au désir du donneur d’ordre. Remarque : Il est évidemment nécessaire d’effectuer les calculs similaires pour les étages 2 et3. La symétrie qui semble évidente n’a pas été montrée, et ne peut donc être mise en avant pour diminuer les calculs.

⊥

Question 8 Expliquer le calcul de la propriété 7. Correspond t-il exactement à la spécification informelle ?

⊤ La spécification informelle de la propriété 7 est :

7. Lorsqu’il existe plusieurs requêtes, l’ascenseur doit traiter prioritairement celle(s) permettant de continuer dans la même direction que le dernier déplacement.

ApresMonte := reach(tgt(Monte),* - Appels); calcule les états accessibles après un mouvement vers le haut de la cabine sans nouvel appel.

ApresMonteDescend := reach(tgt(Descend) /\ ApresMonte, * - Appels); calcule les états accessibles après un

mouvement vers le bas de la cabine, successif à un mouvement vers le haut, le tout sans nouvel appel. propriete7 := ApresMonteDescend /\ src(Monte); calcule les états précédents à partir desquels il est possible d’effectuer un mouvement vers le haut. propriété7 cherche l’existence d’un état qui prouverait que la succession ”monte”, ”descend”, ”monte” est possible pour un ensemble de requêtes donné. Si un tel état existe, l’ascenseur n’aura pas traiter prioritairement la dernière requête qui étaient obligatoirement possible soit lors de la première phase d’ascension, soit dans la phase de descente. propriete7 exprime donc bien la spécification informelle, sous réserve de la symétrie des comportements. En toute rigueur, il faut également faire le calcul analogue.

ApresDescend := reach(tgt(Descend),* - Appels);
ApresDescendMonte := reach(tgt(Monte) /\ ApresDescend, * - Appels);

puis :

propriete7 := (ApresMonteDescend /\ src(Monte)) \/ (ApresDescendMonte /\ src(Descend));

⊥

Question 9 Montrer (par calcul avec Mec) que le premier modèle satisfait les propriétes 1, 2 et 4 mais ne satisfait pas les propriétés 3A, 3B, 5, 6 et 7.

⊤ Les résultats des calculs des diverses propriétés sur le premier modèle donnent :

ascenseur V1 Les propriétés d’état
total  1792
propriete1A  0 satisfaite
propriete1B  0 satisfaite
propriete2  0 satisfaite
propriete4  0 satisfaite
propriete5  4 non satisfaite
propriete7  1024 non satisfaite

Les propriétés de transition

total  17664
propriete3A 17414 non satisfaite
propriete3B 17398 non satisfaite
propriete6  1152 non satisfaite

⊥

6 Le deuxième modèle

Une analyse des résultats du premier modèle montre un manque d’information sur les déplacements de la cabine. Celle-ci est donc remplacée par le système représenté par la figure 4.

[figure: Figure 4: Une nouvelle cabine.; 0; 1; 2; 3; {e \atop is0}; {e \atop is1}; {e \atop is2}; {e \atop is3}; 0to1 monte; 1to0 descend; 1to2 monte; 2to1 descend; 2to3 monte; 3to2 descend]

Question 10 Donner le nouveau système de synchronisation.

⊤ Les actions ”i” et ”d” de la cabine ont été remplacées par des actions plus explicites. Il faut utiliser cette connaissance supplémentaire pour éviter des déplacements si l’on doit ouvrir une porte ou s’il n’y a aucune requête. Cela donne :

bouton porte bouton porte bouton porte bouton porte cabine2 bouton bouton bouton bouton
e isFermee e isFermee e isFermee e isFermee i  e  e  e  e
e isFermee e isFermee e isFermee e isFermee d  e  e  e  e

sont remplacés par

Nobody isFermee requete isFermee e isFermee e isFermee 0to1 Nobody e  e  e
Nobody isFermee e isFermee requete isFermee e isFermee 0to1 Nobody e  e  e
Nobody isFermee e isFermee e isFermee requete isFermee 0to1 Nobody e  e  e
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody requete e  e
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody e requete e
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody e  e requete
e isFermee Nobody isFermee requete isFermee e isFermee 1to2  e Nobody e  e
e isFermee Nobody isFermee e isFermee requete isFermee 1to2  e Nobody e  e
e isFermee Nobody isFermee e isFermee e isFermee 1to2  e Nobody requete e
e isFermee Nobody isFermee e isFermee e isFermee 1to2  e Nobody e requete
e isFermee e isFermee Nobody isFermee requete isFermee 2to3  e  e Nobody e
e isFermee e isFermee Nobody isFermee e isFermee 2to3  e  e Nobody requete
e isFermee e isFermee e isFermee Nobody isFermee 3to2  e  e requete Nobody
e isFermee e isFermee e isFermee Nobody isFermee 3to2  e requete e Nobody
e isFermee e isFermee e isFermee Nobody isFermee 3to2 requete e  e Nobody
e isFermee e isFermee requete isFermee Nobody isFermee 3to2  e  e  e Nobody
e isFermee requete isFermee e isFermee Nobody isFermee 3to2  e  e  e Nobody
requete isFermee e isFermee e isFermee Nobody isFermee 3to2  e  e  e Nobody
e isFermee e isFermee Nobody isFermee e isFermee 2to1  e requete Nobody e
e isFermee e isFermee Nobody isFermee e isFermee 2to1 requete e Nobody e
e isFermee requete isFermee Nobody isFermee e isFermee 2to1  e  e Nobody e
requete isFermee e isFermee Nobody isFermee e isFermee 2to1  e  e Nobody e
e isFermee Nobody isFermee e isFermee e isFermee 1to0 requete Nobody e  e
requete isFermee Nobody isFermee e isFermee e isFermee 1to0 e Nobody e e

⊥

Question 11 Montrer (par calcul avec Mec) que le second modèle satisfait les propriétes 1, 2, 4, 5 et 6 mais ne satisfait pas les propriétés 3A, 3B et 7.

⊤ Les résultats des calculs des diverses propriétés sur le deuxième modèle donnent :

ascenseur V2 Les propriétés d’état
total  1792 inchangé
propriete1A  0 satisfaite
propriete1B  0 satisfaite
propriete2  0 satisfaite
propriete4  0 satisfaite
propriete5  0 satisfaite
propriete7  36 non satisfaite

Les propriétés de transition

total  16896 inférieur au nombre de transitions du premier modèle.
propriete3A 15308 non satisfaite
propriete3B 15094 non satisfaite
propriete6  0 satisfaite

⊥

7 Le troisième modèle

Les propriétés 3 et 7 ne sont pas satisfaites, car il est difficile dans ce modèle de garantir qu’un événement se produira dans le futur. Il est donc nécessaire d’introduire un nouveau composant qui va contrôler les déplacements de la cabine.

Question 12 Donner le système de transition d’un contrôleur (si possible indépendant du nombre d’étages desservis), et le système de synchronisation associé pour lesquels toutes les propriétés (sauf 3A) sont satisfaites.

⊤ La propriété 7 correspond à une méthode utilisée par le contrôleur de la tête de lecture d’un disque, afin de garantir l’équité. C’est une optimation d’une technique de balayage aller-retour sur un intervalle. Il suffit donc de traduire cet algorithme en système de transition.

[figure: Figure 5: Le premier contrôleur.; descend; arret; monte; {e \atop Down}; e; {e \atop Up}; Stop; Down; Up; Stop; OnlyUp; OnlyDown]

Intuitivement, l’état ”arret” indique une absence de requête, l’état ”descend” indique que le dernier mouvement était vers le bas, et l’état ”monte” que le dernier mouvement était vers le haut. De même, l’étiquette ”Stop” détecte l’absence de requête, ”Up” la présence d’une requête vers le haut, ”Down” la présence d’une requête vers le bas, ”OnlyUp” la présence d’une requête vers le haut et d’aucune requête vers le bas, ”OnlyDown” la présence d’une requête vers le bas et d’aucune requête vers le haut.

Il est possible de simplifier ce premier contrôleur. Le fait qu’il n’y ait aucune requête lors de l’arrivée d’une nouvelle requête est sans importance, on peut toujours considérer qu’elle fait suite à un dernier mouvement. L’état ”arret” est donc inutile. Cela donne :

[figure: Figure 6: Le second contrôleur.; descend; monte; {e \atop Down}; {e \atop Up}; OnlyUp; OnlyDown]

L’état ”descend” est l’état initial. Cela n’est pas obligatoire, mais correspond au fait que l’état initial de la cabine est l’étage 0, et par conséquent, que le dernier mouvement de la cabine est un mouvement vers le bas.

Une fois la sémantique des contrôleurs donnée, les vecteurs de synchronisation sont simples à écrire.

bouton porte bouton porte bouton porte bouton porte cabine2 bouton bouton bouton bouton controleur
appuyer e  e  e  e  e  e  e  e  e  e  e  e  e
e  e appuyer e  e  e  e  e  e  e  e  e  e  e
e  e  e  e appuyer e  e  e  e  e  e  e  e  e
e  e  e  e  e  e appuyer e  e  e  e  e  e  e
e  e  e  e  e  e  e  e  e appuyer e  e  e  e
e  e  e  e  e  e  e  e  e  e appuyer e  e  e
e  e  e  e  e  e  e  e  e  e  e appuyer e  e
e  e  e  e  e  e  e  e  e  e  e  e appuyer  e
service fermer  e  e  e  e  e  e  is0 service  e  e  e  e
e  e  service fermer  e  e  e  e  is1  e  service  e  e  e
e  e  e  e  service fermer  e  e  is2  e  e  service  e  e
e  e  e  e  e  e  service fermer is3  e  e  e  service  e
requete ouvrir  e  e  e  e  e  e  is0  e  e  e  e  e
e  ouvrir  e  e  e  e  e  e  is0 requete e  e  e  e
e  e  requete ouvrir  e  e  e  e  is1  e  e  e  e  e
e  e  e  ouvrir  e  e  e  e  is1  e requete e  e  e
e  e  e  e  requete ouvrir  e  e  is2  e  e  e  e  e
e  e  e  e  e  ouvrir  e  e  is2  e  e requete e  e
e  e  e  e  e  e  requete ouvrir is3  e  e  e  e  e
e  e  e  e  e  e  e  ouvrir is3  e  e  e requete  e
Nobody isFermee requete isFermee e isFermee e isFermee 0to1 Nobody e  e  e  Up
Nobody isFermee e isFermee requete isFermee e isFermee 0to1 Nobody e  e  e  Up
Nobody isFermee e isFermee e isFermee requete isFermee 0to1 Nobody e  e  e  Up
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody requete e  e  Up
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody e requete e  Up
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody e  e requete  Up
e isFermee Nobody isFermee requete isFermee e isFermee 1to2  e Nobody e  e  Up
e isFermee Nobody isFermee e isFermee requete isFermee 1to2  e Nobody e  e  Up
e isFermee Nobody isFermee e isFermee e isFermee 1to2  e Nobody requete e  Up
e isFermee Nobody isFermee e isFermee e isFermee 1to2  e Nobody e requete  Up
e isFermee e isFermee Nobody isFermee requete isFermee 2to3  e  e Nobody e  Up
e isFermee e isFermee Nobody isFermee e isFermee 2to3  e  e Nobody requete  Up
e isFermee e isFermee e isFermee Nobody isFermee 3to2  e  e requete Nobody Down
e isFermee e isFermee e isFermee Nobody isFermee 3to2  e requete e Nobody Down
e isFermee e isFermee e isFermee Nobody isFermee 3to2 requete e  e Nobody Down
e isFermee e isFermee requete isFermee Nobody isFermee 3to2  e  e  e Nobody Down
e isFermee requete isFermee e isFermee Nobody isFermee 3to2  e  e  e Nobody Down
requete isFermee e isFermee e isFermee Nobody isFermee 3to2  e  e  e Nobody Down
e isFermee e isFermee Nobody isFermee e isFermee 2to1  e requete Nobody e  Down
e isFermee e isFermee Nobody isFermee e isFermee 2to1 requete e Nobody e  Down
e isFermee requete isFermee Nobody isFermee e isFermee 2to1  e  e Nobody e  Down
requete isFermee e isFermee Nobody isFermee e isFermee 2to1  e  e Nobody e  Down
e isFermee Nobody isFermee e isFermee e isFermee 1to0 requete Nobody e  e  Down
requete isFermee Nobody isFermee e isFermee e isFermee 1to0  e Nobody e  e  Down
Nobody isFermee requete isFermee e isFermee e isFermee 0to1 Nobody e  e  e  OnlyUp
Nobody isFermee e isFermee requete isFermee e isFermee 0to1 Nobody e  e  e  OnlyUp
Nobody isFermee e isFermee e isFermee requete isFermee 0to1 Nobody e  e  e  OnlyUp
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody requete e  e  OnlyUp
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody e requete e  OnlyUp
Nobody isFermee e isFermee e isFermee e isFermee 0to1 Nobody e  e requete OnlyUp
Nobody isFermee Nobody isFermee requete isFermee e isFermee 1to2 Nobody Nobody e  e  OnlyUp
Nobody isFermee Nobody isFermee e isFermee requete isFermee 1to2 Nobody Nobody e  e  OnlyUp
Nobody isFermee Nobody isFermee e isFermee e isFermee 1to2 Nobody Nobody requete e  OnlyUp
Nobody isFermee Nobody isFermee e isFermee e isFermee 1to2 Nobody Nobody e requete OnlyUp
Nobody isFermee Nobody isFermee Nobody isFermee requete isFermee 2to3 Nobody Nobody Nobody e  OnlyUp
Nobody isFermee Nobody isFermee Nobody isFermee e isFermee 2to3 Nobody Nobody Nobody requete OnlyUp
e isFermee e isFermee e isFermee Nobody isFermee 3to2 e e requete Nobody OnlyDown
e isFermee e isFermee e isFermee Nobody isFermee 3to2  e requete e Nobody OnlyDown
e isFermee e isFermee e isFermee Nobody isFermee 3to2 requete e  e Nobody OnlyDown
e isFermee e isFermee requete isFermee Nobody isFermee 3to2  e  e  e Nobody OnlyDown
e isFermee requete isFermee e isFermee Nobody isFermee 3to2  e  e  e Nobody OnlyDown
requete isFermee e isFermee e isFermee Nobody isFermee 3to2  e  e  e Nobody OnlyDown
e isFermee e isFermee Nobody isFermee Nobody isFermee 2to1  e requete Nobody Nobody OnlyDown
e isFermee e isFermee Nobody isFermee Nobody isFermee 2to1 requete e Nobody Nobody OnlyDown
e isFermee requete isFermee Nobody isFermee Nobody isFermee 2to1  e  e Nobody Nobody OnlyDown
requete isFermee e isFermee Nobody isFermee Nobody isFermee 2to1  e  e Nobody Nobody OnlyDown
e isFermee Nobody isFermee Nobody isFermee Nobody isFermee 1to0 requete Nobody Nobody Nobody OnlyDown
requete isFermee Nobody isFermee Nobody isFermee Nobody isFermee 1to0  e Nobody Nobody Nobody OnlyDown
Nobody isFermee Nobody isFermee Nobody isFermee Nobody isFermee e Nobody Nobody Nobody Nobody Stop

Avec le second contrôleur, la dernière contrainte est inutile.

Nous obtenons les résultats suivants :

ascenseur V3 Les propriétés d’état
total  4480
propriete1A  0 satisfaite
propriete1B  0 satisfaite
propriete2  0 satisfaite
propriete4  0 satisfaite
propriete5  0 satisfaite
propriete7  0 satisfaite

Les propriétés de transition

total  41934
propriete3A 26750 non satisfaite
propriete3B  0 satisfaite
propriete6  0 satisfaite

ascenseur V4 Les propriétés d’état
total  2688
propriete1A  0 satisfaite
propriete1B  0 satisfaite
propriete2  0 satisfaite
propriete4  0 satisfaite
propriete5  0 satisfaite
propriete7  0 satisfaite

Les propriétés de transition

total  25032
propriete3A 16050 non satisfaite
propriete3B  0 satisfaite
propriete6  0 satisfaite

Remarque : Une différence notable existe entre les deux contrôleurs. Le premier n’est pas déterministe, alors que le second l’est. Soit en effet la situation suivante :

1. Aucune requête et la cabine à l’étage 1.

2. Deux requêtes simultanées : une pour l’étage 0, et une pour l’étage 2. Le premier contrôleur est a l’arrêt, il va donc de façon aléatoire choisir de traiter d’abord une des deux requêtes. Le second contrôleur est soit dans l’état ”descend”, soit dans l’état ”monte”. Cet état détermine quelle sera la requête traitée en priorité. Cette différence est mise en évidence avec la propriété suivante qui calcule les états ou un choix aléatoire peut-être fait.

deterministe := src(Monte) /\ src(Descend);

ascenseur V3 Les propriétés d’état
total  4480
deterministe  90 non satisfaite

ascenseur V4 Les propriétés d’état
total  2688
deterministe  0 satisfaite

⊥

8 Modalités

• Vous pouvez utiliser les sources disponibles dans ~griffaul/Demos/Ascenseur

• Date limite de remise des rapports : Lundi 13 janvier à 9 heures du matin. Le rapport devra être déposé dans le répertoire ~griffaul/VF/ avec un nom permettant d’identifier le propriétaire. Le répertoire sera accessible en écriture du vendredi 10 janvier au matin jusqu’à la date limite.

• Le rapport doit comprendre les fichiers ”sources” et un texte explicatif (non nécessairement long).

• Les binômes sont acceptés.