Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
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: