MSC II : Automates communicants -- UPPAAL
Support de cours
Zoom :
Pensez svp à ouvrir au début de chaque TP une session Zoom
via votre navigateur
(Pas besoin d'installation de client ni de compte -- accès anonyme via "Join from Your Browser")
Zoom : 98327490725
Contexte du TP
On considè le problème du choix distant
(rapidement) décrit dans la partie Petri (cf support pp 47-51).
Dans le cadre de cet TP, on envisage différentes versions
dans le cas de communication synchrone par
- signal (section I et II)
- échange de valeurs (section III).
I Choix résolu par la synchronisation
On considère un système - décrit par le fichier rdv.xta - constitué par deux entités, Left et Right dont le
comportement est donné ci-dessous ;
Les deux composants se synchronisent sur s, puis ont le choix soit :
- d’une communication de gauche à droite (gauche envoi sur a tandis que droit reçoit sur a)
- d’une communication de droite à gauche (droit envoi sur b tandis que gauche reçoit sur b)
Après l’une ou l’autre de ces communications, chaque composant va de façon indépendante dans l’état reinit.
Lorsqu’ils sont tous les deux dans l’état reinit, une synchronisation sur f a lieu et les deux composants
retrouvent leur état initial.
Simulation
- Exhibez une exécution où la communication a lieu de gauche à droite
- Exhibez une exécution où la communication a lieu de droite à gauche
- Exhibez une exécution infinie comportant uniquement des communications de gauche
à droite
- Exhibez une exécution infinie comportant uniquement des communications de droite
à gauche.
- Les diverses simulations effectuées vous assurent-elles que le système est exempt de blocage ?
- Assurez-vous que le système ne bloque pas en évaluant la formule suivante A[] not deadlock
sous le model-checker (onglet verifier).
II Choix non déterministe
On considère maintenant le système décrit par le fichier nondet.xta.
Le système est toujours constitué de deux
entités Left et Right. La modélisation de celles-ci repose sur un process unique
paramétré par deux canaux de communication respectivement dédiés à la réception et à l'émission.
Questions
- Modélisation
- Etudiez l'ensemble de la description (déclarations globales, définition des process. instanciation, déclaration du système)
- Complétez l'instanciation du process rec pour obtenir les instances letf
et right
- Simulation
- Exhibez une exécution où la communication a lieu de gauche à droite
- Exhibez une exécution où la communication a lieu de droite à gauche
- Exhibez une exécution où le système est bloqué
- Vérification
Allez sous le vérificateur. Chargez (menu query)
le fichier de propriétés specifs.q. Evaluez chaque propriété.
Quelles conclusions pouvez-vous en tirer ?
III Choix autoritaire (tournant)
Pour résoudre le problème de choix, on admet que l’un des processus (left) est maître - décide du sens de communication - et que l’autre (le disciple) obéit.
L'automate du process rc est partiellement représenté ci-dessous.
- Comprenez l'implantation du process rc .
- Vous utiliserez la synchronisation sur le canal s et la
variable partagée vp pour
transmettre le choix du maître au disciple.
- Pour debugguer votre système, simulez-le et retrouvez les scénarios décrits dans la section 1.
- Pour vérifier - et non plus se persuader - que votre système est correct, allez sous le vérificateur.
Chargez (menu query) le fichier de propriétés specifs.q. Assurez vous que chaque propriété est bien
satisfaite.
- Pour obtenir une solution un peu plus symétrique, on veut maintenant
que le statut de “maître” échoit à tour de rôle à chacun des
deux processus.
- Implantez cette solution.
- Simulez le système pour le “debugger”.
- Considérez les propriétés décrites dans le fichier stud.q. Donnez-en une interprétation et évaluez-les.