TP Vérification de Protocoles - CADP / Tina
http://www.laas.fr/~francois/POLYS/ENSEIGNEMENT/VP/
Ouverture fermeture de connexion
Dans cet exercice on reprend le problème de l'ouverture fermeture de
connexion dans l'UF Modélisation de Systèmes Concurrents
(la modélisation avait été faite en
utilisant des automates communicants et UPPAAL).
Pour ce TP, la modélisation
sera effectuée en réseaux de Petri
communicants
avec TINA et la vérification en utilisant CADP.
La description du protocole et des services attendus est fournie
ici .
Pour arriver au protocole complet, quatre étapes sont définies. Pour
chacune de celles-ci, le
service attendu est décrit par un
automate. On va reprendre chacune de ces étapes (les deux premières
sont fournies) et on utilisera le mécanisme de projection de CADP pour
obtenir le
service effectivement fourni. La vérification
consistera à s'assurer que le service effectivement fourni correspond
bien au service (initialement) attendu.
Dans le cadre de ce travail, nous utiliserons deux relations
d'équivalence: l'équivalence observationnelle (option -omin) et
l'équivalence de sûreté (option -smin). Celle-ci correspond (à peu
près) à l'équivalence de traces maximales (une équivalence langage
préservant les blocages).
I Récupération des sources
Récupérez les sources dans le répertoire
suivant /home_pers/vernadat/VP24
(i.e cp -R /home_pers/vernadat/VP24 .) Certains fichiers sont protégés en lecture et ne pourront pas être copies.
Les entités de protocole (cf init0.net et resp0.net)
correspondant à la 1ère question
sont fournies. Pour la seconde question, seul le comportement de
l'initiateur (init1.net) est fourni.
Sont également fournis les systèmes complets, i.e., la
composition des entités Init et Resp et des deux files de communication
(voir cf ec0.tpn, ec1.tpn).
Les fichiers de masquage (init.show, resp.show)
sont fournis et couvrent les 2 premières questions.
- La description du modèle TINA
- Les fichiers ecXX.tpn correspondent à la mise en communication des
4 entités communicantes en présence :
les deux entités de protocole (initiateur et répondeur) ainsi que les deux files de communication les reliant. La description de cet assemblage est assez proche de celle que l'on pourrait faire en algèbre de processus : chaque entité possède des portes qui sont renommées afin de permettre l'assemblage des composants.
- La description des entités est réalisée en réseaux de Petri étiquettés: une transtion peut posséder un label qui correspondra à un événement de communication. La modélisation proposée utilise deux PDUs CR et DR et 4 événements sont considérés l'émission et la réception de ces quatre PDUs. (Voir exemple de comportement :
fichiers init0.net et resp0.net).
- Les files sont des fifos de taille 4 pouvant faire transiter deux types de messages différents. Leur taille est bornée et toute tentative de dépassement de capacité se solde par une mise en état d'erreur conduisant à un blocage.
- Les fichiers d'observation (.show) décrivant respectivement
les événements observables pour l'initiateur et le répondeur.
- Les fichiers correspondant aux différentes projections obtenues :
2 pour le service local offert à l'initiateur (smin et omin) et
2 pour le service local répondeur.
- Le script run qui permet de lancer les différents softs
(TINA et CADP) et d'obtenir les différentes projections.
Lire le script.
II Question I
Dans un premier temps, on suppose que seul l'un des deux usagers
(init) est apte à ouvrir et à fermer une connexion. L'autre (resp)
peut par contre accepter ou refuser les offres de communication. De
plus, l'initiateur ne peut fermer qu' une connexion déjà ouverte.
La modélisation est déjà réalisée.
(cf modèles init0.net, resp0.net et assemblage ec0.tpn)
- Regardez les différents fichiers de comportement (suffixe .net) ainsi que le fichier (.tpn) décrivant la composition.
- Vous pouvez simuler le modèle global via nd. Vu la taille du réseau, il est conseillé de le faire en textuel.
- Exécutez le script run
- Equivalence de sûreté (suffixe smin) : Assurez-vous que les services offerts respectivement à l'initiateur et au répondeur sont identiques (isomorphe au nommage des transitions près) aux services attendus (cf feuille de TP).
- Equivalence Observationnelle (suffixe omin) : Comparez les résultats obtenus avec l'équivalence de Safety. Expliquez la présence ou l'absence de transtions inobservales externes (étiquetées i par CADP).
II Question II
On suppose maintenant que les deux usagers peuvent clore une connexion ouverte.
La modélisation est partiellement réalisée: l'intiateur est fourni
(init1.net), vous devez modéliser le récepteur (resp1.init).
- Equivalence de sûreté (suffixe smin) : Assurez-vous que les services offerts respectivement à l'initiateur et au répondeur sont identiques (isomorphe au nommage des transitions près) aux services attendus (cf feuille de TP).
- Equivalence Observationnelle (suffixe omin) : Comparez les résultats obtenus avec l'équivalence observationnelle.
III Question III
En vous inspirant des questions précédentes,
résolvez les questions
- 3) On suppose maintenant que l'initiateur a la possibilité
de clore une une connexion en cours d'établissement.
- 4) On suppose maintenant que les deux usagers ont
le même pouvoir -
tous deux sont capables d'initier et de rompre des connexions.
Les deux usagers seront donc représentés par un seul process