Enseignements

Seance CPN Tools

Seance de TD sur CPNTools

Pour finir ce cours d’initiation à l’Ingénierie des Protocoles nous allons expérimenter l’outil CPNTools développé par le Prof. K. Jensen et le CPN Group de l’Université d’Aarhus au Danemark.

CPN signifie Colored Petri Nets. C’est une extension des Réseaux de Petri dans laquelle les jetons peuvent avoir différentes couleurs. Et pour cela on autorise des tests (en particulier sur la couleur des jetons) au niveau des arcs (pre- et post-conditions). Cette extension est intuitivement facile à comprendre, nous allons la découvrir et l’expérimenter sur le tas.

Installation

CPNTools est un outil très puissant, dont l’ergonomie est assez originale et ludique, mais très exigeant en terme de configuration car utilisant le standard OpenGL. En pratique, le programme n’est disponible que sous forme binaire, et seulement pour Linux et Windows. Mais sur MacOs, on peut eventuellement le faire tourner dans une machine virtuelle Windows (ca marche très bien sur mon <nop>MacBook Pro Intel).

Le programme n’est pas librement téléchargeable, mais l’Université d’Aarhus nous a accordé un droit d’utilisation. Vous trouverez l’archive .tar.gz sur le compte de Olivier Dalle. Sur les machines Linux de la fac, vous NE pouvez PAS utiliser directement la version installee sur le compte de Olivier Dalle en /u/profs/dalle/CPNTools, decomprimez l’archive cpntools_2.3.5.tar.gz sur votre compte, ou en /tmp si vous manquez de place. La commande à lancer est cpntools.

Premiers pas (Seance 1)

Lisez la documentation sur le site cpntools, elle est très bien faite: http://cpntools.org/documentation/start

On vous y explique en particulier ce qui fait l’originalité de l’interface, ce menu qu’on obtient en cliquant avec le bouton droit.

Lors du demarrage de l’application ou du chargement d’un RdP, il est courant que les traits (pre- et post-conditions) n’apparaissent pas. C’est un petit bug de l’outil, vous pouvez corriger en deplacant les elements graphiques ou en redimmensionnant la fenetre pour forcer le rafraichissement de l’affichage.

Ouvrez un exemple de Réseau de Petri, par exemple les philosophes, et essayez de comprendre son fonctionnement. Remarquez que grace a l’utilisation des couleurs, il n’y a besoin de décrire qu’un seul philosophe.

Remarquez ce qui se passe lorsque vous “tirez” les éléments du menu Toolbox dans la partie gauche avec la souris vers la zone de droite. Entrainez-vous un peu…

Essayez de faire tourner l’exemple pas à pas a l’aide du menu de simulation. Vous pouvez choisir précisément quel jeton utiliser, ou lancer la simulation pour un certain nombre d’etapes. Expériementez ces différentes options.

Expérimentez le menu State Space. Lancez l’action de proudction de rapport, et analysez le resultat.

Un protocole simple

Ouvrez l’exemple SimpleProtocol. Faites le tourner et cherchez une explication précise du role de chaque élement du réseau: les places, les arcs, les couleurs, etc.

Ce réseau est-il k-borné ? Pourquoi ?

Y a-t-il un moyen de le rendre k-borné sans changer la partie centrale du réseau (les transitions <nop>TransmitPacket et <nop>TransmitAck ? (Pensez aux généraux …)

Réfléchissons un peu… ( a terminer avant la seance 2)

Avez-vous remarque que la liste initiale des messages ne s’épuise jamais ? En fait, ce réseau ne fait pas la différence entre les messages que l’on envoie pour la première fois et ceux que l’on ré-envoie.

Modifiez ce réseau de facon a corriger cela, cad faire en sorte que la liste des messages a envoyer pour la première fois s’épuise. Vous pouvez par exemple ajouter de nouvelle places pour représenter la liste des messages déjà envoyés en attente de confirmation.

Modifiez maintenant le protocole précédent de telle facon que le message d’acquittement contienne systématiquement le numéro du paquet recu par le destinataire. Il faudra donc faire en sorte que l’emeteur ignore les acquitements pour des messages deja envoyés et acquités. Il faudra aussi faire attention à ce que le destinataire continue de recevoir et d’accepter les paquets dans le bon ordre (en particulier il ne faut pas permettre que la place Received recoive plusieurs fois le meme message).

On souhaite maintenant modéliser le fait que perdre plus de 3 fois le meme message est tellement improbable que ca ne peut pas se produire. (Au fait, pourquoi peut-on vouloir modéliser une telle chose au lieu de la réalité ?). Pour cela on va modifier le réseau de telle facon qu’il se souvienne de ce qu’il a transmis, et fasse en sorte que si le message est deja passé trois fois, alors il est remis de facon certaine à la destination (ou à la source dans le sens des acquittements). Une fois que cette dernière modification est effectuée, utilisez l’analyse statique pour vérifier les bonnes propriétés de votre réseau de Petri.

Pour aller plus loin (Seance 2, a rendre a la fin de la seance).

Le protocole CSMA-CA est le protocole utilisé par les réseaux radio WiFi. Pour eviter les collisions, il utilise une technique consistant à signaler d’abord son intention d’envoyer avant d’envoyer vraiment. Pour cela le temps est decoupé alternativement en périodes de contention et période de transmission. Durant la période de contention, les stations candidates envoient un message RTS (Request To Send). Si ce message n’est pas collisionné alors le destinataire envoie un message CTS (Clear To Send). Puis aprés un certain délai, les stations commencent à échanger. Pendant cet échange, les autres stations qui ont vu passer l’échange RTS/CTS sont supposées rester silencieuses jusqu’à la fin de l’échange.

Il faudra donc modéliser les différentes périodes (contention, échange) et état du canal durant la période de contention (si 1 message Ok, si plus que 1 contention).

INDICATIONS

  • L’objectif du TP est simuler 3 stations qui communiquent en utilisant le protocole CSMA-CA.
  • Pour montrer (de facon informelle) que le protocole fonctionne, votre simulation devra montrer que chaque station parvient a envoyer un message a chaque autre station.
  • Au depart vous chaque station devra donc etre dans etat initial comportant un message a envoyer vers chacune des deux autres stations.
  • Pensez a utiliser les “couleurs” (jetons typés) de CPN: chacune des 3 station execute exactement le meme protocole, mais en utilisant des jetons de couleur differente. Comme dans l’exemple des philosophes, vous n’avez donc besoin de représenter l’automate que d’une seule station.* Comme dans l’exemple du protocole simple, vous devrez représenter l’état du réseau (libre, occupé sans collision, occupé avec collision).
  • Gestion du non determinisme:
    • initialement, chaque station a deux messages a envoyer, soit 6 messages en tout. On ne sait pas a l’avance quel message sera choisi pour etre envoye le premier, ni quelle station commence: vous devez laisser CPN faire ce choix. Attention: votre solution doit pouvoir fonctionner aussi avec plus que 3 stations et/ou plus que 2 messages initiaux. Cela signifie que votre solution ne doit pas dependre du nombre de messages restant a envoyer.
    • deux stations peuvent choisir de commencer en meme temps, ou presque, ce qui doit normalement conduire a une collision.
    • Attention: une station ne peut pas envoyer son deuxieme message avant d’avoir fini d’envoyer le premier. Initialement, sur chaque station il y a donc un choix du message a envoye qui rend l’envoi du message suivant impossible tant que le premier n’est pas fini d’envoyer.
  • Types des messages: les messages pourront etre representes a l’aide de jetons. Chaque message comporte un type (RTS, CTS, DATA, …) un expediteur et un destinataire, donc les jetons auront 3 dimensions.

Ne vous jetez pas sur l’outil CPNTools des la premiere minute. Commencez reflechir avec un papier et un crayon. Une fois que vous avez une solution sur le papier, la réalisation ira très vite!

Vous DEVEZ rendre une premiere version de votre projet sur jalon a la fin de la seance, ou au plus tard dans l’heure suivante. Ensuite, vous pourrez encore améliorer votre solution (éventuellement) pendant quelques jours. Vous deposerez votre projet CPNTools définitif sur Jalon au plus tard le 13 novembre minuit. Vous pouvez travailler en binôme, mais pas plus que 2 etudiants par projet. Il est interdit de copier sur le voisin ou de laisser le voisin copier sur votre projet. Votre archive doit etre un fichier zip faisant apparaitre votre nom ou les noms des deux binomes. L’archive contenant le version definitive doit avoir le suffixe additionnel “final”. L’archive doit produire un repertoire unique contenant tous vos fichiers, Ce repertoire doit aussi faire apparaitre votre(vos) nom(s). Exemple: OlivierDalle-final.zip, contenant OlivierDalle-final/CSMA-CA.cpn …

retour a la page du cours…

Page d’Accueil

Enseignements 2017-18

Enseignements Antérieurs

Recherche…

edit SideBar

Blix theme adapted by David Gilbert, powered by PmWiki