Figure I.1: Une transition
| La modélisation est la première étape effectuée lors de l'analyse d'un système concurrent. Elle permet de décrire de manière formelle toutes les composantes faisant partie du système concurrent à analyser. Pour ce faire, le modèle doit permettre une représentation précise et non-ambigüe du comportement des processus impliqués dans la modélisation. |
|
La structure fondamentale du modèle d'Arnold-Nivat est l'automate fini. Celui-ci permet de représenter le comportement des systèmes concurrents à modéliser à l'aide de graphes orientés.
Dans le modèle, les sommets et les arêtes de ce graphe orienté sont appelés respectivement états et transitions. Ces états et transitions sont associés avec une chaîne de caractères de manière à pouvoir les distinguer entre eux. Ces chaînes de caractères s'appellent noms lorsqu'elles sont associées aux états, et étiquettes lorsqu'elles sont associées aux transitions.
Le graphe orienté lui-même, avec ses chaînes de caractères associés, est appelé système de transitions étiquetées.
Formellement, un système de transitions étiqueté par un alphabet d'actions U est un quintuplet A = <S,T,a,b,y> où
Les états d'un système de transitions sont directement associés aux états du système concurrent qu'il modélise. Les transitions quant à elles, jouent un rôle fondamental dans un système de transitions car ce sont elles qui servent à modéliser les actions faites par le système concurrent, l'étiquette d'une transition représentant le type d'action qui est effectué. Par exemple, dans la Figure I.1, lorsque le système de transitions passe de l'état nommé 1 à l'état nommé 2 en empruntant la transition t décrite par a(t) = 1, b(t) = 2 et dont l'étiquette est y(t) = "a", on dit que le système de transitions effectue, ou éxécute, l'action a.
Cependant, et contrairement aux noms d'états, plusieurs transitions peuvent avoir les mêmes étiquettes, ceci est même nécessaire pour exprimer certaines propriétés importantes, telle le non-déterminisme. On ne peut donc pas se référer uniquement aux étiquettes pour identifier une transition.
Il existe certaines actions spéciales, discutées au cours des chapitres suivants, et dont la plus importante est l'action nulle. Celle-ci sera définie immédiatement. Par exemple, il est possible, et souvent souhaitable, que l'on désire qu'un système de transitions n'effectue aucune action et qu'il puisse cependant être synchronisé avec les actions qu'effectuent d'autres systèmes de transitions. Cette transition existe, est nommée epsilon-transition, ou action nulle, et est étiquetée e. Elle est définie ainsi:
Soit A = <S,T,a,b,y> un système de transitions. Une epsilon-transition est une transition t, tel que y(t) = e et que pour tout s appartenant à S on a a(t) = b(t) = s. Autrement dit, le système de transitions A reste dans le même état lorsqu'il effectue l'action e.
En tout temps, dans le système de transitions, il n'y aura qu'un seul état qui sera actif. Celui-ci est nommé état courant et les étiquettes des transitions ayant comme état source l'état courant représenteront l'ensemble des actions que le système de transitions peut effectuer à cet instant précis.
Les systèmes de transitions permettent de représenter aisément et avec concision des concepts fondamentaux des systèmes concurrents, tel le choix, le non-déterminisme, le séquencement, l'infinité des traces [Hoare,78] . Le Tableau I.1 montre comment ces concepts peuvent être représentés dans le modèle des systèmes de transitions.
Le système de transitions de la Figure I.2 modélise le comportement d'une variable booléenne. L'ensemble d'états contient les deux valeurs possibles pour une variable booléenne, c'est-à-dire soit elle est vraie ou soit elle est fausse. L'alphabet dénombrant les actions possibles est U= { :=Vrai, :=Faux, Faux, Vrai }. Les deux premières actions modélisent le fait que l'on peut assigner une valeur booléenne à la variable. ":=Vrai" assignant la valeur Vrai à la variable et ":=Faux" assignant la valeur Faux. Les deux autres actions représentent le fait que l'on peut effectuer une requête pour déterminer la valeur de la variable.
Les systèmes de transitions ayant été définis, nous avons maintenant les éléments de base avec lesquels nous pouvons construire des modèles de systèmes concurrents. Chaque système de transitions sert à modéliser un processus bien spécifique du système concurrent.
Nous définissons maintenant un produit de systèmes
de transitions. Le produit libre de n systèmes de
transitions 
étiquetés par des alphabets 
, est noté
et 
et est le système de transitions 
défini par
On remarque qu'il s'agit d'une construction énorme, dont la taille est donnée par le produit de la taille des composants. En partie à cause de cela, le produit libre n'est pas souvent directement utilisable. L'intérêt de cette construction est qu'elle génère un système de transitions dont les états, qu'on nomme états globaux, sont composés de toutes les combinaisons possibles des états des sous-systèmes de transitions. De même, les transitions, qu'on nomme transitions globales ou actions globales, sont composées de toutes les combinaisons possibles des transitions des sous-systèmes de transitions.
Afin de bien expliquer le résultat du produit libre de plusieurs systèmes de transitions, voici un petit exemple.
Nous avons une liste de quatre petits systèmes de transitions. L'ordre des systèmes de transitions est important car c'est lui qui nous permettra de décrire les transitions et états globaux sous la forme de liste dont le ième état, ou la ième transition, appartient au ième système de transitions. Par exemple, la transition globale déterminée par les sous-transitions en gras dans le Tableau I.2 est identifiée par la liste (b.a.b.b). Il en va de même pour l'identification des états globaux. Cependant, afin de pouvoir différencier ces derniers de la représentation des transitions globales, leurs listes seront précédées de la lettre e.
Si on effectue le produit libre de ces quatre systèmes de transitions dans l'ordre, nous obtenons un système de transitions global comportant 48 états et 16 transitions. La figure suivante représente une petite section du système de transitions global, centrée sur l'état global e(0.2.0.0) qui représente l'état courant global, et qui est composé des états courants des sous systèmes de transitions. Les transitions marquées en gras dans les systèmes de transitions du Tableau I.2 représentent une unique transition globale, également marquée en gras, de la Figure I.3.
A partir de l'état courant global, il n'y a que quatre façons de combiner les transitions des sous-systèmes de transitions dont l'état source est l'état courant de manière à former des transitions globales. Ces transitions globales représentent le fait que chaque sous-système de transitions passe simultanément d'un état à un autre. La liste des sous-transitions ainsi empruntées forme une transition globale entre deux états globaux dans le produit libre.
On remarque également, étant donné que le produit libre est un produit cartésien des états et des transitions, il conserve complètement la structure de tous les sous-systèmes de transitions impliqués.
L'idée sous-jacente au produit synchronisé est de restreindre l'ensemble des transitions globales pouvant être effectuées aux seules transitions dont l'action globale sera définie dans la spécification du modèle. Il est en effet fort possible qu'une transition globale du produit libre soit composée de sous-actions qui sont mutuellement exclusives, contradictoires ou même illogiques du point de vue du système concurrent à modéliser.
Par exemple on pourrait avoir une transition globale produite par le produit libre, qui est définie comme suit.(A:=Vrai . A:=Faux). Ce qui représente clairement des sous-actions mutuellement exclusives, ne pouvant pas être effectuées simultanément, et qu'on doit exclure du produit synchronisé. De même, la transition globale (A:=Vrai . B:=Vrai), bien que parfaitement légale d'un point de vue logique peut être interdite ou impossible dans le modèle et devra donc être également exclue du produit synchronisé.
Soit 
les alphabets de n systèmes
de transitions. Une contrainte de synchronisation est un
sous-ensemble du produit cartésien 
. Les éléments
de cet ensemble sont appelés vecteurs de synchronisation
et sont représentés par des listes d'étiquettes
de transitions.
La contrainte de synchronisation décrit quelles sont les transitions globales du produit libre qui sont autorisées et qui vont être conservées lors du calcul du produit synchronisé. En effet, à chaque transition globale est associée une liste d'étiquettes représentant la liste des étiquettes des sous-transitions. Pour qu'une transition globale appartienne au produit synchronisé, il faut que sa liste d'étiquettes appartiennent à la contrainte de synchronisation. Donc, qu'elle soit égale à un des vecteurs de synchronisation.
L'appartenance d'une transition globale au produit synchronisé représente donc le fait que l'on force les sous-systèmes de transitions à coopérer entre eux de manière à ce qu'ils synchronisent leurs actions. Les transitions globales appartenant au produit synchronisé sont appelées transitions synchronisées, de même, les états globaux appartenant au produit synchronisé sont appelés états synchronisés.
Nous savons alors que le produit synchronisé
de n systèmes de transitions étiquetés
par des alphabets , et effectué sous la contrainte
de synchronisation C = {v1 ,v2, ... ,vm }, où les vi
représentent les m vecteurs
de synchronisation, est une partition connexe du produit libre
des Ai, formée par les restrictions suivantes:
présentes dans le produit synchronisé
sont celles du produit libre dont la liste d'étiquettes
appartiennent
à C.
Nous appellerons le résultat du produit synchronisé: système de transitions synchronisé. Il ne s'agit en fait que d'un système de transitions dans lequel les transitions et états représentent respectivement une liste de sous-transitions et de sous-états.
En prenant comme systèmes de transitions ceux du Tableau I.2 de la page 7, que nous nommerons S1, S2, S3 et S4, nous allons montrer un exemple de produit synchronisé. Il faut tout d'abord définir les vecteurs de synchronisation. Nous allons restreindre l'ensemble des vecteurs de synchronisation afin de ne pas générer un produit synchronisé qui soit trop gros. Toutefois, il ne peut pas être de dimension supérieure au produit libre, soit 48 états et 16 transitions, mais ceci est déjà trop grand pour être affiché ici.
Soit C une contrainte de synchronisation sur les systèmes de transitions S1, S2, S3 et S4, définie ainsi
En prenant comme états initiaux les états courants des systèmes de transitions S1, S2, S3 et S4, le résultat du produit synchronisé de ceux-ci sous la contrainte de synchronisation C est assez petit pour être calculable à la main et est donné par la Figure I.4.
Le comportement global des systèmes de transitions S1, S2, S3 et S4 sous la contrainte de synchronisation C est entièrement et complètement modélisé par le système de transitions synchronisé de la Figure I.4.
On remarque également que le produit synchronisé est connexe et qu'il est une forme très compacte de représentation de systèmes concurrents. Car bien que le résultat de ce produit synchronisé soit relativement complexe, les systèmes de transitions S1, S2, S3 et S4 ainsi que la contrainte de synchronisation C sont extrêmement simples.