Master 2010 2011
cps: TME 8 : Modélisation de la concurrence - 1

Dans ce TME, nous utilisons l’outil LTSA pour modéliser et analyser des systèmes concurrents simples.

Dans un premier temps, on installera l’outil LTSA que l’on peut récupérer ici

Exercice 1 : machines à expresso

Question 1

Définir un modèle simple de machine à expresso dont le fonctionnement est le suivant.

Compiler votre modèle et lancer le mode de simulation (menu run). On vérifiera que le modèle ne possède pas de deadlock avec le menu safety.

Question 2

Définir une second machine à expresso dont la particularité est de pouvoir tomber en panne à n’importe quel moment. Une fois en panne la machine est bloquée dans l’état STOP. Testez le mode simulation et lancez à nouveau l’analyse de safety.

Exercice 2 : Usinage

On modélise dans cet exercice un système très simple d’usinage.

Question 1

On modélise d’abord deux chaînes de fabrication pour des objets A et B. Chaque chaîne prépare un objet A ou B puis déclare que l’objet est prêt. La chaîne se met ensuite en attente.

Question 2

Les objets fabriqués par les chaînes de la question précédente sont assemblées dans une chaîne d’assemblage. Une fois que les objets A et B sont prêts, on procède à l’assemblage et on « réveille » ensuite les chaînes de fabrication.

L’usine est constitués de la mise en parallèle des deux chaînes de fabrication avec la chaîne d’assemblage. Compiler et composer le système obtenu puis vérifier que la synchronisation entre les chaînes est correcte.

Question 3

Plutôt que de définir deux chaînes de fabrication séparée, on peut exploiter le renommage d’actions pour factoriser les définitions.

On rappelle la syntaxe du renommage d’actions :

Process/{nouvelle1/ancienne1,nouvelle2/ancienne2/...)

Question 4

Une fois le protocole de synchronisation établi, on souhaite en général vérifier des propriétés « fonctionnelles ». Pour cela, le principe est de cacher les actions utilisés pour la synchronisation.

On rappelle la syntaxe pour cacher des actions :

Process\{action1,action2,...}

Après composition du système, les actions cachées sont remplacées par des actions internes tau. On peut s’abstraire (de l’essentiel) des actions internes en sélectionnant le menu Minimize. Comparez le LTS obtenu avant et après minimisation (onglet Draw).

Question 5

Une autre façon de cacher le protocole de synchronisation est de forcer l’interface d’un système.

La syntaxe pour forcer une interface est la suivante :

Process@{action1,action2,...}

Dans ce cas, seules les actions de l’interface seront visibles, toutes les autres actions sont cachées.

Proposer une variante de l’usine avec interface forcée.

Exercice 3

Dans cet exercice, l’objectif est de modéliser un système de type client/serveur.

Question 1

Voici des modèles simplifiés pour les clients et le serveur :

Client = (call->wait->run->Client).
Server = (request->service->reply->Server).

Proposer un système composé d’un client et d’un serveur.

Question 2

On souhaite maintenant modéliser un système pour \codeN clients. Les définitions préliminaires sont les suivantes :

const N = 3  // nb de clients
range T = 1..N    // indices pour chaque client

Pour chaque client connecté, un service spécifique sera instancié. On utilise la définition suivante pour les services :

Service = (c[i].start->Service[i]),
Service[i:T] = (c[i].deliver->c[i].end->Service)

Le sous-système des clients est composé de la façon suivante :

||Clients = (c[i:T]:(Client/{request/call,reply/wait}))

Et le système complet est le suivant :

||System = (MServer || Clients)\{c[i:T].start,c[i:T].end}

Proposer une définition du serveur MServer

Question 3

Proposer une variante parallèle du serveur qui, pour chaque client, « lance » un sous-processus Service en parallèle.