 |  |  |
| Dans le chapitre précédent , nous avons vu comment on peut, à l'aide du modèle d'Arnold-Nivat, modéliser un système concurrent. Cependant, bien que le modèle permet de décrire précisément le système en question, cette description n'est pas d'une grande utilité sans la capacité de pouvoir vérifier que le système se comporte bien de la manière désirée. |
|
Maintenant que l'on dispose d'une méthode permettant de
construire le produit synchronisé, on a déja effectué
un certain travail de validation. En effet, seules les transitions
globales qui sont définies comme vecteurs de synchronisation
apparaissent dans le produit synchronisé. Par construction,
le système de transitions synchronisé n'effectue
donc que des actions légales et autorisées.
Cependant ceci ne garantit pas que la modélisation d'un
système concurrent sous la forme d'un système de
transitions synchronisé soit exempt de comportement non-désirables.
Contrairement aux systèmes séquentiels, où
la validation peut être effectuée à l'aide
de simulations et d'analyses modulaires, les systèmes concurrents
ne peuvent être validés que par des méthodes
formelles. Elles seules peuvent apporter une certitude mathématique
sur le respect de la spécification par une modélisation
d'un système concurrent.
La syntaxe utilisée pour décrire les opérateurs,
termes et expressions de ce chapitre est celle implémentée
dans le logiciel MEC. Cependant, il faut noter que ce chapitre
n'est pas un manuel ni d'utilisation, ni de référence
pour le logiciel MEC. Le lecteur intéressé en trouvera
un dans [Arnold-Bégay-Crubillé, 94].
Dans tout ce qui suit, A = <S ,T ,a ,b > est le système
de transitions étiqueté de référence
et on a S1,S2 inclu dans S et
T1,T2 inclu dans T.
Afin de pouvoir valider mathématiquement un système
de transitions synchronisé modélisant un système
concurrent, il faut disposer d'outils capables d'exprimer formellement
les propriétés que l'on veut vérifier. Ces
outils existent et sont appellés logiques. Elles
permettent de calculer si un ensemble d'états ou de transitions
est le résultat d'une expression formelle décrivant
une propriété. Quelques logiques de systèmes
de transitions ont été définies. Entre-autres:
C'est une extension de cette dernière que nous allons vous
présenter car c'est celle qui a été implémentée
dans le logiciel MEC.
Les termes de la logique des systèmes de transitions sont
représentés par des ensembles d'états ou
des ensembles de transitions. On appelle ces ensembles des marques.
Selon le type d'ensemble représenté, on parlera
de marque de transitions ou marque d'états.
Les marques peuvent être définies en affectant à
celles-ci le résultat de la composition d'un ou plusieurs
opérateurs.
Il existe trois marques prédéfinies, dont deux sont
de type indéterminé. Les marques de type indéterminé
prennent le type soit d'une marque d'états, soit d'une
marque de transitions dépendant du contexte dans lequel
elles sont utilisées. Ce sont:
| * = S lorsqu'il s'agit d'une marque d'états |
| * = T lorsqu'il s'agit d'une marque de transitions |
| {}= 0S lorsqu'il s'agit d'une marque d'états |
| {}= 0T lorsqu'il s'agit d'une marque de transitions |
Comme les marques sont des ensembles, il est normal que l'on
désire effectuer des opérations ensemblistes sur
celles-ci. On utilise les opérateurs ensemblistes usuels.
Ils agissent soit sur des ensembles de transitions, soit sur
des ensembles d'états. Le langage utilisé est typé
et sa syntaxe implique un type compatible sur les opérantes
d'une expression et également sur les paramètres
des opérateurs.
A titre d'exemple le Tableau II-1 décrit la représentation
graphique de l'opérateur union opérant sur les états
d'un système de transitions. Dans cet exemple, ainsi que
dans les exemples suivants, les états et les transitions
marqués seront représentés respectivement
par des cercles et lignes en trait gras.
|
| | |
Ces opérateurs effectuent la liaison entre les marques
d'états et les marques de transitions en permettant de
calculer des relations entre les états et les transitions.
Cet opérateur retourne l'ensemble des états qui
sont la source des transitions de l'ensemble des transitions données
en paramètre. Il est défini par
 |  |
Cet opérateur retourne l'ensemble des états qui
sont la cible de l'ensemble des transitions données en
paramètre. Il est défini par
 |  |
Cet opérateur retourne l'ensemble des transitions dont
l'état source appartient à l'ensemble des états
donnés en paramètre. Il est défini par
 |  |
Cet opérateur retourne l'ensemble des transitions dont
l'état cible appartient à l'ensemble des états
donnés en paramètre. Il est défini par
 |  |
Remarque
Les opérateurs src,
tgt sont respectivement
les inverses des opérateurs rsrc,
rtgt. Nous avons en
effet les identités suivantes:
S1 = src(rsrc( S1 )), S1 = tgt(rtgt( T1 )) T1 = rsrc(src( T1 )), T1 = rtgt(tgt( T1 ))
Cette classe d'opérateurs est constituée d'opérateurs
dont le calcul requiert un parcours non-linéaire des états
et des transitions sur le graphe sous-jacent d'un système
de transitions. Ce ne sont pas des opérateurs atomiques
de la logique de Dicky. Ils sont introduits ici car ils sont
utilisés intensivement afin de pouvoir exprimer certaines
propriétés importantes.
Cet opérateur prend deux paramètres, un ensemble
d'états S1 représentant les états
sources et un ensemble de transitions T1 représentant
les transitions que l'on est autorisé à emprunter.
Le résultat est un ensemble d'états représentant
tous les états qui sont accessibles depuis l'ensemble des
états sources S1 et en empruntant seulement
que les transitions qui appartiennent à l'ensemble des
transitions autorisées T1. C'est la
solution du calcul du plus petit point fixe de l'équation
suivante:
Reach = tgt(rsrc(S1 \/ Reach ) /\ T1)
Cet opérateur est calculé itérativement de
la manière suivante
Reachn+1 = tgt(rsrc(S1 \/ Reachn ) /\ T1)
avec Reach0 ={}
comme condition initiale et Reachn+1
- Reachn = {} comme condition d'arrêt.
 |  |  |
Cet opérateur prend deux paramètres, un ensemble
d'états S1 représentant les états
cibles et un ensemble de transitions T1 représentant
les transitions que l'on est autorisé à emprunter.
Le résultat est un ensemble d'états représentant
tous les états d'où il est possible d'atteindre
les états de l'ensemble des états cibles S1
et en empruntant seulement que les transitions qui appartiennent
à l'ensemble des transitions autorisées T1.
C'est la solution du calcul du plus petit point fixe de l'équation
suivante:
CoReach = src(rtgt(S1 \/ CoReach ) /\ T1)
Cet opérateur est calculé itérativement de
la manière suivante
CoReachn+1 = src(rtgt(S1 \/ CoReachn ) /\ T1)
avec CoReach0 = {}
comme condition initiale et CoReachn+1
- CoReachn = {} comme condition d'arrêt.
 |  |  |
Cet opérateur retourne les transitions formant des cycles.
Il prend comme paramètres deux ensembles de transitions.
Le premier ensemble, T1, représente
les transitions autorisées. Toutes les transitions faisant
parties d'un cycle doivent appartenir à T1.
De plus, au moins une des transitions de chacun des cycles doit
appartenir à l'ensemble T2,
 |  |  |
Cet opérateur prend comme paramètres, deux ensembles
d'états S1, S2 et un
ensemble de transitions autorisées T1.
Il retourne l'ensemble des transitions représentant un
plus court chemin de l'ensemble d'états S1
à l'ensemble d'états S2 en ne
passant que par les transitions autorisées T1.
 |  |
 |  |
Les opérateurs peuvent être combinés ensemble pour produire des expressions décrivant les propriétés que l'on désire valider. On peut se poser la question suivante: Comment fait on pour travailler de manière concrète avec ces opérateurs? Evidement, lors de l'analyse des résultats des calculs, on ne travaille pas sur une représentation graphique comme dans ce chapitre, ce qui serait tout à fait inutile dès que la taille des systèmes de transitions impliqués dépasse quelques dizaines d'états. Disposer de la liste des éléments appartenant à une marque peut être utile dans certains cas, mais ce n'est pas très utile en général lorsque le nombre d'éléments est très grand.
Or les propriétés que l'on désire tester sont habituellement des propriétés booléennes où ce que l'on veut savoir sont des réponses à des questions comme: La marque contient elle ou non des éléments? Il est suffisant de se baser uniquement sur le cardinal de celles-ci pour une interprétation rapide du résultat d'un calcul.
Voyons maintenant quelques exemples de propriétés génériques. Ce sont des propriétés importantes qui ne dépendent pas de la nature des systèmes concurrents ni de la modélisation de ceux-ci.
En combinant les opérateurs src, rsrc,
tgt et rtgt, il est possible de créer
de nouvelles fonctions permettant d'effectuer un parcours par
étape d'un système de transitions. Ceci n'est pas
une propriété, mais est utilisé à
maintes reprises dans la définition des propriétés
génériques qui vont suivre.
| Les états successeurs | EtatsSucc(S1) = tgt(rsrc(S1)) |
| Les états prédécesseurs | EtatsPred(S1) = src(rtgt(S1)) |
| Les transitions suivantes | TransSuiv(T1) = rsrc(tgt(T1)) |
| Les transitions précédentes | TransPrec(T1) = rtgt(src(T1)) |
Cette propriété est fortement liée à l'utilisation de l'opérateur reach. On veut savoir si, à partir des états synchronisés initiaux, et en ne passant que par des transitions autorisées, il est possible d'atteindre des états donnés.
Par exemple, dans un système de transitions modélisant une chaîne de montage, on peut définir une marque de transitions ActionsLegales représentant les opérations que la chaîne de montage peut effectuer, et définir également une marque d'état Defectueux représentant des états dans lequel la chaîne de montage produit un élément défectueux.
On peut alors poser la question suivante: A partir de la mise en route de la chaîne de montage, est-il possible qu'en n'effectuant que des opérations de montage correctes, on puisse produire un élément défectueux?
L'expression ci-dessous nous donne l'ensemble des états
où l'on a produit un élément défectueux
malgré le fait que l'on ait effectué que des opérations
correctes.
Defect:= Defectueux /\ reach(Defectueux, ActionsLegales)
Le système est exempt d'état défectueux non
contrôlés si on a
|Defect| = 0.
Une propriété souvent non désirable d'un système concurrent est l'inter-blocage (deadlock). C'est le blocage non désiré d'au moins un des processus du système concurrent par un autre processus. Dans le produit synchronisé, ceci se traduit par un état synchronisé d'où ne sort aucune transition synchronisée. Il s'agit donc d'un état d'où il est impossible d'effectuer une action.
Cette condition particulière se retrouve habituellement lorsque deux processus tentent de s'approprier une ressource partagée et que le processus ayant réussi à obtenir cette ressource se trouve dans l'impossibilité de la libérer.
Pour vérifier que le système est exempt d'inter-blocage,
il suffit de calculer l'expression suivante:
Deadlock:= * - src()
Le système est exempt d'état bloquant lorsque
|Deadlock| = 0.
Pour beaucoup de systèmes concurrents, il existe des états biens spécifiques signifiant que le processus modélisé est en état d'attente. Par exemple, un daemon sous Unix, qui attend une action particulière afin de s'activer et d'effectuer la tâche qu'il a à faire.
Or, une recherche négative des inter-blocages ne signifie pas pour autant que le processus fonctionne bien. Une propriété intéressante à vérifier est que, de tout état il est possible de revenir, par une séquence d'actions, à un des états d'attente. Si ce n'était pas le cas, il serait alors possible de bloquer le processus dans un cycle d'actions infini et on ne pourrait plus alors avoir accès au processus de nouveau.
On est donc en mesure de vérifier s'il existe des états
d'où on ne peut jamais revenir à au moins un des
états marqués Attente, signifiant que le
processus est prêt à accepter une tâche. Ceci
ce traduit par l'expression:
PasDeRetour:= * - coreach(Attente, *)
Le système est exempt d'état défectueux non
contrôlés lorsque
|PasDeRetour| = 0.
Nous venons de définir l'inter-blocage et la co-accessiblité. Une des propriétés intéressantes qui en découle est celle des états critiques. Ce sont des états, qui une fois atteints par le système, conduisent à un état bloquant, et ce quelque soit la suite de transitions empruntée par la suite.
Il faut tout d'abord calculer les états bloquants, tels
que définis précédemments:
Deadlock:= * - src()
Calculons maintenant la marque EtatsCritiques. Les états
inévitablement bloquants sont certainement inclus dans
ceux d'où on ne peut pas revenir à un des états
marqués Initial. Encore une fois tel que défini
précédemment:
PasDeRetour:= * - coreach(Initial, *)
Il faut enlever de PasDeRetour les états d'où
il est impossible d'atteindre un des états bloquants.
C'est le cas des états formant un cycle ne pouvant pas
conduire à un état bloquant et ne pouvant pas revenir
à l'état initial. Les états restants sont
inévitablement bloquant.
EtatsInevBloquant:= PasDeRetour /\ coreach(Deadlock,*)
Les états critiques forment la frontière de cet
ensemble d'états, et sont calculés par
EtatsCritiques:= tgt(rtgt(*-PasDeRetour) /\ rsrc(PasDeRetour)))
Les états critiques nous permettent de définir
une autre propriété, les transitions critiques.
Ce sont les transitions qui forment la frontière entre
l'ensemble des états critiques et le reste des états
du système de transitions. Une fois que le système
a emprunté une de ces transitions critiques, il va se retrouver
inévitablement dans un des états bloquants.
TransCritiques:= rtgt(*-PasDeRetour) /\ rsrc(PasDeRetour)
Un autre comportement important est celui de la famine (livelock). Il s'agit d'une autre forme de blocage d'un processus par un autre. A la différence de l'inter-blocage toutefois, la famine ne bloque qu'un seul des deux processus.
Cette situation se retrouve lorsque deux processus ont l'occasion d'obtenir l'accès à une ressource partagée. Il suffit qu'un des processus obtienne toujours la ressource en la reprenant dès qu'il la libère et ce avant que le deuxième processus n'ait le temps de s'en emparer. Le processus bloqué est toujours en condition d'attente tandis que l'autre processus continue de s'exécuter normalement.
Il y a donc un cycle dans la séquence des actions éxécutées, et c'est donc l'opérateur loop qui sera utilisé dans la détection des transitions formant une famine possible.
On définit les marques Execution1 et Execution2 comme représentant respectivement les états durant lesquels les processus 1 et 2 sont actifs et possèdent l'utilisation exclusive de la ressource. Ceci peut être fait car le processus qui ne possède pas la ressource reste dans l'état d'attente. Execution1 contient donc les états synchronisés dans lesquels le ième sous-état, correspondant à l'indice du système de transitions modélisant le processus 2 dans la liste des systèmes de transitions du produit synchronisé, est l'état d'attente du processus 2.
De plus on définit également les marques d'états Obtention1 et Obtention2 représentant les états où respectivement le processus 1 ou le processus 2 peut obtenir la ressource.
Il faut maintenant déterminer quels sont les états
où les deux processus sont sur le point d'obtenir la ressource.
ObtentionDouble:= Obtention1 /\ Obtention2
Nous allons maintenant trouver un cycle de famine pour le processus 1. C'est-à-dire une séquence d'actions durant laquelle le processus 1 prend la ressource, l'utilise, la relâche et ensuite peut la reprendre immédiatement.
Les transitions menant ou sortant des états ou le processus
1 possède l'utilisation exclusive de la ressource sont:
TransExecution1:= rsrc(Execution1) \/ rtgt(Execution1)
Un cycle de famine pour le processus 1 doit nécessairement
passer par l'une des transitions sortant des états de ObtentionDouble
et doit être entièrement inclus dans TransExecution1.
Le calcul suivant nous donne les transitions faisant partie
de ce cycle
TransFamine:= loop(TransExecution, rsrc(ObtentionDouble))
Il y a un cycle de famine pour le processus 1 lorsque
|TransFamine| = 0
Si c'est le cas, les états impliqués dans ce cycle
sont donnés par l'expression suivante:
EtatsFamine:= src(TransFamine) /\ tgt(TransFamine)