Skip to topic | Skip to bottom
Home
Minfo
Minfo.SeanceTdCPNToolsr1.1 - 06 Nov 2008 - 09:31 - OlivierDalletopic end

Start of topic | Skip to actions

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 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 pouvez utiliser directement la version installee sur le compte de Olivier Dalle en /u/profs/dalle/CPNTools. La commande a lancer est cpntools.

Premiers pas

Lisez la documentation sur ce site, elle est très bien faite: http://wiki.daimi.au.dk/cpntools/cpntools.wiki

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.

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 TransmitPacket et TransmitAck ? (Pensez aux généraux ...)

Réfléchissons un peu...

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

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 messahe 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).
to top


You are here: Minfo > IngenierieProtocoles > SeanceTdCPNTools

to top

Copyright © 1999-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding WIKIDeptinfo? Send feedback