L'architecture générale du protocole du bit alterné est :
et les automates qui décrivent le fonctionnement de l'émetteur (automate (a)) et du récepteur (automate (b)) sont :
On désire modéliser ce protocole en Promela et puis vérifier des formules Ltl en utilisant Spin.
On modélise les canaux de communication K et L par des canaux Promela ayant une longueur constante (à choisir), strictement positive.
Le type des messages qui circulent sur ces canaux est bit, c'est-à-dire qu'on fait abstraction des messages envoyés et on considère uniquement le bit qui accompagne les messages.
Donner la déclaration des canaux de communication K et L.
On modélise les canaux de communication SND et RCV par deux variables de type bit, c'est-à-dire qu'on fait abstraction des messages envoyés par les clients et on suppose qu'il sont égaux au bit alterné émis resp. reçu.
Donner la déclaration de SND et RCV.
On modélise l'émetteur (processus sender) par un processus Promela qui implémente l'automate (a).
Ce processus est paramétré par deux canaux : in sur lequel l'émetteur reçoit des messages et out sur lequel l'émetteur envoie des messages.
Pour la modélisation de l'automate, utiliser les étiquettes et les instructions ``goto'' du C.
Pour la modélisation la transition étiquetée par SND, affecter la variable SND au bit alterné émis et afficher un message (avec ``printf'').
Donner la définition du processus sender en utilisant un nombre minimum d'états (< 6).
On modélise le récepteur (processus receiver) par un processus Promela qui implémente l'automate (b).
Ce processus est paramétré par deux canaux : in sur lequel le récepteur reçoit des messages et out sur lequel le récepteur envoie des messages.
Pour la modélisation la transition étiquetée par RCV, affecter la variable RCV au bit alterné reçu et afficher un message (avec ``printf'').
Donner la définition du processus receiver en utilisant un nombre minimum d'états (< 6).
Donner la définition du processus ``init''.
Simuler avec Spin le comportement du système ainsi modélisé.
Donner la formula Ltl qui exprime la propriété p : ``tout message envoyé par l'émetteur est reçu par le récepteur sans erreur au moins une fois''.
Vérifier avec Spin cette propriété et expliquer (en quelques lignes) le résultat obtenu.
Modifier la définition des processus sender et receiver pour modéliser l'occurrence d'une erreur à la réception de l'acquittement resp. du message.
Il s'agit d'ajouter à l'automate (a) deux transitions étiquetées err, l'une partant de l'état 2 vers l'état 1 et l'autre partant de l'état 5 vers l'état 4. Pareil pour l'automate (b) : de l'état 3 vers l'état 2 et de l'état 0 vers l'état 5.
Pour la modélisation, utiliser ``printf'' sur signaler l'occurrence d'une erreur.
Pour cette nouvelle modélisation, vérifier la propriété p avec Spin et expliquer (en quelques lignes) le résultat obtenu.
