Méthodes formelles Université de Provence
Master II Informatique
TP A. SPIN : propriétés d’accessibilité
Année 2010-2011
Exercice A.1 (Test de la première démonstration)
Refaites les exercices de la démonstration de spin effectuée en cours.
Exercice A.2 (Modélisation d’un ascenseur rigide)
Le programme PROMELA Ascenseur.pml contient le code de l’ascenseur (cf démonstration).
Question 1. Comment modifier le modèle de l’ascenseur pour assurer qu’au moins un chan-
gement d’étage à lieu entre chaque ouverture de porte ? Testez votre solution en
simulant le modèle à l’aide de spin.
Question 2. Comment modifier le modèle de l’ascenseur pour assurer qu’une porte ne s’ouvre
jamais deux fois de suite ? Testez la solution obtenue avec spin.
Exercice A.3 (Problème du berger)
Nous considérons à nouveau le problème du berger, du loup, du mouton et du chou.
Question 1. Proposez une modélisation du système en PROMELA dans laquelle chaque in-
dividu est représenté par un processus. Votre modèle utilisera un seul canal, de
type rendez-vous.
Question 2. Simulez votre modèle à l’aide spin pour vous assurer qu’il a le comportement
souhaité.
Question 3. Dans votre modèle, comment représenter l’état que le berger souhaite atteindre ?
Nous verrons plus tard comment décider l’existence d’un chemin vérifiant certaines propriétés
intermédiaires.
Exercice A.4 (Test de la seconde démonstration)
Vérifier les exercices de la seconde démonstration de spin effectuée en cours.
Exercice A.5 (Hyman, version 2)
Nous avons vu en TD une modélisation différente en PROMELA du protocole de Hyman,
issue de la représentation sous forme d’automate que nous avions. Appliquez les étapes de la
démonstration réalisée en cours sur le protocole de Hyman à cette nouvelle modélisation.
Exercice A.6 (Hyman, à plusieurs)
Proposez une modification du protocole de Hyman (dans sa version correcte...) pour modéliser
le cadre d’un accès de 4 utilisateurs. Vérifiez votre modélisation à l’aide de spin.
Exercice A.7 (Peterson)
Le protocole de Peterson étudié en TD est donné dans le fichier Peterson.pml Modifiez-le
pour permettre la vérification de la propriété d’exclusion mutuelle, puis vérifiez-le à l’aide de
spin.
1
Exercice A.8 (Protocole de Dijkstra)
L’algorithme auto-stabilisant de Dijkstra (1974) réalise une exclusion mutuelle pour des
systèmes distribués disposés en anneau. Les n processus P0 ,..., Pn−1 peuvent chacun deman-
der des informations à leur voisin de droite immédiat. Pour chaque processus Pi , le privilège
d’être en section critique est matérialisé par une configuration de ses variables propres et de
celles de son voisin de droite Pi−1mod n . Chaque processus possède une variable drapeau qu’il
peut lire et écrire, et il peut également lire le contenu de drapeau pour le processus à sa
droite. Le protocole proposé n’est pas symétrique : le processus P0 y joue un rôle particulier
alors que les autres processus ont un comportement identique.
Protocole pour P0 . Répéter les étapes suivantes :
attendre que P0 .drapeau == Pn−1 .drapeau
< Section critique >
P0 .drapeau = P0 .drapeau +1 (mod k)
Protocole pour Pi si i 6= 0. Répéter les étapes suivantes :
attendre que Pi .drapeau 6= Pi−1 .drapeau
< Section critique >
Pi .drapeau = Pi−1 .drapeau
Initialement chaque drapeau est mis à 0 et on choisit k > n. Noter qu’un processus ne change
son drapeau qu’à la sortie de la section critique : un seul processus change donc de drapeau
à la fois si l’exclusion mutuelle est satisfaite.
Question 1. Dans la configuration initiale, quel processus peut entrer en section critique ?
Question 2. Expliquer pourquoi il y a toujours un processus qui peut exécuter une transition.
Question 3. Écrire en PROMELA un programme qui modélise ce protocole.
Question 4. Simuler ce protocole avec n = 4 puis vérifier que l’exclusion mutuelle est bien
satisfaite grâce à la commande assert.
Question 5. Pour quelle valeur de n la construction exhaustive de l’espace d’états devient-elle
irréalisable, c’est-à-dire incomplète au bout de cinq minutes ou bien dépassant
les capacités de la machine ?
Question 6. Cet algorithme est dit autostabilisant car si on n’impose plus que chaque drapeau
soit mis à zéro initialement, on parvient au bout d’un nombre fini de transitions
dans un état où, de toutes façons, un seul processus possède le privilège d’être
en section critique. Cette propriété permet d’envisager par exemple un problème
électrique temporaire, et une correction automatique. Simuler ce protocole avec
des valeurs initiales quelconques.
Question 7. Modéliser en PROMELA le choix non-déterministe d’une valeur initiale pour
chaque processus Pi avec i 6= 0. Pour quelle valeur de n la construction exhaustive
de l’espace d’états devient-elle irréalisable ?
2
Méthodes formelles Université de Provence
Master II Informatique
TP B. SPIN et LTL
Année 2010-2011
Exercice B.1 (Test de la troisième démonstration)
Vérifiez les exercices de la démonstration relative à spin et LTL effectuée en cours.
Exercice B.2 Lancer la commande spin -f ’! [] (p -> X <> q )’. Quelle est la sortie
de spin ? Quel est l’automate de Büchi correspondant ? La syntaxe adoptée est la suivante :
Symboles propositionnels
true, false
Opérateurs booléens
toute chaı̂ne de minuscules
! (negation)
Opérateurs temporels -> (implication)
[] (G=toujours) <-> (equivalence)
<> (F=plus tard) && (et)
U (jusqu’à ce que) || (ou)
X (next)
Exercice B.3 (L’ascenseur)
On reprend le modèle de l’ascenseur vu au précédent TP (voir Ascenseur.pml). On souhaite
vérifier sur ce modèle qu’à chaque fois que la porte du premier étage est ouverte, l’ascenseur
se trouve bien au premier étage.
Question 1. Exprimer comme une formule LTL cette propriété.
Question 2. Modifiez le programme Promela pour pouvoir écrire cette propriété (ajoutez les
define pour les propositions atomiques).
Question 3. Effectuez la vérification.
Exercice B.4 (Exclusion mutuelle et vivacité de Peterson)
On considère à nouveau le code du protocole de Peterson donné dans le fichier Peterson.pml.
Question 1. Modifiez le programma afin de vérifier avec spin que l’exclusion mutuelle est
bien satisfaite.
Question 2. Comme dans l’exercice précédent, on souhaite tester si toute requête finit par
être satisfaite. Donnez une formule LTL simple de cette propriété, et appliquez
la méthodologie pour obtenir le résultat. Qu’obtenez-vous ? Cela vous semble-t-il
correct ?
Question 3. Proposez une correction mineure de la modélisation actuelle permettant de vérifier
la propriété souhaitée (sans dénaturer le protocole).
Exercice B.5 (Hyman, encore et encore)
Nous avons vu lors des TDs/TPs précédents le protocole de Hyman (voir Hyman4.pml). Nous
nous intéressons maintenant à la propriété de vivacité suivante : Si le processus i demande à
entrer en section critique (c’est-à-dire b[i] = 0) alors il finit tôt ou tard par entrer en section
critique.
Question 1. Exprimez cette propriété pour le processus 0 sous la forme d’une formule LTL.
Question 2. Est-ce que ce protocole satisfait cette propriété (cf Question 5. de l’exercice I.4
– TD1) ?
Question 3. Modifiez le programme pour pouvoir exprimer la propriété. Appliquez la méthodologie
vue dans la démonstration. Qu’obtenez-vous ? Etudiez avec attention la trace ob-
tenue. Est-ce que cela vous semble convaincant ?
3
Question 4. Pour mieux comprendre ce qui s’est passé à la question précédente, il est utile de
considérer le protocole dans le lequel le processus never est “embarqué”. Celui-
ci est modélisé dans le fichier Hyman5.pml. Quelle trace obtenez-vous pour ce
modèle ? Est-ce plus clair ?
Question 5. Par défaut, les variables sont initialisées à 0 dans Promela. Ainsi, on a initialement
b[0] = 0. Pour éviter ce problème, on peut considérer le modèle décrit dans le
fichier Hyman6.pml. Renouvelez la vérification. Qu’obtenez-vous ?
Question 6. Proposez une propriété exprimant une sorte de vivacité conditionnée à une cer-
taine équité entre les deux processus. Vérifiez qu’elle est satisfaite par le proto-
cole.
Exercice B.6 (Suite du TD sur LTL)
Comparez, pour chacune des formules LTL suivantes, l’automate de Büchi obtenu en TD avec
celui produit par spin.
– Gp
– Fp
– pU q
– (F p) → Gq
– F (p ∧ (q U r))
– (Gp) U q
– (F p) U q
– p U (G(q U r))
Vous pourrez aussi vérifier vos réponses sur le site http://www.liafa.jussieu.fr/~oddoux/ltl2ba/.
