 |
TIme petri |
 |
| Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
I Courte Introduction à la vérification avec LTL
Pour permettre la vérification de propriétés spécifiques, TINA dispose d'un model-checker pour la logique temporelle LTL (Linear Time 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 LTL s'évaluent sur l'ensemble des séquences d'exécution
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 exécutions du système S. On le note S |= f.
Les formules de LTL 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 : [] qui signifie toujours et <> qui signifie dans le futur.
Quelques exemples de formules:
- [] (p1 /\ p2) signifie que (p1/\p2) est vraie dans tous les états de l'exécution.
- <> (p1 /\ p2) signifie que (p1/\p2) deviendra vraie sur au moins un état de l'exécution
- [] (<> P) signifie que P sera vraie une infinité de fois pendant l'exécution
- <> ([] P) signifie que P deviendra définitivement vraie sur l'exécution
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: [] (- dead)
- Le système est bloqué dans tous les états: [] dead
- Le blocage est inevitable <> dead
- Le marquage (m1,m3) n'est pas accessible [] - (m1 /\ m3)
- Si e1 arrive alors p1 sera vrai plus tard [] (e1 => (<> p1) )
II Invocation de SELT (Model-Checker SE-LTL de TINA)
SELT permet de vérifier la satisfaction de formules de SE-LTL (une extension de LTL permettant de considérer de façon uniforme propositions d'états et propositions de transitions). En cas de non satisfaction, un contre-exemple fournissant une séquence d'exécution invalidant la formule est fourni. Celle-ci peut être automatiquement rechargée sous le stepper.L'invocation de SELT 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 SELT (via clic droit souris dans le lecteur ktz)
- Saisie et evaluation des formules.
Par défaut, il est présenté sous forme compactée. Pour l'obtenir sous la forme dépliée, il suffit de taper sous l'interpréteur selt la commande suivante : output fullproof;.
Il est possible de le charger automaiquement sous le stepper pour l'exécuter. Il suffit d'avoir le stepper en fonction et d'évaluer la formule. Le contre-exemple est directement chargé sous le stepper.
III Quelques Exemples (voir Description )
Les formules correspondantes sont en gras. Toute requète se termine par un ;.- Pont
- <> dead; Toute exécution se termine par un blocage
True - <> stop; (equivalent à <> Fin ) Toute exécution arrive marque la place Fin
False -> Le système peut se bloquer sans avoir atteint la fin du calcul (voir sequence contre-exemple) - [] - stop ; On ne peut pas executer stop (Peut-on faire traverser le pont aux 4 scouts ?)
False -> Le système peut exécuter stop. Le contre-exemple fourni précisément une exécution comportant stop - [] - (fin /\ Temps = 17); On ne peut pas arriver à fin en 17 u.t
False -> Si on peut y arriver (cf contre-exemple) - Pour s'assurer que 17 est bien le temps minimal
[] - (fin /\ Temps <= 16);
TRUE -> Impossible de faire traverser le pont aux 4 scouts en moins de 17 u.t
- <> dead; Toute exécution se termine par un blocage
- Piscine
- <> dead; Toute exécution se termine par un blocage
False - [] - dead ; Absence de Blocage
False (cf contre-exemple) - [] (x1 <= 3); x1 est 3-bornée
True - [] (x2 + x3 + x4 + x7 = 3);
True -> Effectivement c'est un invariant de place du réseau
- <> dead; Toute exécution se termine par un blocage
- Base de Données
- [] (lock <= 5); La place lock est 5 bornée
True - [] - (reading /\ writting); Lecture et Ecriture sont exclusives
True - [] (reading <= 5); Au maximum 5 lectures possibles en //
True - [] - (reading = 5);
False -> Le contre-exemple fournit une exécution où 5 lectures ont lien en // - []( arrivee_lecteurs => <> debut_lecture);
Toute arrivée de lecteurs sera suivie par une lecture
False -> Il peut y avoir famine. L'accès en écriture ou en lecture n'est pas équitable.
Voir le contre-exemple fourni - [] (debut_lecture => <> fin_lecture);
Tout début de lecture sera suivi par une fin de lecture
True
- [] (lock <= 5); La place lock est 5 bornée