Vérification automatique de protocoles. Un "Model-Checker" pour CCS

On donne ici des compléments au projet informatique.

Exemple de code CCS

On s'intéresse ici à un protocole de communication entre deux agents, supposés permettre le bon acheminement des messages même lorsque les lignes de communications ne sont pas parfaites. On doit quand même supposer un certain nombre de choses concernant ces lignes: elles peuvent simplement perdre ou dupliquer un message, mais pas le corrompre. On va représenter nos deux agents par des termes CCS Send et Reply, dont le seul but est pour l'un d'envoyer des messages sur une ligne (un buffer \`a capacité infinie), également représentée par un terme CCS Trans, vers Reply, qui lui, va renvoyer un reçu \`a Send, par la ligne Ack. Ces deux lignes sont censées être imparfaites dans le sens explicité plus haut. Pour communiquer, Send et Reply vont utiliser le protocole du bit alterné. Le nom du protocole vient du fait que chaque message va être taggé, alternativement par un 1 et par un 0:

Send fonctionne de la façon suivante:
- Il prend un message à envoyer sur un canal accept
- Il l'envoie taggé avec un bit b le long de Trans et démarre une horloge (représentée par un terme CCS Timer)
- Il y a alors trois possibilités:
  - Il reçoit un timeout du timer: alors il renvoie le même message sur Trans. toujours taggé avec le même bit.
  - Il reçoit une confirmation de réception sur la ligne Ack avec la valeur b: il est alors prêt à recevoir un nouveau message (qu'il renverra avec le bit 1-b).
  - Il reçoit 1-b sur la ligne Ack: il ne fait rien.
Reply fonctionne d'une façon duale:
- Lorsqu'il reçoit un message sur Trans, il renvoie le bit b avec lequel il avait été taggé, sur la canal Ack, renvoie le contenu du message sur le canal deliver et met en route une horloge.
- Il y a alors trois possibilités:
  - Il reçoit un timeout de l'horloge: il renvoie le message b sur la ligne Ack.
  - Il reçoit un nouveau message taggé avec le bit 1-b sur la ligne Trans: il peut alors délivrer le nouveau message, qu'il confirme sur la ligne Ack avec le bit 1-b.
  - Il reçoit un message avec bit b: il l'ignore.

Pour écrire les termes CCS correspondants, on paramètre Send et Reply par l'état courant du bit. On écrira ainsi Send(b) pour Send dans lequel le bit est à la valeur b. De plus, on écrira ici bar(a) pour l'envoi sur le canal a. Les codes CCS correspondants sont:

Send(b)=bar(send_b).bar(time).Sending(b)
Sending(b)=timeout.Send(b)+ack_b.timeout.Accept(1-b)
Accept(b)=accept.Send(b)
Reply(b)=bar(reply_b).bar(time).Replying(b)
Replying(b)=timeout.Reply(b)+trans_(1-b).timeout.Deliver(1-b)+trans_b.Replying(b)
Deliver(b)=bar(deliver).Reply(b)
Timer=time.bar(timeout).Timer

Pour les lignes Ack et Trans, il faut paramétrer les termes CCS correspondants par les bits encore en circulation sur les lignes. Ils sont donc paramétrés par des chaînes de bits. On a ainsi:

Ack(sbt)=tau.Ack(sbbt)+tau.Ack(st)
Ack(s)=reply_b.Ack(sb)
Ack(bs)=bar(ack_b).Ack(s)
Trans(tbs)=tau.Trans(tbbs)+tau.Trans(ts)
Trans(s)=send_b.Trans(bs)
Trans(sb)=bar(trans_b).Trans(s)

Vérification automatique de protocoles. Un "Model-Checker" pour CCS

Exemple de code CCS

Exemples de formules CTL

Quelques pointeurs

Pour me joindre...