Lab-4 - SEG-2506 - Vérification de systèmes concurrents

Partie A: Un exercice en analyse d'accessibilité sur papier

Nous considérons deux machines d'états avec le comportement montré sur le diagramme ci-dessous. Les machines communiquent par l'échange de messages asynchrones et des files d'attente FIFO. Les messages sont nommés a, b, c, d et e.

Vos tâches:

1. Faites une analyse d'accessibilité pour explorer le comportement du système global qui est formé par les deux machines d'états communicants. Dessinez les états globaux qui sont accessibles de l'état initial du système, et les transitions impliquées (en utilisant la notation introduite dans les notes de cours).
2. Identifiez des problèmes de conception (s'il y en a) - tel que des réceptions non spécifiées ou des blocages.
3. Pour chaque problème identifié, expliquez une solution possible en indiquant les changements que vous suggérez à appliquer aux spécifications des deux machines d'états. Si vous avez assez de temps, vérifiez que les solutions proposées produisent un comportement du système sans problèmes.

À préparer:

1. Esquisse du graphe d'accessibilité pour le système global.
2. Courtes explications des points 2 et 3 ci-dessus (et un deuxième graph d'accessibilité si vous avez le temps de le faire)

Partie B: Analyser d'autres versions de TCP par LTSA

Nous commençons avec la version 4 de la spécification LTSA de TCP, comme discutée dans les notes de cours.

Vos tâches:

1. Modifier la spécification TCP pour réaliser les interactions de service à la OSI, comme montrées dans la figure (b) dans les notes de cours: Version 5
• Éliminer les primitives Connect et Listen (déjà éliminé) et introduire les primitives montrées dans la figure (b) dans des états appropriés de la machine à états. Ceci devient la version 5. Vérifier qu'il n'y a pas de blocage.
• Définir une nouvelle version de la propriété Check_Service et vérifier que la spécification du système réalise cette propriété.
2. Inclure la phase de disconnexion (comme montrée par le diagramme de Wikipedia): Version 6
• Après la phase d'échange de données (l'état Established) inclure la phase de disconnexion comme décrite dans le diagramme de Wikipedia. Notes:
  • CLOSE est une primitive de service par laquelle l'usager indique qu'il veut terminer la connexion. Après cette primitive, l'usager ne devrait plus envoyer de données, mais il pourrait toujours en recevoir de l'autre côté.
  • fin est un type de message, indiquant que l'usager qui l'a envoyé veut terminer la connexion. En réponse, on envoie un message ack. Ceci est similaire que le protocole d'établissement de connexion.
3. Inclure une version simple d'échange de données en supposant que les données des usagers sont envoyées dans des messages data entre les deux parties.
• Avec TCP, la transmission de données peut commencer dans l`état Established et peut continuer jusqu'à ce qu'une primitive CLOSE est exécutée localement. Cela veut dire que la réception de données peut continuer dans d'autres états de la phase de disconnexion. Le but de ce travail est de déterminer dans quels états il ne pourrait y avoir de réception de données pendant la phase de disconnexion.
• Étape 1: (a) Introduire des transitions d'envoi de données dans tous les états où cela est permis (transitions envoyant un message data et retournant dans le même état). (b) Introduire des transitions de réception de données dans l'état Established et tous les états de la phase de disconnexion (transitions recevant un message data et retournant dans le même état). Ceci devient la version 7. Vérifier que cette version n'a pas de blocage.
• Étape 2: Pour chaque état de la phase de disconnexion, éliminer la transition de réception de données et vérifier si cela introduit un blocage. Sinon, il n'y aura jamais de réception de données dans cet état.
• Résultat: Les états dans lequels il n'y aura jamais de réception de données.

A remettre

Ceci est un lab "informel". À la fin du laboratoire, s.v.p., montrez au TA les brouillons de diagrammes et textes et spécifications LTSA que vous avez préparés pour votre travail. Le TA prendra note de la complétude (ou non) de votre travail, mais n'évaluera pas la qualité de vos travaux.

S.v.p., consultez le TA pendant les sessions de laboratoire. Le rôle du TA est de vous aider à faire les travaux suggérés dans les laboratoires.