1. Installation of TTool+

            Créez un répertoire de travail sur votre disk.

            Ouvrez la page http://www-sop.inria.fr/oasis/Vercors/software/TTool+/index.html dans votre navigateur.

            Recuperer les fichiers TTool+.jar et le fichier de configuration. Elle doivent se trouver dans le même répertoire, soit votre répertoire de travaille.

 Lancez TTool+.

Vérifiez que la machine virtuelle java est bien installé sur votre ordinateur.

A la console : java -jar TTool+.jar -lotos

2. Etude d'un model: ConsumerProducer.

           Recuperez le fichier ConsumerProducer.xml.

Ouvrez-le dans Turtle. Il y a deux modélisations. Le système ConsumerProducer avec un producteur et un seul consommateur ( ConsumerProducer 1p 1c) et le même système avec deux consommateurs( ConsumerProducer 1p 2c).

 Étudiez la diagramme de composantes et les diagrammes des machines d'état. Pour mieux comprendre, voir  Work Report Chapter5.

3. Système Voiture

On défini la spécification d'une voiture comme suivant:

Deux composantes principales: Board_Panel  et Car_Manager.

Car_Manager est composé par GearManager, SpeedManager et Engine.

Le fonctionnement:

Boar_Panel peux 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 peux 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=1 :

           nbRotations=0 -> speed=0

           nbRotations=1 ->speed=30

            nbRotations=2 ->speed=60.

La valeur calculée de la vitesse sera envoyé a l'Engine_Manager et au Board_Panel.

Travail a faire.

Recuperez le fichier car1.xml et ouvrez-le dans TTool+.

Effectuez une vérification de syntaxe: L'icône "syntax analysis".

Générez la specification formelle (Lotos): L'icône "Generate Lotos Specification".

Générez le graphe d'accessibilité : L'icône "Run Validation".

Le graphe généré (difficilement lisible) peut être vu a partir du menu "View->Show last RG".

Allez dans V&V->Analysis (Last AUT Graph). On trouve plusieurs deadlocks. Pouvez-vous trouver le problème et le corriger?

Correction (fichier car2.xml): Dans la sous-machine  "compute speed" on traite les cas gear=0 et gear=1 mais pas le cas gear=2.  La machine "speed_manager" ne sais donc pas traiter ce cas, d'où les deadlocks.

Rajouter une nouvelle fonctionnalité:  

  un deuxième panneau de bord pour le prof d'une voiture d'école.  Ce panneau a les fonctionnalités "accelerate" et "decelerate".

 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?

(Fichier car3.xml avec la fonctionnalité rajoutée).