TPs Model-Checking
Support de Cours
Executer la commande source ~vernadat/.bashrc pour positionner les variables
d'environnement TINA
Annale 2021:
2022
Videos du cours
Tableau WorkBench TWB
LTL, Patterns et Equité : TP 1
TP1: LTL, Patterns et Equité
Exo 1 : Pb d'Allocations de Ressources :
2 Clients + 2 Gestionnaires de Ressource
Un client a besoin pour travailler de posséder de manière mutuellement
exclusive deux ressources (R_1,R_2) qui sont distantes et gérées
individuellement par deux gestionnaires (G_1,G_2).
La communication entre client et gestionnaire
est régie par les messages suivants:
- Req - demande d'accès à la ressource,
- Ack - autorisation d'accès à la ressource,
- Lib - libération de la ressource
Les clients ont un comportement symétrique, il en est de même
pour les gestionnaires.
Client C_j: C_j demande séquentiellement les deux
ressources. Plus précisément, il demande d'abord la ressource R_1, et
lorsqu'il l'a obtenue, il demande la ressource R_2. Il entre en
section critique lorsqu'il possède les deux ressources. Il libère
ensuite en même temps les deux ressources et retourne à son état initial.
Gestionnaire G_j:
A la réception d'un message Req envoyé par le client Ci,
G_j alloue exclusivement la ressource à Ci
(i.e envoi du message Ack à Ci si la ressource est libre,
sinon la requête reste en attente.
A la réception du message Lib, la ressource est libérée.
Le système global décrit par composition de 4 réseaux
(2 gestionnaires et 2 clients). Les sources sont accessibles
ici .
Sauvez les différents fichiers et
lancez dans le même directory la commande nd compo.tpn ).
- Apéritif :
- Simulez le système à l'aide du Stepper (ne pas chercher à dessiner le réseau)
- Construisez son graphe des marquages (option par défaut ktz)
Pour la suite de l'exercice, vous utiliserez un fichier (fic.ltl) dans lequel vous
donnerez l'énoncé informel de la propriété, sa traduction en LTL et la réponse
que vous attendez du model-checker (True/False). Vous pouvez commenter les lignes en commencant par un #.
Vous pourrez invoquer directement selt via la commande suivante:
selt compo.ktz fic.ltl On pourra ainsi réutiliser ces propriétés
dans la dernière partie de l'exercice.
- Cas d'un Système non bloquant
En utilisant les formules de LTL assurez-vous:
- Que le système est non bloquant.
- Que les clients travaillent en exclusion mutuelle
- Que l'accès en exclusion mutuelle est garanti pour chaque ressource (*).
- Que chaque client peut être en situation de famine (*).
(*) Vous donnerez une formule spécifique pour chaque client/ressource.
- Que le système est infiniment actif (c-à-d peut s'exécuter indéfiniment).
- Que le système peut comporter des exécutions infinies où un des clients ne s'exécute (plus) jamais
(c-à-d un client n'exécute aucune action - soit dès le départ soit à partir d'un état particulier).
- Peut-on trouver une séquence infinie où un des gestionnaires ne s'exécute jamais ?
Pour ces 3 dernières propriétés, vous obtiendrez une séquence (contre-exemple)
caractéristique de la situation décrite.
Proposez une version purement événentielle des propriétés 4) et 6).
- Système bloquant :
On suppose maintenant qu'un des deux clients demande les 2 ressources en même temps : le système obtenu est maintenant bloquant (cf TP 4 IR).
- Le nouveau système est accessible ici (cl1bis.net et compobis.tpn)
- Vérifiez les propriétés vues en première partie
(par exemple via selt compobis.ktz fic.ltl) et notez les changements.
- Un interblocage est-il possible ?
- Caractérisez le en utilisant la logique LTL : vous devez trouver une formule Phi caractéristique de cet interblocage.
- Montrez que l'interblocage est la seule cause de blocage : proposez une formule LTL
montrant que phi et dead sont bien équivalentes.
Exo 2 : Spécification et Patterns
La page patterns présente les patterns de propriétés et leur traduction en LTL.
- Analysez les patterns d'Absence, Existence, Universality,
Presence, Response.
On peut utiliser directement ces patterns LTL sous selt
en utilisant la bibliotheque patterns de selt.
Pour faire appel à une bibliothèque, on peut procéder soit:
- en ligne de commande : ex
selt compo.ktz -prelude patterns.ltl
- sous l'interpéteur selt ; il suffit alors de taper source patterns.ltl;
- On considère l'exemple de spécification vu en cours.
On dispose de deux "implémentations" de ce système d'allocations:
une non équitable unfairmutex , l'autre oui fairmutex .
- Reprendre les formules vue en cours et analysez les 2 systèmes avec elles.
Vous les écrirez dans un fichier spec.ltl. Pour les évaluer
vous pouvez travailler soit:
- en ligne de commande : ex selt compo.ktz spec.ltl
- sous l'interpéteur selt : il suffit alors de taper source spec.ltl;
- Regardez (Vérifiez) les spécifications exprimez dans fichier specfairmutex.ltl et répondez aux questions posées.
- Même exercice en exprimant les propriétés directement à l'aide de patterns.
Le plus simple est d'inclure la directive source patterns.ltl; dans le fichier spec.ltl.
Exo 3 : Equité et Progrès (Juste un apercu)
Equité : On considère de nouveau le premier système
pour lequel on a vu que la famine était possible, on va étudier
l'absence de famine sous condition d'équité.
- Proposez une formule permettant d'assurer que si C1 ne demande pas une infinité de fois à travailler alors C2 ne risque pas la famine.
- Vérifiez si cette formule est satisfaite.
Progrès : On considère le réseau suivant .
On retrouve deux clients, leurs transitions d'accès en CS sont en conflit via la place x
mais celle-ci contient deux jetons.
- Conserve-t-on la propriété d'exclusion mutuelle ?
- Qu'en est-il intutivement de la propriété d'absence de famine ?
- Votre intuition est elle vérifiée ?
- Pour lever le paradoxe ....
- Caractérisez en LTL les séquences au cours de laquelle un des clients est définitivement bloqué.
- Donnez une formule montrant que si un client n'est
pas définitivement bloqué alors il ne risque pas la famine.
- Mêmes questions en considérant le réseau suivant
- Questions optionnelles (Hors sujet) Quelle différence peut-on faire entre les deux systèmes ?
Cette différence se retrouve-t-elle sur la structure de Kripke qui les représente ?