Avant d'aborder ce TP, il convient de découvrir le langage de spécification de protocoles Promela. Le document PolyPromela vous permet d'en connaitre la syntaxe. L'archive PremiersTestsPromela contient 6 programmes à charger dans l'outil xspin, puis à exécuter (Run -> Run Simulation) de plusieurs manières (Run -> Set Simulation Parameters).

Après cette phase de familiarisation à Promela, vous devez écrire quatre protocoles de plus en plus complexes et les exécuter/tester à l'aide de l'outil xspin. La couche physique est matérialisé par des canaux (chan en Promela). 
Les protocoles devront être exécutés avec plusieurs valeurs de "seed" et testés lors d'une phase de vérification.

1. Protocole utopique

Dans un premier temps, on considère un émetteur et un récepteur qui transmettent leur données via un canal fiable : pas de perte, pas de duplication, pas d'erreur, pas de désequencement.

2. Protocole "Send and Wait" dans un cas sans perte

On suppose cette fois que le récepteur ne parvient pas forcément à traiter les trames au rythme d'envoi imposé par l'émetteur. Pour éviter de saturer le tampon du récepteur, l'émetteur attend, après l'envoi de chaque trame, un acquittement du récepteur indiquant que celui-ci est prêt à traiter un nouveau paquet.

3. Protocole "Send and Wait" dans un cas avec pertes

Cette fois, la couche physique peut perdre des données. Il s'agit alors d'adapter le protocole précédent en introduisant des retransmissions. La perte de paquet est réalisée par un processus Medium qui reçoit et retransmet les paquets avec d'éventuelles pertes. On pourra alors prévoir 4 canaux, deux canaux entre l'émetteur et le medium, un dans chaque sens de transmission, et deux canaux entre le récepteur et le médium.

4. Protocole piggybacking

Pour finir, on envisage un protocole dans lequel chaque coté est à la fois émetteur et récepteur. Les acquittements sont alors joints aux trames de données (piggybacking).