Chemins d'acces : source /mnt/n7fs/etr2013/etr.sh
Demo CTL Muse
I Courte Introduction à la vérification avec CTL
Pour permettre la vérification de propriétés spécifiques, TINA
dispose d'un model-checker pour la logique temporelle CTL (Conditional
Time Logic ou encore Computation Tree Logic). Cette logique permet
d'exprimer des propriétés caractéristiques du système que vous
modélisez et de les vérifier.
Les formules de CTL s'évaluent sur l'ensemble des
états du système (ici du graphe de marquages associé au
réseau que vous analysez).
Une formule f est vraie si elle est satisfaite par toutes
les états du système S. On le note S |= f.
Les formules de CTL contiennent les formules habituelles
du calcul propositionnel construites avec les connecteurs classiques
négation (-), conjonction (/\) disjonction (\/) et implication (=>).
En plus des connecteurs propositionnels, on trouve deux opérateurs temporels binaires utilisés en notation infixe:
- f EU g qui
signifie que pour une exécution : g deviendra vraie et que
f sera vraie jusqu'à ce que g le devienne.
- f AU g qui
signifie que pour toute exécution maximale : g deviendra vraie et que
f sera vraie jusqu'à ce que g le devienne.
Abbréviations
TRUE EU g | EF g |
TRUE A g | AF g |
- EF - g | AG g |
- AF - g | EG g |
|
Notations Equivalentes
f EU g (ou encore EF (f U g)) | Pot f g |
f AU g (ou encore AF (f U g)) | Inev f g |
EF g | Pot g |
AF g | Inev g |
AG g | All g |
EG g | Some g |
|
Quelques exemples de formules (où s0 est l'état initial du système)
-
M,s0 |= AG (p1 /\ p2) signifie que (p1/\p2) est vraie dans tous les états du système.
-
M,s0 |= EF (p1 /\ p2) signifie que (p1/\p2) peut devenir vraie dans le futur.
-
M,s0 |= AF (p1 /\ p2) signifie que (p1/\p2) deviendra inévitablement vraie.
-
M,s0 |= AG EF Init signifie que le système est réintialisable.
-
M,s0 |= AG EF EG Phi signifie qu'à partir de tout état,
on peut atteindre un état qui est l'origine d'une séquence où Phi
est constamment vraie.
Formules très pratiques
- dead est une propriété prédéfinie vraie uniquement sur les états de blocage
- Pas de blocage dans le système: AG - dead;
- Le système est bloqué dans tous les états: AG dead;
- Le blocage est inevitable AF dead
- Le marquage (m1,m3) n'est pas accessible AG - (m1 /\ m3);
- Si e1 arrive alors p1 sera vrai plus tard AG (e1 => AF p1);
II Invocation de MUSE (Model-Checker Mu-Calcul de TINA)
MUSE permet de vérifier la satisfaction de formules du Mu-Calcul.
Dans le cadre de ce TP on n'utilisera que la partie CTL en chargeant
la bibliothèque ctl.mmc (seule la partie
propriétés d'états est implantée).
L'invocation de MUSE nécessite au préalable la construction du graphe
des marquages. Celui-ci doit avoir été construit au format ktz.
Séquence type:
- Invocation de ND
- Invocation Construction du KTZ (onglet Tools : Reachability/Marking Graph - format ktz)
- Invocation de MMC (via clic droit souris dans le lecteur ktz)
- Chargement de la bibliothèque CTL : source ctl.mmc;
- Saisie et évaluation des formules.
- Ou directement, sans passer par ND, on peut aussi procéder en
ligne de commande :
ex muse bdd0.ktz -prelude ctl.mmc
- man muse pour plus de détails
L'évaluation d'une formule CTL renvoie l'ensemble des états satisfaisant la formule.
* Par défaut, Muse renvoie le cardinal de l'ensemble.
* Pour obtenir, la liste des états, ajouter l'option
-s en ligne de commande ou output set dans Muse
* L'option -b en ligne de commande ou output bool dans Muse
renvoie un résultat booléen suivant que l'état initial satisfait ou non la formule.
Pour obtenir les informations relatives à ces états le plus simple
est de construire l'espace d'états sous la forme verbose (tina bdd0.ndr > bdd0.txt) et de le consulter.
Contrairement à LTL, il n'y
aura pas de contre-exemple fourni lorsque la propriété est fausse.
L'outil pathto permet d'obtenir une séquence minimale
de transitions menant à un état donné.
Exemples d'utilisation
- pathto 102 pont.ktz
permet d'obtenir une séquence états/transitions menant à l'état 102
0 ABL2R 1 AR2L 7 ACL2R 19 AR2L 39 ADL2R 87 AR2L 102
- pathto 102 pont.ktz -t
permet d'obtenir une séquence de transitions menant à l'état 102
ABL2R AR2L ACL2R AR2L ADL2R AR2L
- Pour obtenir un contre-exemple jouable sous le stepper Tina
pathto 102 pont.ktz -t > pont.scn
pont.scn est un scenario rejouable via nd
- man pathto pour plus de détails
La bibliothèque CTL qui est fournie ne prend en compte que les propriétés
d'états (CTL standard et non SE-CTL).
III Quelques Exemples (voir Description )
Les formules correspondantes sont en gras. Toute requète se termine par un
;.
- Pont
- AF dead; Un blocage est inévitable
Vraie dans tous les états
- AF fin; Toute exécution arrive marque la place Fin
Vraie uniquement dans 15 états (sur 177)
- EF fin; Peut-on faire traverser le pont aux 4 scouts ?
Vraie uniquement dans dans 117 états.
- AG - (fin <=> dead); ???
Vraie dans 60 états. Le système est bloqué avant la fin dans 60 états.
- Pour s'assurer que 17 est bien le temps minimal
EF (fin /\ Temps <= 16);
Vide -> Impossible de faire traverser le pont aux 4 scouts en moins de 17 u.t
- Piscine
- dead; Tous les états de blocage.
Vraie en un seul état (28)
- AF dead; Tous les états où le blocage est inévitable.
Vraie uniquement pour l'état 28. On peut donc en déduire que
le blocage peut en tout état être évité.
- - EF dead; Y-a-t-il des états où le bloquage
ne risque pas de se produire ?
Vide -> aucun état.
- AG (x1 <= 7); x1 est 7-bornée
Vraie partout
- AG (x2 + x3 + x4 + x7 = 7);
Vraie partout -> Effectivement c'est un invariant de place du réseau
- Base de Données
- AG (lock <= 5); La place lock est 5 bornée
Tous les états
- AG - (reading /\ writting); Lecture et Ecriture sont exclusives
Tous les états
- De manière plus directe EF (reading /\ writting); Lecture et Ecriture sont exclusives
Aucun état
- AG (reading <= 5); Au maximum 5 lectures possibles en //
Tous les états
- AG EF reading; A partir de tout état on peut atteindre un état conduisant vers une lecture (reading est vivant au sens RdP)
Tous les états
- AG EF EG - reading; A partir de tout état on peut atteindre un
état origine d'une séquence où il n' y aura aucune lecture.
Tous les états