CTTool Homework, with Corrections

Pour toute aide :

• sur le contenu du sujet : E. Madelaine
• sur les outils et la config: E. Salageanu

Lancement de CTTool

• récupérez le logiciel CTTool (CTTool.jar et config.xml); intallez-les chez vous dans le même répertoire.
• récupérez la doc (CTToolReport.pdf)
• récupérez les fichiers d'exemples: ConsumerProducer.xml et car1.xml
• Lancez CTTool (attention java 1.5 seulement): java -jar CTTool.jar -lotos -proactive

Exemple du Consumer / Producer

• Ouvrez le fichier ConsumerProducer.xml: (Dans l'éditeur CTTool, File->Open->... )
• Étudiez le diagramme de composants et les diagrammes des machines d'état. Pour mieux comprendre, voir CTToolReport Chapter5.

Exemple d'un Systeme de contrôle de boite de vitesse : Utilisation des outils CTTool / CADP

• On définit la spécification d'une voiture de la manière suivante:
  Deux composantes principales: Board_Panel et Car_Manager. Car_Manager est composé des sous-composants GearManager, SpeedManager et Engine.
• Le fonctionnement: Boar_Panel peut envoyer des messages "change_gear" au Car_Manager. On considère que gear peut prendre seulement les valeurs 1 et 2.
  Gear_Manager traite ce message et envoie un message "updateGear" au composant speedManager.
  BoardPanel peut envoyer des messages "accelerate" et "deccelerate" au Car_Manager.
  Speed_Manager traite ces messages. Il augmente ou diminue le nb de rotations (limite a 2). Speed_Manager calcule la vitesse de la façon suivante:
  
  • pour gear=1 :
    • nbRotations=0 -> speed=0
    • nbRotations=1 -> speed=20
    • nbRotations=2 -> speed=30.
  • pour gear=2 :
    • nbRotations=0 -> speed=0
    • nbRotations=1 -> speed=30
    • nbRotations=2 -> speed=60.
  La valeur calculée de la vitesse sera envoyée à l'Engine_Manager et au Board_Panel.
• Travail à faire :
  • Effectuez une vérification de syntaxe: L'icône "Syntax Analysis".
  • Générez la spécification formelle (Lotos): L'icône "Generate Lotos Specification".
  • Analyser la syntaxe du code généré (et créer les fichiers intermédiaires): Bouton "Check Synatx of Formal Code".
  • Générez le graphe d'accessibilité : L'icône "Run Validation".
  • Le graphe généré (difficilement lisible) peut être vu à partir du menu "View->Show last RG".

  Questions :

  • Allez dans V&V->"Analysis (Last AUT Graph)". On trouve plusieurs deadlocks. Pouvez-vous trouver le problème et le corriger?
    • Réponse: On remarque que, dans la sous-machine computeSpeed de la machine d'état SpeedManager le cas gear=2 n'est pas traité. Au moment ou gear arrive dans la position 2 le système ne peut pas calculer la vitesse et se retrouve dans une situation de deadlock.
      Le model corrigé: car2.xml - a sauvegarder et ouvrir avec CTTool
      
  • Rajouter une nouvelle fonctionnalité:
    un deuxième panneau de bord pour le prof d'une auto-école. Ce panneau a les fonctionnalités "accelerate" et "decelerate".
    • Corrigé: car2.xml - a sauvegarder et ouvrir avec CTTool
      
  • On remarque que le graphe d'accessibilité de ce deuxième modèle a le même nombre d'états mais plus de transitions. Pourquoi?
    • Corrigé: Les actions faites par BordPanelProf (accelerate et decelerate) se trouvent aussi parmi les actions du BoardPanel et ont le même effet sur le système que celles-ci. En rajoutant le BoardPanelProf on se retrouve avec un nombre plus grand de transitions entre les mêmes états (ou, plutôt, des états équivalentes aux premiers)
      
  • Equivalences observationelles et Minimisation:
    Générez une ou plusieurs minimisations des graphes d'accessibilité du "Consumer / Producer" et "Car" et étudiez les. Pour ce faire:
    • Allez dans V&V->"Make minimization".
    • Dans l'interface graphique qui apparaît sélectionner les messages que vous voulez garder dans le graphe minimisé.
      Appuyez ensuite sur Start.
    • Pour visualiser le graphe minimisé ainsi créé : View->Minimized RG.

  ---

  Eric Madelaine
  Last modified: Fri Oct 27 10:58:49 CEST 2006