TP Vérification de Protocoles - CADP / Tina
http://www.laas.fr/~francois/POLYS/ENSEIGNEMENT/VP/
TINA / CADP :
- Home Page CADP
- Home Page Tina
- SE-LTL
Chemins d'accès :
Directives à ajouter dans votre environnement (.bashrc).
export CADP=/usr/local/insa/cadp
export PATH=$CADP/bin.`$CADP/com/arch`:$PATH
export PATH=$CADP/com:$PATH
Alternative : source ~vernadat/.cadprc
Quelques outils de CADP : bcg_io, bcg_labels, bcg_min, aldebaran
bcg_io : Formats d'entrée et conversion :
Les LTS seront, suivant les outils utilisés,
au format textuel (.aut) ou au format binaire (.bcg).
L'outil
bcg_io permet de passer d'un format à l'autre.
Ainsi
bcg_io lts.aut lts.bcg produit un lts au format bcg à partir
d'un lts au format .aut, tandis que
bcg_io lts.bcg lts.aut produit un .aut à partir d'un .bcg.
Les fichiers .aut sont visualisables en utilisant
nd
bcg_labels : Renommage / Masquage :
- Le masquage permet de cacher les événements que l'on ne désire pas observer.
La description des événements observés est décrite dans un fichier .hide
tel que celui-ci serv1.hide
L'outil bcg_labels permet de réaliser le masquage.
la commande bcg_labels -hide serv1.hide lts.bcg lts-serv1.bcg produit un fichier lts-serv1.bcg en cachant (renommant par i)
toutes les transitions du lts initial (lts.bcg) que l'on voulait effacer.
- Le renommage permet de renommer des événements.
La description du renommage est réalisée dans un fichier .rename
tel que celui-ci autres.rename
L'outil bcg_labels permet de réaliser le masquage.
la commande bcg_labels -rename autres.rename lts.bcg lts-autres.bcg procède au renommage des transitions de lts.bcg et
produit le fichier renommé lts-autres.bcg.
aldebaran : Equivalence de Sûreté (safety equivalence)
La commande
aldebaran -smin lts.aut > lts_smin.aut construit la projection de lts relativement à
l'équivalence de sûreté (proche de l'équivalence langage) et produit le résultat dans lts_smin.aut
bcg_min : Equivalence Observationnelle
Pour obtenir la projection d'un LTS suivant relativement à l'équivalence observationnelle (option par défaut)
ou pour obtenir l'ensemble quotient avec la mention et la localisation explicite des tau-cycles.
- La commande bcg_min -observational lts.bcg lts_omin.bcg construit la projection de lts relativement à
l'équivalence observationnelle et produit le résultat dans lts_omin.bcg
- La commande bcg_min -observational -class - lts.bcg affiche la
liste des classes d'équivalence en mentionnant et en localisant les éventuels tau-cycles (livelock) pouvant provoquer des
problèmes de divergence.
I Exemple du Token-Ring
Pour cet exemple, on s'intéresse à vérifier deux propriétés : l'exclusion mutuelle (au maximum un client travaille) et l'absence de famine (tout client ayant demandé à travailler devra travailler au bout d'un temps fini). Les techniques de projection offertes par CADP vont permettre de vérifier si ces propriétés sont satisfaites et dans la négative permettre d'aider à comprendre pourquoi ces propriétés ne le sont pas.
- Recopiez le script ctk0 permettant de générer un token ring à K sites
(usage ./ctk0 4 > tk4.net )
- Construisez son graphe de marquages via tina ( nd tk4.net ) au format lts
- Visualisez le via nd ( nd tk4.aut)
- Convertir le fichier .aut en fichier .bcg : bcg_io tk4.aut tk4.bcg
- Visualisation du service local pour le client du site 1 (Equivalence Observationnelle)
- On définit les événements observables dans le fichier
serv1.hide
- On définit les événements observables dans le fichier
serv1.hide
Dans ce cas, on cache tous les événements sauf ceux ayant trait
au client du site 1.
- On obtient un LTS renommé via la commande:
bcg_labels -hide serv1.hide tk4.bcg tk4serv1.bcg
- On obtient le LTS quotient (la projection) pour l'équivalence observationnelle via la commande ci-dessous:
bcg_min -observational tk4serv1.bcg tk4serv1-omin.bcg
- Pour visualiser la projection, repassez en .aut via bcg_io et dessinez via nd :
bcg_io tk4serv1-omin.bcg tk4serv1-omin.aut ; nd tk4serv1-omin.aut
- On obtient l'ensemble des classes d'équivalence via la commande:
bcg_min -observational -class - tk4serv1.bcg
Localisez les classes contenant des tau-cycles. Que peut-on dire ?
- En vous inspirant du fichier serv1.hide et des opérations précédentes,
construisez et visualisez le service local pour le site 1
(les seuls événements observables seront ceux du site 1 : ceux du client ainsi que ceux de la station)
Que peut-on en déduire ?
- Proposez une projection permettant d'observer la circulation du jeton entre les différents sites.
Que pouvez-vous en déduire ?
Etudiez la possibilite de livelocks. Que peut-on en déduire ?
- Vérification de la propriété d'exclusion mutuelle en utilisant CADP :
Proposez une solution en vous inspirant de ce qui a été fait en cours et en utlisant l'équivalence de safety (outil aldebaran).
- Pour éliminer les problèmes de famine, le générateur est modifié. Recopiez le nouveau générateur stk .
Construisez les différentes projections (systemes quotients) et effectuez les comparaisons.
II Un pont et 4 scouts
- Recopiez l'exemple du pont pont.ndr
- En le simulant, assurez-vous que l'on peut :
- faire traverser le pont aux 4 scouts (exécuter la transition stop),
- faire traverser le pont aux 4 scouts en 17 u.t,
- bloquer le système avant que les 4 scouts n'aient traversé (ca c'est un bug!).
- Peut-on être sûr, par simulation, que 17 est le temps minimal ?
- Pour info (demander à FV), regardez ici pour voir comment on peut procéder pour vérifier ces propriétés en utilisant une approche logique temporelle. On va faire de même en utilisant maintenant l'équivalence observationnelle.
- On cherche à étudier la "correction partielle" : vérifie que
lorsque le programme termine, le calcul est correctement fini
(ici les 4 scouts ont traversé)
* Obtenez une projection observationnelle où seul stop est visible.
* Que suggère le modèle obtenu ?
* Quelle peut-être la provenance de l'événement inobservable i ?
* Pour étudier la "terminaison", regarder s'il existe
des livelocks (tau-cycles).
* Quelle est votre conclusion ?
- On cherche maintenant à visualiser les scenarii conduisant
à une terminaison incorrecte.
* Obtenez une projection observationnelle où seul stop et les événements de retour sont visibles. Le résultat obtenu est-il exploitable ?
Peut-il exister des livelocks ?
* Pour diminuer la complexité de la projection précédente,
vous renommerez tous les événements de "retour"
de facon indifférenciée, idem pour les événements d'"aller".
- Corrigez le modèle de pont initialement fourni. Vérifiez que votre solution est correcte (correction partielle + terminaison).
A faire en fin de séance ou à la maison
Partant de votre modèle corrigé, proposez une approche permettant
d'obtenir - en utilisant l'équivalence observationnelle et CADP -
le plus petit temps de traversée.
Vous avez le droit d' "instrumenter" le réseau et vous pouvez ajouter,
en particulier, des transitions non intrusives permettant d'observer l'état
du système.
III Alternating Bit Protocol
- Recopiez l'exemple du bit alterné abp.ndr ainsi que quelques slides de présentation
slides.pdf
Demandez quelques explications orales à FV
- Simulez le via nd (onglet tools -> stepper)
- Construisez son graphe des classes en mode lts (.aut)
- Visulalisez le graphe des classes via nd
- En utilisant bcg_min (observationnal equ) et aldebaran (safety eq)
- Visualisez le service offert coté émetteur
- Visualisez le comportement de l'entité de protocole
associée à l'émetteur
- Visualisez le service offert coté récepteur
- Visualisez le comportement de l'entité de protocole
associée au récepteur
Donnez une explication à la présence de transitions inobservables
- Visualisez le service offert coté médium
Démonstration SELT (FV): vérifiez les propriétés décrites dans le fichier
abp.ltl
A l'issue de cette question, vous devez avoir compris l'ensemble des formules
et des réponses (et des contre-exemples) qui auront été fournies par SELT.
IV Interblocage
- On considère un système composé par deux clients et deux gestionnaires de ressources.
Chaque client a besoin pour travailler des deux ressources.
Dans le modèle proposé, les deux clients demandent les deux ressources dans un ordre différent et un interblocage peut survenir.
Un tel système peut se représenter par le réseau syst2.ndr
- Recopiez le réseau et simulez-le via nd
Construisez son graphe de marquages au format ktz (utilisable par SELT)
et au format lts (utilisable par CADP/aldebaran)
- Etude des états de blocage:
La commande aldebaran -dead syst2.aut fournit l'ensemble des états de deadlock (1 seul etat ici, l'état 17)
La commande aldebaran -path 17 syst2.aut fournit un chemin conduisant à l'état 17
- Construisez les services locaux associés à chacun des clients
- Proposez un critère d'observation permettant de s'assurer que chaque ressource est utilisée
en exclusion mutuelle
- Proposez un critère d'observation permettant de s'assurer que chaque client
travaille en exclusion mutuelle
- Proposez un ensemble d'événements observables permettant d'obtenir en utilisant aldebaran une
explication du probleme d'interblocage.
Pour obtenir des modèles plus concis, vous pourrez utiliser l'équivalence de sûreté (safety equivalence) au lieu de l'équivalence observationnelle (option -smin au lieu
de -omin).
nb: De facon informelle, l'équivalence de sûreté conserve le séquencement d'actions
(comme l'équivalence langage) mais aussi la présence d'états de blocage (comme l'équivalence
observationnelle).
- Résolution de l'interblocage : L'un des 4 composants est capable de détecter l'interblocage. Lequel ? proposez et implantez une solution permettant de résoudre l'interblocage.
En utilisant les différentes techniques de vérification, assurez-vous de la correction de votre solution.