Exemple d'un protocole de communication : L'analyse du protocole TCP

Présentation de TCP

TCP est un vieux protocole, défini à l'origine en 1981. Le but de ce protocole est de fournir des connections pour le transfert fiable de données entre des processus s'exécutant sur des ordinateurs différents connectés par l'Internet. Le réseau Internet fournit la transmission de paquets (protocole IP) qui n'est pas fiable (des paquets peuvent se perdre ou arriver en désordre, même être dupliqués). L'architecture de système pour TCP est l'architecture typique pour des protocoles de communication en général, comme montré dans la figure (a). La figure (b) montre la vue "boîte noire" du système TCP montrant les interfaces par lesquels la communication fiable est fournie aux programmes d'usagers. Pour simplifier, la figure montre seulement deux ports (interfaces) par lesquels des applications dans deux ordinateurs différents peuvent communiquer d'une façon fiable. Ces ports sont aussi appelés points d'accès au service (SAP - service access point).

TCP est un protocole assez complexe, considérant en particulier les extensions qui ont été ajoutées avec le temps. Dans ce qui suit, nous prenons une vue abstraite, considérant seulement la première phase du protocole qui établit une connexion logique entre les deux usagers sur les ordinateurs différents. Nous considérons les interactions qui précèdent l'état connecté dans lequel les échanges de données ont lieu (mais l'échange des données n'est pas modélisé dans ce qui suit).

L'établissement d'une connexion TCP est basée sur un échange de trois messages ("three-way handshake). En effet, chaque partie doit envoyer un message sync qui propose un numéro de séquence pour la numération des données échangées, et qui doit être suivi par un message d'acquittement ack de l'autre côté. Cela donne normalement lieu au diagramme de séquencement (a) (le deuxième message contient les deux, un acquittement du premier sync, et un sync de l'autre côté).

Définition du service de communication offert par TCP

Lorsque TCP a été développé, les concepteurs se concentraient sur la vue "boîte blanche" (définissant les règles pour les échanges de messages entre les deux entités de protocole), parce que la notion de service de communication (vue "boîte noire") n'était pas encore bien établie. Dans ma publication de 1980 la vue "boîte noire" étaient promue pour la première fois. Dans les années 1980, les travaux de normalisation OSI donnaient lieu à des spécifications de services typiques pour l'établissement de connexions comme montrées dans la figure (b). Ceci implique un Request par l'initiateur de la connexion, suivi par une Indication du côté du récepteur de la connexion, suivi par une Response positive (si l'usager accepte la demande de connexion), et finalement suivi par une Confirmation chez l'initiateur. Ceci est similaire que pour le service de téléphone quand une connexion est établie entre usager A et B: A.activate-phone, A. dial-number, B.ring, A.hear-ringing, B.activate-phone, both.talk.

La spécification de service ci-haut implique des entrées et des sorties entre l'usager et l'entité de protocole. Ces interactions sont souvent appelée primitive de service. Ceci est naturelle pour des systèmes modélisés par des machine à états. Les interfaces sont assez symmétriques entre usager et entité (fournissant le service).

Par contre, les concepteurs de TCP étaient des programmeurs qui n'étaient pas habitués à des vues abstraites; ils utilisaient ce que les languages de programmation fournissaient. Les langages de programmation offrent normalement des API (Application Programming Interfaces) en forme d'un ensemble de procédures (ou méthodes dans l'approche OO). Ceci donnait lieu à l'interface socket pour TCP dont il y a aussi une version en Java. Ici l'application doit décider si elle veut initier une connexion (appellant la procédure connect) ou recevoir une connexion (appellant la procédure listen). Cet interface n'est pas symmétrique entre le côté initiant et repondant.

Définition du protocole TCP

Les noms de procédures de l'interface de service TCP ont été inclus dans la machine à états qui modélise le protocole TCP, comme montré dans le modèle du Wikipedia ci-dessous.

Utilisant l'outil LTSA pour analyser le protocole TCP

Version simplifiée

Nous commençons avec une version simplifiée où l'usager A est l'initiateur d'une connexion vers l'usager B. Utilisant le diagramme de séquencement (a) ci-haut, et suivant les lignes verticale du temps, on peut dériver la séquence des opérations d'envoi et de réception à être exécutée par chacune des entités. Ces séquences d'opération peuvent ensuite être modélisées par des machines à états. Dans la notation LTSA, cela donne lieu au modèle dans le fichier TCP simplified.lts (svp, regarder cela en utilisant LTSA). L'entité de protocole représentant l'usager A est l'initiateur, et B est le répondant. En faisant la composition SYSTEM, LTSA fait une analyse d'accessibilité et trouve qu'il n'y a pas de blocage. Nous avons aussi défini la propriété TCP_SERVICE qui représente la vue abstraite (boîte noire), ce qui dit que dataExchange peut seulement arriver après qu'un Listen et Connect ont eu lieu (dans n'importe quel ordre). En faisant la composition Check_Service, LTSA vérifie que cette propriété est réalisée par le système donné.

Version symétrique

La conception de TCP permet aux deux usagers A et B de faire une requête de connexion vers l'autre côté, possiblement en même temps.

• Dans " TCP symetric v2 ", les deux entités, A et B, ont le même comportement consistant de deux alternatives: initiateur ou répondant (comme dans la version simplifiée). LTSA trouve un blocage qui arrive quand les deux parties commencent avec le comportement de répondant (après les deux interactions listen). J'ai donc éliminé cette interaction, ce qui nous donne la version 2.
  • Version 2 a encore un blocage qui arrive quand les deux parties prennent le rôle d'initiateur. Ceci n'est pas vraiment un blocage dans le vrai monde, mais une réception non spécifiée. Ce problème avait déjà été trouvé par les concepteurs de TCP qui ont introduit une solution: si cela arrive, les deux côtés vont réaliser la situation (ils reçoivent un message sync après avoir envoyé leur propre sync), et il devraient établir la connexion. En regardant le diagramme de machine du Wikipedia, on trouve la transition avec la mention "simultaneous open". En introduisant cette transition dans notre modèle LTSA, nous avons la version 3.
• En vérifiant " TCP symmetric v3 " pour blocages, on trouve encore un problème. Est-ce que cela veut dire que la conception de TCP contient des erreurs ???
  • Je me demandais qu'est-ce qui se passe ici ... Puisque je crois que la conception de TCP est correcte, il pouvait y avoir les situations suivantes:
    • Mon modèle LTSA ne reflète pas correctement le modèle de la machine à états du Wikipedia.
    • Le modèle du Wikipedia ne reflète pas correctement la spécification de TCP.
  • Alors, j'ai commençé à vérifier mon modèle LTSA, et puis vérifier le dernier contre la définition de TCP originale (voir diagramme d'états). - et j'ai trouvé que le modèle du Wikipedia contient une erreur: Quand les deux côtés prennent le rôle d'initiateur, la transition étiquettée "simultaneous open" est exécutée des deux côtés, ce qui devrait envoyer un message ack et non pas un message ack-sync comme indiqué dans le Wikipedia. C'est parce que le prochain état attend un message ack pour établir la connexion, et non pas un ack-sync. En changeant la spécification LTSA en conséquence, nous obtenons la version 4.
• Vérifiant " TCP symmetric v4 " avec LTSA, nous ne trouvons pas de blocage. Aussi la propriété Check_Service (qui est un peu modifiée par rapport à la version simplifiée parce que l'interaction listen a été éliminée) est vérifiée pour cette version. Alors tout a l'air correct - Ouff.