Jouer avec l'outil LTSA (modéliser des machines à états communicant par rendez-vous)

Une introduction à l'outil LTSA et son utilisation (voir fichier d'exemples "check properties") ont été expliquées en classe. Une explication de la syntaxe du langage pour écrire des spécifications LTS acceptables par l'outil est donnée ici.

Partie 1: Revision

• Tâche (A): Allez à travers les exemples dans le fichier "check properties" et exécutez les commandes LTSA nécessaires pour vérifier que vous avez bien compris les opérations de cet outil.

Partie 2: Exemple de l'hôtel

S.v.p., regardez l'exemple de l'hôtel encore et chargez le fichier "hotel-room-and-restaurant-3" dans l'outil LTSA. Regardez les diagrammes d'états des différentes composantes du système et du système global. Faites une simulation interactive en utilisant la commande Check -> Run.

• Tâche (B): Vérifier si les séquences de test (1) à (4) sont exécutables par le modèle. Note: Pour voir les résultats de la composition du SYSTEM avec Sequence_1, il faut sélectionner sur la barre sur la fenêtre graphique la sélection TEST_1 (au lieu de SYSTEM).
  • Expliquez ce qui se passe dans le cas de problèmes. Est-ce que vous pensez que la spécification du modèle devrait être changée pour réaliser les séquences de tests (les prenant comme cas d'utilisation des exigences), ou est-ce qu'il y a une erreur dans les cas d'utilisation ?
• Tâche (C): Modifier la spécification du système Hotel (version 3) de telle manière que le client doit manger dans le restaurant avant de faire le checkOut.
  • Étape 1: Pensez ! - Pensez comment résoudre ce problème, quels changements à introduire pour les différentes machines (le moins de changements possible).
  • Étape 2: Faire les changements proposés et compiler.
  • Étape 3: Composer le système et vérifier qu'il satisfait les exigences ci-hautes (par exemple, en regardant le diagramme du comportement global et en vérifiant qu'il n'y a pas de blocage).
  • Question C: (a) expliquez les changements que vous avez faits, (b) montrez la spécification changée, (c) expliquez les vérifications que vous avez faites.

Part 3: Exemple du système de téléphones

• Tâche (D): Chargez l'exemple telephone-system dans l'outil LTSA.
  • Étape 1: Lire le texte qui décrit le système téléphonique et les cas de tests. Compiler l'exemple (commandes build -> parse; build -> compile) Regarder les trois diagrammes de transitions pour les trois composantes du système (cliquer sur DRAW, puis sélectionner chaque composante dans la fenêtre à gauche); jouer avec la grandeur des diagrammes en cliquant sur les symboles bizarres entre la fenêtre gauche et les diagrammes.
    • Vérifier que les diagrammes font du bon sens - est-ce que vous pensez que la spécification définit un comportement convenable pour ces trois composantes ?
    • Question D.1: L'état appelé WAIT dans le comportement de la définition de PHONE1, par quel état du diagramme de transitions est-il représenté ? (c'est-à-dire, quel est le numéro d'état correspondant dans le diagramme graphique ?). Similairement, pour l'état TALKING1, et pour l'état BUSY du comportement de PHONE2.
    • Utilisez l'animateur de l'outil pour réaliser des exécutions simulées du système téléphonique (la commande check -> run ). L'animateur montre les interactions qui sont possibles à chaque moment de l'exécution.
    • Construire la composition des trois composantes (commande build -> compose); regarder le diagramme du comportement global de cette composition, appelée PHONE_SYSTEM (cliquer encore sur DRAW). Est-ce que ce comportement fait du bon sens ?
  • Maintenant, nous voulons voir si certaines séquences d'interactions peuvent être réalisées par la spécification donnée du PHONE_SYSTEM. Pour cela, nous combinons le PHONE_SYSTEM avec une séquence d'exécution et nous appelons cette composition TEST. L'exemple LTSA contient trois tels tests, TEST1, TEST2 et TEST3. Pour voir le résultat de la composition du PHONE_SYSTEM avec la séquence Sequence_1, il faut sélectionner TEST1 (dans la barre de sélection au dessus de la fenêtre des diagrammes) au lieu de la sélection PHONE_SYSTEM utilisée auparavent; ensuite exécuter la commande de composition, et puis regarder le diagramme qui en résulte. Vous allez voir que la séquence Sequence_1 au complet est là, ce que veut dire que cette séquence peut être réalisée par le PHONE_SYSTEM.
  • Faire de même pour TEST2.
  • Faire de même pour TEST3.
    • Question D.2: Pourquoi cette séquence n'est par réalisable ? (comme on voit, elle termine au milieu) ?
  • Jouez avec d'autres séquences d'exécutions en définissant vous-même une Sequence_4 et TEST4, etc.
  • Répondez aux questions suivantes:
    • Question D.3: Qu'est-ce qu'il arrive si d'abord les deux téléphones font un pick_up et puis l'usager du PHONE1 fait un dial pendant que l'usager du PHONE2 fait un hang_up ? - Utilisez LTSA pour trouver la réponse.
    • Question D.4: Par quelle séquence d'exécution pourrait-on modéliser le cas que les deux usagers font le pick_up en même temps ? (Comment peut-on modéliser, en général, des interactions simultanées ? - Note: les LTS communiquent par rendez-vous.) - Similairement, le cas où les deux font un hang_up simultanément ?
  • Il y a une erreur de conception dans la description du système téléphonique, en effet, quand l'usager du PHONE2 au début fait un pick_up et va dans l'état BUSY, le PHONE2 ne peut quitter cet état jusqu'à ce qu'il soit appelé par PHONE1 et les deux téléphones font un hang_up simulatanément (la raison est que l'interaction hang_up est un rendez-vous entre les deux téléphones, un téléphone ne peut pas le faire tout seul).
    • Question D.5: Modifiez la spécification du modèle pour permettre aux deux usagers de faire un hang-up correctement dans la situation où une connection a été établie et dans la situation où l'Usager 2 était busy (comme suggéré dans la question de boni du Lab1). La spécification devrait être telle que le SWITCH sache quand une connexion termine. Suggestion: introduire deux interactions hang-up différentes.
      • Analysez la Safety de votre spécification.
      • Écrivez quelques séquences d'interactions (similaires que celles données dans la spécification originale) qui représentent quelques cas d'utilisation typiques et vérifiez que ces séquences peuvent être exécutées par le modèle du système téléphonique.

A remettre

Ceci est un lab "informel". À la fin du laboratoire, s.v.p., montrez au TA les brouillons de textes et de diagrammes que vous avez préparés pour votre travail sur les tâches (A) à (D). 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.