CREATION ET MISE EN OEUVRE D'UN DESIGN PATTERN
Le but de cet exemple est d'illustrer la construction et la mise en oeuvre d'un "design pattern". On peut parler aussi de "modèle générique" ou de "patron de conception".
D'une manière générale, il est plus facile de travailler sur des modèles de petite taille que sur des gros. Par ailleurs, certaines problématiques sont récurrentes à différents systèmes. Pour ces deux raisons, il est intéressant d'être en mesure d'élaborer des modèles génériques.
L'exemple traité ici se retrouve dans les systèmes connus tels que :
- la synchronisation de deux bases de données configurés en mode "maître - esclave",
- le rejeu à l'identique d'un processus qui s'est déroulé dans le passé, à des fins de compréhension et d'analyse
- la réplication de données entre systèmes distribués.
L'illustration va comporter trois parties :
- une première partie destinée à construire le modèle générique, donc en l'occurrence, le mécanisme d'enregistrement d'une histoire d'un processus quelconque et de rejeu de cette histoire pré-enregistrée.
- une deuxième partie destinée à représenter le processus dont on souhaite enregistrer l'evolution puis la rejouer,
- une troisième partie destinée à illustrer l'instanciation des paramètres du modèle générique obtenue dans la première partie, avec le résultat obtenu sur la seconde partie.
Premier développement
Nous allons d'abord visualiser de manière progressive la réplication entre deux systèmes représentés de manière complètement générique. De fait donc, le dispositif de réplication sera donc valide pour tout système discret à répliquer.
Le système dont nous souhaitons répliquer le comportement est à représenter de manière la plus abstraite possible. Nous allons considérer qu'il prend ses états dans un ensemble baptisé S et qu'il a un état initial baptisé s0. Nous pouvons donc élaborer un contexte baptisé c00 dans lequel est introduit l'ensemble S et l'axiome suivant : "s0 est un élément de S".
Nous allons supposer que la réplication fonctionne comme suit :
- Le système principal évolue durant un temps puis s'arrête. Durant ce temps le système secondaire n'a pas bougé.
- Une fois que le système principal est arrêté, le système secondaire évolue pour se remettre dans le même état que le système principal.
- à ce moment-là le système principal peut à nouveau évoluer (retour au point 1).
ITERATION 0
Notre première observation du fonctionnement de ce l'ensemble de ce système (système principal et système secondaire) va comporter un seul instant d'observation. Celui-ci est choisi de telle sorte que la scène visualisée est celle où les deux systèmes sont toujours dans le même état. Certes, entre deux instants d'observation consécutifs, les deux systèmes principal et secondaire ont évolué l'un après l'autre. Mais pour le moment l'observateur choisit de ne pas le voir.
Si on baptise ep l'état du système principal et es l'état du système secondaire, ces deux variables seront toujours perçues comme égales. Nous allons donc introduire la propriété invariante suivante : "ep = es"
Le seul évènement que nous allons considérer peut être baptisé "le système global évolue". Cet évènement permet de tracer le fait que l'état des deux systèmes a évolué entre deux instants consécutifs d'observation.
Voici le résultat de la modélisation.
MODELE OBTENU :
Nous pouvons noter que le système ne se bloque jamais : la garde de l'évènement est de la forme "Il existe s tel que s appartienne à S". Comme est S est non vide, le prédicat est donc toujours vrai.
ITERATION 1
Nous allons à présent simplement observer l'ensemble du système "plus souvent".
Nous allons ajouter un instant d'observation. Il est choisi de telle sorte qu'il soit placé entre le moment où le système principal a évolué et le moment où le système secondaire va évoluer pour finalement rattraper son "retard" par rapport au système principal.
Nous avons donc deux évènements désormais au lieu d'un seul auparavant. Baptisons-les :
- "le système principal évolue"
- "le système secondaire évolue"
Pour établir un lien de raffinement entre l'événement abstrait et les deux événements concrets il nous faut introduire une variable permettant de mémoriser le fait que le système principal seul a évolué. Baptisons cette variable "spe" ("le Système Principal a Evolué") et considérons qu'il s'agit d'un booléen.
Ce booléen est initialisé à faux au démarrage du système global.
Il est positionné à vrai lorsque l'observateur a vu le système principal prendre de l'avance par rapport au système secondaire et à faux lorsque le système secondaire a rattrapé son retard.
Voici le résultat de la modélisation.
MODELE OBTENU :
vous pouvez noter :
- qu'il y a eu un changement de variable ("ep" ne pouvant pas être modifié au sein d'un nouvel événement, il a été rebaptisé "ep2") ;
- que le paramètre "s" de l'évènement raffiné a disparu. En effet, l'état final du système secondaire doit être égal à l'état du système principal. Cependant la méthode nous impose de définir un "witness" dans ce cas pour permettre de tracer le lien entre "s" et la valeur qu'il prend désormais dans cet évènement. Ce witness sert pour la production des obligations de preuve.
ITERATION 2
Nous allons à nouveau observer plus souvent le système. Pour le moment la perception de l'évolution du système principal ou secondaire était global.
L'observateur va désormais observer :
- l'évolution pas à pas du système principal (le nombre maximal de pas possible est plafonné) ;
- le remplissage d'une file dont l'objet est de mémoriser l'histoire du système principal ;
- la consommation du contenu de cette file pour permettre au système secondaire de rattraper pas à pas son retard par rapport au système principal.
Une variable baptisée "h" (pour "Histoire") est introduite pour mémoriser l'ensemble des états intermédiaires pris par le système principal. Il s'agit d'une file.
Une variable baptisée "i" (pour index) est introduite pour mémoriser la premier position disponible dans cette file.
Une variable baptisée "j" est introduite pour mémoriser le prochain élément à consommer dans la file pour permettre au système secondaire de refaire son retard.
Une constante baptisée "mx" (pour maximum) est introduite pour borner la taille de la file.
L'évènement "le système principal évolue" va être remplacé par un enchaînement de 3 évènements :
- "le système principal évolue pas à pas 1" : cet évènement permet d'initier l'évolution pas à pas du système principal. il ne se produit qu'une seule fois.
- "le système principal évolue pas à pas 2" : cet évènement permet de faire évoluer le système principal pas à pas. Cet évènement se succède à lui-même un certain nombre de fois. Le nombre consécutif de fois où cet évènement se répète est toutefois limité du fait que la taille de la file est bornée.
- "le système principal évolue pas à pas 3" : cet évènement permet de faire terminer la phase d'évolution du système principal.
Pour permettre de démontrer que l'ensemble formé par ces 3 évènements raffine l'évènement abstrait "le système principal évolue" il est nécessaire d'introduire une variable supplémentaire baptisée "esp" (pour "évolution du système principal en cours"). Il s'agit d'un booléen.
Nous procédons de même avec le système secondaire en introduisant une variable booléenne baptisée "ess" (pour "évolution du système secondaire en cours").
Voici le résultat de la modélisation.
MODELE OBTENU :
Vous pouvez noter qu'un variant a été introduit : "mx - i + mx - j".
Il s'agit d'un nombre entier naturel qui est décrémenté d'une unité par chacun des deux évènements suivants lorsque l'ou ou l'autre de ces deux évènements se produit :
- "le système principal évolue pas à pas 2"
- "le système secondaire évolue pas à pas 2"
Le but recherché est de démontrer que chacun de ces deux événements ne sont pas susceptibles de "garder la main indéfiniment" aux dépens des autres évènements du système.
Pour l'évènement "le système principal évolue pas à pas 2", le nombre "mx - i" est réduit d'une unité à chaque fois que cet événement se produit. Ce nombre "mx - i" étant positif ou nul, cet évènement ne peut donc pas se succéder à lui-même indéfiniment.
Il en de même pour l'évènement "le système secondaire évolue pas à pas 2" avec le nombre entier "mx - j".
ITERATION 3
Désormais la description de l'observation du système principal est affinée. Ce système principal est désormais perçu comme un ensemble d'opérations.
Ces opérations sont simplement définies comme des fonctions partielles du produit cartésien de S par S dans S.
Un des deux paramètres de chaque opération correspond à l'état antérieur du système avant l'appel de l'opération.
Le second paramètre correspond aux éventuelles informations introduites par l'opérateur pour paramétrer l'opération.
MODELE OBTENU :
ITERATION 4
Deux files mémorisant l'histoire de l'évolution du système principal sont observées :
- une première file mémorise les opérations appelées,
- une seconde file mémorise les paramètres utilisés.
Plutôt que de mémoriser la définition des opérations utilisées, il est plus judicieux de mémoriser es identifiants de ces opérations appelées.
On suppose qu'à deux opérations distinctes sont associées deux identifiants distincts.
Voici le résultat de la modélisation.
MODELE OBTENU :
Deuxième développement
Nous allons ici créer représenter un service d'annuaire simple (la gestion du contenu d'un bottin téléphonique).
Bien qu'il soit tout à fait de représenter ce système simple en une seule étape, nous allons procéder en deux étapes pour illustrer une fois de plus la notion de raffinement.
Cet annuaire comporte un ensemble de personnes. il est possible d'en ajouter et d'en retirer.
Chaque personne comporte un nom, un prénom, un ou plusieurs numéros de téléphone.
il est possible de modifier le nom, le prénom et les numéros de téléphone associés à une personne.
Néanmoins le service garantit l'impossibilité de trouver deux personnes distinctes comportant à la fois le même nom et le même prénom. De même un numéro de téléphone ne peut être rattaché à deux personnes distinctes.
ITERATION 0
L'observateur ne visualise qu'un ensemble de personnes qu'il est possible d'accroître ou de réduire.
MODELE OBTENU :
ITERATION 1
L'observateur visualise le détail de l'annuaire. il perçoit le nom, le prénom et les numéros de téléphone associés à chaque personne.
il perçoit aussi les propriétés suivantes :
- Deux personnes distinctes ne peuvent avoir à la fois le même nom et le même prénom.
- Chaque personne a au moins un numéro de téléphone.
- Un même numéro de téléphone ne peut être rattaché à deux personnes distinctes.
il est possible de modifier les attributs d'une personne.
Il est toujours possible d'ajouter des personnes ou d'en retirer.
MODELE OBTENU :
Troisième développement
Nous souhaitons instancier les paramètres du modèle issu du premier développement avec le résultat issu du second développement.
Les paramètres à instancier sont l'ensemble des états S et l'ensemble des opérations OP.
Dans le second développement, nous allons supposer que chaque évènement observe individuellement chaque opération du système. Il suffit alors de formaliser ces opérations pour préparer l'instanciation qui va suivre.