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
CTL et Points Fixes : TP 2
TP2 : CTL et Points Fixes
Exo 1 : Pb d'Allocations de Ressources :
2 Clients + 2 Gestionnaires de Ressource
Il s'agit de l'exemple utilisé pour le TP LTL !
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 ).
- Simulez le système à l'aide du Stepper (ne pas chercher à dessiner le réseau)
- Construisez son graphe des marquages au format verbose et ktz. Vous pouvez le faire via nd soit en ligne de commande.
- tina compo.tpn > compo.verbose
- tina compo.tpn compo.ktz
Pour la suite de l'exercice, comme pour le tp LTL, vous écrirez les formules dans un fichier (fic.mmc).
Pour chaque question, vous donnerez une formulation et le résultat attendu
en consièrant les options bool et card. Pour l'option card, vous donnerez la formulation la plus simple (de complexité modale minimale).
- En utilisant les formules de CTL 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 le système est infiniment actif (c-à-d peut s'exécuter indéfiniment).
- Que le système peut comporter des exécutions où un des clients ne s'exécute (plus) jamais (c-à-d un client n'exécute aucune action soit dès l'état initial soit à partir d'un état particulier).
- Que chaque client peut être en situation de famine.
- On suppose maintenant qu'un des deux clients demande les 2 ressources en même temps.
- Le nouveau système est accessible ici (cl1bis.n
et et compobis.tpn)
- Le système est maintenant bloquant : Trouvez les états
- où le système est bloqué.
- à partir desquels le système pourra se bloquer.
- à partir desquels le blocage est inévitable.
- à partir desquels le blocage n'est pas possible.
- à partir desquels il existe une exécution infinie (sans blocage).
- Caractérisez l'interblocage en utilisant la logique CTL.
Exo 2 : Analyse de blocages
On considère le réseau suivant . Simulez-le à l'aide du stepper
et essayez de voir pourquoi il peut se bloquer et pourquoi
il peut échapper au blocage.
A l'aide de CTL, trouvez et caractérisez les états à partir desquels:
- à partir desquels le système est bloqué.
- à partir desquels le système se bloquera inévitablement
- à partir desquels le système ne pourra pas se bloquer.
Proposez une interprétation aux formules suivantes :
- EF EG (p4 + p5 = 0);
- (1 <= p0 + p1 + p2) => - AF dead;
- AF dead <=> - EG T ;
Exo 3 : Points Fixes
Muse est un évaluateur de formules du mu-calcul (plus général que CTL).
Pour les exercices précédents,vous avez utilisé la
bibliothèque CTL .
Le fichier CTL est une définition
commentée de la bibliothèque que vous avez utilisé.
Lisez le et comprenez-le.
- Proposez une interprétation aux formules suivantes:
- op EFevt E phi = min x | <E> phi \/ <T> x;
- op AFevt E phi = min x | (<E> T /\ [E] phi) \/ (<T>T /\ [T]x);
Construisez un petit exemple pour confirmer/infirmer votre intuition.
- Mêmes questions pour les formules suivantes:
- op EFtau phi = min phi | phi \/ <tau> phi;
- op Pos E phi = EFtau ( <E> ( EFtau phi));
- op Nec E phi = - (Pos E (- phi)) ;
Construisez un petit exemple pour confirmer/infirmer votre intuition.